Theorem elab2g 3637

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2145  {cab 2740

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837

This theorem is used by:  elab2  3639  elab4g  3640  elrab  3648  eldif  3912  elin  3918  elun  4103  elpwg  4563  elsng  4601  elprg  4610  eluni  4873  elintg  4918  eliun  4958  eliin  4959  elopabw  5508  elxpi  5681  elrn2g  5878  eldmg  5886  dmopabelb  5904  elrnmpt  5946  elrnmpt1  5948  elimag  6064  elong  6369  elrnmpog  7551  elrnmpores  7554  eloprabi  8063  orderseqlem  8158  frrlem13  8300  tfrlem12  8381  elqsg  8766  fsetfocdm  8865  elixp2  8911  isacn  10050  isfin1a  10297  isfin2  10299  isfin4  10302  isfin7  10306  isfin3ds  10334  elwina  10698  elina  10699  iswun  10716  eltskg  10762  elgrug  10804  elnp  10999  elnpi  11000  iscat  17764  isps  18660  isdir  18690  ismgm  18735  elefmndbas2  18987  elsymgbas2  19504  mdetunilem9  22846  istopg  23124  isbasisg  23176  isptfin  23746  isufl  24143  isusp  24491  2sqlem9  27664  elno  27883  elz12s  28738  isuhgr  29518  isushgr  29519  isupgr  29542  isumgr  29553  isuspgr  29613  isusgr  29614  cplgruvtxb  29874  isacycgr  30631  isacycgr1  30632  isconngr  30670  isconngr1  30671  isplig  30958  isgrpo  30979  elunop  32354  adjeu  32371  isarchi  33624  ispcmp  34369  eulerpartlemelr  34870  eulerpartlemgs2  34893  ballotlemfmpn  35008  elkarden  35683  ismfs  36130  dfon2lem3  36364  elaltxp  36557  elttcirr  37152  bj-ismoore  37857  heiborlem1  38563  heiborlem10  38572  isass  38598  isexid  38599  ismgmOLD  38602  elghomlem2OLD  38638  elcoeleqvrels  39429  eleldisjs  39578  gneispace2  44974  ismnu  45087  nzss  45143  elrnmptf  46015  issal  47144  ismea  47281  isome  47324  ismgmALT  49140  eloprab1st2nd  49798  setrec1lem1  50615