elab2 - Metamath Proof Explorer

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

Theorem elab2 3671

Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995.)

**Assertion**
Ref	Expression
elab2	⊢ (𝐴 ∈ 𝐵 ↔ 𝜓)

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

**Proof of Theorem elab2**
Step	Hyp	Ref	Expression
1		elab2.1	. 2 ⊢ 𝐴 ∈ V
2		elab2.2	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3		elab2.3	. . 3 ⊢ 𝐵 = {𝑥 ∣ 𝜑}
4	2, 3	elab2g 3669	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝐵 ↔ 𝜓))
5	1, 4	ax-mp 5	1 ⊢ (𝐴 ∈ 𝐵 ↔ 𝜓)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 = wceq 1534 ∈ wcel 2099 {cab 2705 Vcvv 3471

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699

This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806

This theorem is referenced by: opabidw 5526 opabid 5527 oprabidw 7451 oprabid 7452 soseq 8164 wfrlem3OLDa 8331 tfrlem3a 8397 fsetfcdm 8878 cardprclem 10002 iunfictbso 10137 aceq3lem 10143 dfac5lem4 10149 kmlem9 10181 domtriomlem 10465 ltexprlem3 11061 ltexprlem4 11062 reclem2pr 11071 reclem3pr 11072 supsrlem 11134 supaddc 12211 supadd 12212 supmul1 12213 supmullem1 12214 supmullem2 12215 supmul 12216 01sqrexlem6 15226 infcvgaux2i 15836 mertenslem1 15862 mertenslem2 15863 4sqlem12 16924 conjnmzb 19206 sylow3lem2 19582 mdetunilem9 22521 txuni2 23468 xkoopn 23492 met2ndci 24430 2sqlem8 27358 2sqlem11 27361 madef 27782 eulerpartlemt 33991 eulerpartlemr 33994 eulerpartlemn 34001 subfacp1lem3 34792 subfacp1lem5 34794 rdgssun 36857 finxpsuclem 36876 heiborlem1 37284 heiborlem6 37289 heiborlem8 37291 cllem0 42996 fsetsnf 46433 fsetsnfo 46435 cfsetsnfsetf 46440 cfsetsnfsetf1 46441 cfsetsnfsetfo 46442

	
		OSZAR »