Theorem elab2g 3647

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803

This theorem is referenced by:  elab2  3649  elab4g  3650  elrab  3659  eldif  3924  elin  3930  elun  4116  elpwg  4566  elsng  4603  elprg  4612  eluni  4874  elint  4916  elintg  4918  eliun  4959  eliin  4960  elopabw  5486  elxpi  5660  elrn2g  5854  eldmg  5862  dmopabelb  5880  elrnmpt  5922  elrnmpt1  5924  elimag  6035  elong  6340  elrnmpog  7524  elrnmpores  7527  eloprabi  8042  orderseqlem  8136  frrlem13  8277  tfrlem12  8357  elqsg  8737  fsetfocdm  8834  elixp2  8874  isacn  9997  isfin1a  10245  isfin2  10247  isfin4  10250  isfin7  10254  isfin3ds  10282  elwina  10639  elina  10640  iswun  10657  eltskg  10703  elgrug  10745  elnp  10940  elnpi  10941  iscat  17633  isps  18527  isdir  18557  ismgm  18568  elefmndbas2  18801  elsymgbas2  19303  mdetunilem9  22507  istopg  22782  isbasisg  22834  isptfin  23403  isufl  23800  isusp  24149  2sqlem9  27338  elno  27557  elnoOLD  27558  elzs12  28337  isuhgr  28987  isushgr  28988  isupgr  29011  isumgr  29022  isuspgr  29079  isusgr  29080  cplgruvtxb  29340  isconngr  30118  isconngr1  30119  isplig  30405  isgrpo  30426  elunop  31801  adjeu  31818  isarchi  33136  ispcmp  33847  eulerpartlemelr  34348  eulerpartlemgs2  34371  ballotlemfmpn  34486  isacycgr  35132  isacycgr1  35133  ismfs  35536  dfon2lem3  35773  elaltxp  35963  bj-ismoore  37093  heiborlem1  37805  heiborlem10  37814  isass  37840  isexid  37841  ismgmOLD  37844  elghomlem2OLD  37880  elcoeleqvrels  38586  eleldisjs  38720  gneispace2  44121  ismnu  44250  nzss  44306  elrnmptf  45175  issal  46312  ismea  46449  isome  46492  ismgmALT  48211  eloprab1st2nd  48856  setrec1lem1  49676