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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837

This theorem is used 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  5509  elxpi  5682  elrn2g  5879  eldmg  5887  dmopabelb  5905  elrnmpt  5947  elrnmpt1  5949  elimag  6065  elong  6368  elrnmpog  7547  elrnmpores  7550  eloprabi  8058  orderseqlem  8151  frrlem13  8293  tfrlem12  8374  elqsg  8759  fsetfocdm  8856  elixp2  8897  isacn  10035  isfin1a  10282  isfin2  10284  isfin4  10287  isfin7  10291  isfin3ds  10319  elwina  10677  elina  10678  iswun  10695  eltskg  10741  elgrug  10783  elnp  10978  elnpi  10979  iscat  17734  isps  18630  isdir  18660  ismgm  18705  elefmndbas2  18939  elsymgbas2  19449  mdetunilem9  22788  istopg  23063  isbasisg  23115  isptfin  23684  isufl  24081  isusp  24429  2sqlem9  27602  elno  27821  elz12s  28676  isuhgr  29421  isushgr  29422  isupgr  29445  isumgr  29456  isuspgr  29513  isusgr  29514  cplgruvtxb  29774  isconngr  30551  isconngr1  30552  isplig  30839  isgrpo  30860  elunop  32235  adjeu  32252  isarchi  33511  ispcmp  34256  eulerpartlemelr  34756  eulerpartlemgs2  34779  ballotlemfmpn  34894  elkarden  35576  isacycgr  35645  isacycgr1  35646  ismfs  36049  dfon2lem3  36283  elaltxp  36475  elttcirr  37070  bj-ismoore  37775  heiborlem1  38490  heiborlem10  38499  isass  38525  isexid  38526  ismgmOLD  38529  elghomlem2OLD  38565  elcoeleqvrels  39356  eleldisjs  39505  gneispace2  44886  ismnu  44999  nzss  45055  elrnmptf  45927  issal  47056  ismea  47193  isome  47236  ismgmALT  49016  eloprab1st2nd  49674  setrec1lem1  50493