Theorem elab2g 3502

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

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1630   ∈ wcel 2144  {cab 2756

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-v 3351

This theorem is referenced by:  elab2  3503  elab4g  3504  eldif  3731  elun  3902  elin  3945  elsng  4328  elprg  4334  eluni  4575  elintg  4617  eliun  4656  eliin  4657  elopab  5116  elrn2g  5451  eldmg  5457  elrnmpt  5510  elrnmpt1  5512  elimag  5611  elong  5874  elrnmpt2g  6918  elrnmpt2res  6920  eloprabi  7381  tfrlem12  7637  elqsg  7949  elixp2  8065  isacn  9066  isfin1a  9315  isfin2  9317  isfin4  9320  isfin7  9324  isfin3ds  9352  elwina  9709  elina  9710  iswun  9727  eltskg  9773  elgrug  9815  elnp  10010  elnpi  10011  iscat  16539  isps  17409  isdir  17439  ismgm  17450  elsymgbas2  18007  mdetunilem9  20643  istopg  20919  isbasisg  20971  isptfin  21539  isufl  21936  isusp  22284  2sqlem9  25372  isuhgr  26175  isushgr  26176  isupgr  26199  isumgr  26210  isuspgr  26268  isusgr  26269  cplgruvtxb  26542  isconngr  27366  isconngr1  27367  isfrgr  27437  isplig  27664  isgrpo  27685  elunop  29065  adjeu  29082  isarchi  30070  ispcmp  30258  eulerpartlemelr  30753  eulerpartlemgs2  30776  ballotlemfmpn  30890  ismfs  31778  dfon2lem3  32020  orderseqlem  32083  elno  32130  elaltxp  32413  bj-ismoore  33384  heiborlem1  33935  heiborlem10  33944  isass  33970  isexid  33971  ismgmOLD  33974  elghomlem2OLD  34010  gneispace2  38949  nzss  39035  elrnmptf  39881  issal  41045  isome  41222  ismgmALT  42377  setrec1lem1  42952