Theorem elab2g 3659

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809

This theorem is referenced by:  elab2  3661  elab4g  3662  elrab  3671  eldif  3936  elin  3942  elun  4128  elpwg  4578  elsng  4615  elprg  4624  eluni  4886  elint  4928  elintg  4930  eliun  4971  eliin  4972  elopabw  5501  elxpi  5676  elrn2g  5870  eldmg  5878  dmopabelb  5896  elrnmpt  5938  elrnmpt1  5940  elimag  6051  elong  6360  elrnmpog  7540  elrnmpores  7543  eloprabi  8060  orderseqlem  8154  frrlem13  8295  tfrlem12  8401  elqsg  8780  fsetfocdm  8873  elixp2  8913  isacn  10056  isfin1a  10304  isfin2  10306  isfin4  10309  isfin7  10313  isfin3ds  10341  elwina  10698  elina  10699  iswun  10716  eltskg  10762  elgrug  10804  elnp  10999  elnpi  11000  iscat  17682  isps  18576  isdir  18606  ismgm  18617  elefmndbas2  18850  elsymgbas2  19352  mdetunilem9  22556  istopg  22831  isbasisg  22883  isptfin  23452  isufl  23849  isusp  24198  2sqlem9  27388  elno  27607  elnoOLD  27608  elzs12  28338  isuhgr  28985  isushgr  28986  isupgr  29009  isumgr  29020  isuspgr  29077  isusgr  29078  cplgruvtxb  29338  isconngr  30116  isconngr1  30117  isplig  30403  isgrpo  30424  elunop  31799  adjeu  31816  isarchi  33126  ispcmp  33834  eulerpartlemelr  34335  eulerpartlemgs2  34358  ballotlemfmpn  34473  isacycgr  35113  isacycgr1  35114  ismfs  35517  dfon2lem3  35749  elaltxp  35939  bj-ismoore  37069  heiborlem1  37781  heiborlem10  37790  isass  37816  isexid  37817  ismgmOLD  37820  elghomlem2OLD  37856  elcoeleqvrels  38559  eleldisjs  38692  gneispace2  44103  ismnu  44233  nzss  44289  elrnmptf  45153  issal  46291  ismea  46428  isome  46471  ismgmALT  48146  eloprab1st2nd  48791  setrec1lem1  49499