Theorem elab2g 3211

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

Syntax hints:   → wi 4   ↔ wb 191   = wceq 1468   ∈ wcel 1937  {cab 2491

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485

This theorem depends on definitions:  df-bi 192  df-an 380  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-v 3068

This theorem is referenced by:  elab2  3212  elab4g  3213  eldif  3436  elun  3601  elin  3644  elsng  4009  elprg  4014  eluni  4231  eliun  4312  eliin  4313  elopab  4750  elrn2g  5073  eldmg  5078  elrnmpt  5130  elrnmpt1  5132  elimag  5222  elong  5482  elrnmpt2g  6483  elrnmpt2res  6485  eloprabi  6932  tfrlem12  7184  elqsg  7496  elixp2  7609  isacn  8560  isfin1a  8807  isfin2  8809  isfin4  8812  isfin7  8816  isfin3ds  8844  elwina  9196  elina  9197  iswun  9214  eltskg  9260  elgrug  9302  elnp  9497  elnpi  9498  iscat  15744  isps  16613  isdir  16643  ismgm  16654  elsymgbas2  17183  mdetunilem9  19803  istopg  20083  isbasisg  20120  isptfin  20688  isufl  21086  isusp  21434  2sqlem9  24462  isplig  26070  isgrpo  26087  isass  26207  isexid  26208  ismgmOLD  26211  elghomlem2OLD  26253  elunop  27688  adjeu  27705  isarchi  28654  ispcmp  28839  eulerpartlemelr  29344  eulerpartlemgs2  29367  ballotlemfmpn  29481  ismfs  30339  dfon2lem3  30582  orderseqlem  30641  elno  30684  elaltxp  30893  heiborlem1  32380  heiborlem10  32389  gneispace2  36928  nzss  37023  elrnmptf  37814  issal  38619  isuhgr  39682  isushgr  39683  isupgr  39710  isumgr  39720  isuspgr  39782  isusgr  39783  iscplgr  40036  isconngr  40756  isconngr1  40757  isfrgr  40830  ismgmALT  41049