Theorem elab2g 3561

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

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1601   ∈ wcel 2107  {cab 2763

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-v 3400

This theorem is referenced by:  elab2  3562  elab4g  3563  elrab  3572  eldif  3802  elun  3976  elin  4019  elsng  4412  elprg  4419  eluni  4674  elintg  4718  eliun  4757  eliin  4758  elopab  5220  elrn2g  5558  eldmg  5564  elrnmpt  5618  elrnmpt1  5620  elimag  5724  elong  5984  elrnmpt2g  7049  elrnmpt2res  7051  eloprabi  7512  tfrlem12  7768  elqsg  8081  elixp2  8198  isacn  9200  isfin1a  9449  isfin2  9451  isfin4  9454  isfin7  9458  isfin3ds  9486  elwina  9843  elina  9844  iswun  9861  eltskg  9907  elgrug  9949  elnp  10144  elnpi  10145  iscat  16718  isps  17588  isdir  17618  ismgm  17629  elsymgbas2  18184  mdetunilem9  20831  istopg  21107  isbasisg  21159  isptfin  21728  isufl  22125  isusp  22473  2sqlem9  25604  isuhgr  26408  isushgr  26409  isupgr  26432  isumgr  26443  isuspgr  26501  isusgr  26502  cplgruvtxb  26761  isconngr  27592  isconngr1  27593  isfrgr  27666  isplig  27903  isgrpo  27924  elunop  29303  adjeu  29320  isarchi  30298  ispcmp  30522  eulerpartlemelr  31017  eulerpartlemgs2  31040  ballotlemfmpn  31155  ismfs  32045  dfon2lem3  32278  orderseqlem  32341  elno  32388  elaltxp  32671  bj-ismoore  33632  heiborlem1  34234  heiborlem10  34243  isass  34269  isexid  34270  ismgmOLD  34273  elghomlem2OLD  34309  gneispace2  39386  nzss  39472  elrnmptf  40290  issal  41458  isome  41635  ismgmALT  42874  setrec1lem1  43539