Theorem elab2g 3638

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 2853	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})
3		elab2g.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	3	elabg 3634	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))
5	2, 4	bitrid 286	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1568   ∈ wcel 2141  {cab 2739

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1571  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836

This theorem is referenced by:  elab2  3640  elab4g  3641  elrab  3649  eldif  3914  elin  3920  elun  4106  elpwg  4564  elsng  4602  elprg  4611  eluni  4874  elintg  4919  eliun  4959  eliin  4960  elopabw  5510  elxpi  5683  elrn2g  5880  eldmg  5888  dmopabelb  5906  elrnmpt  5948  elrnmpt1  5950  elimag  6066  elong  6368  elrnmpog  7545  elrnmpores  7548  eloprabi  8059  orderseqlem  8152  frrlem13  8294  tfrlem12  8375  elqsg  8760  fsetfocdm  8857  elixp2  8898  isacn  10027  isfin1a  10275  isfin2  10277  isfin4  10280  isfin7  10284  isfin3ds  10312  elwina  10670  elina  10671  iswun  10688  eltskg  10734  elgrug  10776  elnp  10971  elnpi  10972  iscat  17727  isps  18623  isdir  18653  ismgm  18698  elefmndbas2  18932  elsymgbas2  19442  mdetunilem9  22756  istopg  23031  isbasisg  23083  isptfin  23652  isufl  24049  isusp  24397  2sqlem9  27567  elno  27786  elz12s  28641  isuhgr  29376  isushgr  29377  isupgr  29400  isumgr  29411  isuspgr  29468  isusgr  29469  cplgruvtxb  29729  isconngr  30506  isconngr1  30507  isplig  30794  isgrpo  30815  elunop  32190  adjeu  32207  isarchi  33468  ispcmp  34213  eulerpartlemelr  34713  eulerpartlemgs2  34736  ballotlemfmpn  34851  elkarden  35534  isacycgr  35603  isacycgr1  35604  ismfs  36007  dfon2lem3  36241  elaltxp  36433  elttcirr  37008  bj-ismoore  37713  heiborlem1  38428  heiborlem10  38437  isass  38463  isexid  38464  ismgmOLD  38467  elghomlem2OLD  38503  elcoeleqvrels  39296  eleldisjs  39445  gneispace2  44828  ismnu  44941  nzss  44997  elrnmptf  45869  issal  46998  ismea  47135  isome  47178  ismgmALT  48955  eloprab1st2nd  49613  setrec1lem1  50432