elab2g - Metamath Proof Explorer

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

Theorem elab2g 3668

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

**Hypotheses**
Ref	Expression
elab2g.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
elab2g.2	⊢ 𝐵 = {𝑥 ∣ 𝜑}

**Assertion**
Ref	Expression
elab2g	⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ 𝜓))

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

**Proof of Theorem elab2g**
Step	Hyp	Ref	Expression
1		elab2g.2	. . 3 ⊢ 𝐵 = {𝑥 ∣ 𝜑}
2	1	eleq2i 2818	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})
3		elab2g.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	3	elabg 3664	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))
5	2, 4	bitrid 282	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ 𝜓))

Colors of variables: wff setvar class

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

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 2697

This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803

This theorem is referenced by: elab2 3670 elab4g 3671 elrab 3681 eldif 3957 elin 3963 elun 4148 elpwg 4610 elsng 4647 elprg 4655 eluni 4916 elint 4960 elintg 4962 eliun 5005 eliin 5006 elopabw 5532 elxpi 5704 elrn2g 5897 eldmg 5905 dmopabelb 5923 elrnmpt 5962 elrnmpt1 5964 elimag 6073 elong 6384 elrnmpog 7561 elrnmpores 7564 eloprabi 8077 orderseqlem 8171 frrlem13 8313 tfrlem12 8419 elqsg 8797 fsetfocdm 8890 elixp2 8930 isacn 10087 isfin1a 10335 isfin2 10337 isfin4 10340 isfin7 10344 isfin3ds 10372 elwina 10729 elina 10730 iswun 10747 eltskg 10793 elgrug 10835 elnp 11030 elnpi 11031 iscat 17685 isps 18593 isdir 18623 ismgm 18634 elefmndbas2 18864 elsymgbas2 19370 mdetunilem9 22613 istopg 22888 isbasisg 22941 isptfin 23511 isufl 23908 isusp 24257 2sqlem9 27456 elno 27675 elnoOLD 27676 isuhgr 28996 isushgr 28997 isupgr 29020 isumgr 29031 isuspgr 29088 isusgr 29089 cplgruvtxb 29349 isconngr 30122 isconngr1 30123 isplig 30409 isgrpo 30430 elunop 31805 adjeu 31822 isarchi 33045 ispcmp 33659 eulerpartlemelr 34178 eulerpartlemgs2 34201 ballotlemfmpn 34315 isacycgr 34956 isacycgr1 34957 ismfs 35360 dfon2lem3 35592 elaltxp 35782 bj-ismoore 36795 heiborlem1 37495 heiborlem10 37504 isass 37530 isexid 37531 ismgmOLD 37534 elghomlem2OLD 37570 elcoeleqvrels 38276 eleldisjs 38409 gneispace2 43782 ismnu 43918 nzss 43974 elrnmptf 44771 issal 45918 ismea 46055 isome 46098 ismgmALT 47583 setrec1lem1 48416

	
		OSZAR »