elrab3 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > elrab3		Structured version Visualization version GIF version

Theorem elrab3 3680

Description: Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 5-Oct-2006.)

**Hypothesis**
Ref	Expression
elrab.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

**Assertion**
Ref	Expression
elrab3	⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ 𝜓))

Distinct variable groups: 𝜓,𝑥 𝑥,𝐴 𝑥,𝐵 Allowed substitution hint: 𝜑(𝑥)

**Proof of Theorem elrab3**
Step	Hyp	Ref	Expression
1		elrab.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
2	1	elrab 3679	. 2 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))
3	2	baib 534	1 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ 𝜓))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 = wceq 1533 ∈ wcel 2098 {crab 3418

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696

This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-rab 3419 df-v 3463

This theorem is referenced by: unimax 4948 fnelfp 7184 fnelnfp 7186 fnse 8138 fin23lem30 10367 isf32lem5 10382 negn0 11675 ublbneg 12950 supminf 12952 sadval 16434 smuval 16459 dvdslcm 16572 dvdslcmf 16605 isprm2lem 16655 isacs1i 17640 isinito 17988 istermo 17989 subgacs 19124 nsgacs 19125 odngen 19544 sdrgacs 20701 lssacs 20863 mretopd 23040 txkgen 23600 xkoco1cn 23605 xkoco2cn 23606 xkoinjcn 23635 ordthmeolem 23749 shft2rab 25481 sca2rab 25485 lhop1lem 25990 ftalem5 27054 vmasum 27194 eqscut2 27785 elmade 27840 israg 28573 ebtwntg 28865 eupth2lem3lem3 30112 eupth2lem3lem4 30113 eupth2lem3lem6 30115 cycpmco2lem1 32939 cycpmco2lem4 32942 cycpmco2 32946 ssdifidllem 33268 1arithufdlem2 33360 tgoldbachgt 34426 cvmliftmolem1 35022 neibastop3 35977 fdc 37349 pclvalN 39493 dvhb1dimN 40589 hdmaplkr 41516 aks4d1p8 41690 sticksstones1 41749 fsuppssind 41961 diophren 42375 islmodfg 42635 fsovcnvlem 43585 ntrneiel 43653 radcnvrat 43893 supminfxr 44984 stoweidlem34 45560

	
		OSZAR »