Theorem elab2g 3696

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ∈ wcel 2108  {cab 2717

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819

This theorem is referenced by:  elab2  3698  elab4g  3699  elrab  3708  eldif  3986  elin  3992  elun  4176  elpwg  4625  elsng  4662  elprg  4670  eluni  4934  elint  4976  elintg  4978  eliun  5019  eliin  5020  elopabw  5545  elxpi  5722  elrn2g  5915  eldmg  5923  dmopabelb  5941  elrnmpt  5981  elrnmpt1  5983  elimag  6093  elong  6403  elrnmpog  7585  elrnmpores  7588  eloprabi  8104  orderseqlem  8198  frrlem13  8339  tfrlem12  8445  elqsg  8826  fsetfocdm  8919  elixp2  8959  isacn  10113  isfin1a  10361  isfin2  10363  isfin4  10366  isfin7  10370  isfin3ds  10398  elwina  10755  elina  10756  iswun  10773  eltskg  10819  elgrug  10861  elnp  11056  elnpi  11057  iscat  17730  isps  18638  isdir  18668  ismgm  18679  elefmndbas2  18909  elsymgbas2  19414  mdetunilem9  22647  istopg  22922  isbasisg  22975  isptfin  23545  isufl  23942  isusp  24291  2sqlem9  27489  elno  27708  elnoOLD  27709  elzs12  28439  isuhgr  29095  isushgr  29096  isupgr  29119  isumgr  29130  isuspgr  29187  isusgr  29188  cplgruvtxb  29448  isconngr  30221  isconngr1  30222  isplig  30508  isgrpo  30529  elunop  31904  adjeu  31921  isarchi  33162  ispcmp  33803  eulerpartlemelr  34322  eulerpartlemgs2  34345  ballotlemfmpn  34459  isacycgr  35113  isacycgr1  35114  ismfs  35517  dfon2lem3  35749  elaltxp  35939  bj-ismoore  37071  heiborlem1  37771  heiborlem10  37780  isass  37806  isexid  37807  ismgmOLD  37810  elghomlem2OLD  37846  elcoeleqvrels  38551  eleldisjs  38684  gneispace2  44094  ismnu  44230  nzss  44286  elrnmptf  45088  issal  46235  ismea  46372  isome  46415  ismgmALT  47946  setrec1lem1  48779