Theorem elab2g 3353

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

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1483   ∈ wcel 1990  {cab 2608

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202

This theorem is referenced by:  elab2  3354  elab4g  3355  eldif  3584  elun  3753  elin  3796  elsng  4191  elprg  4196  eluni  4439  elintg  4483  eliun  4524  eliin  4525  elopab  4983  elrn2g  5313  eldmg  5319  elrnmpt  5372  elrnmpt1  5374  elimag  5470  elong  5731  elrnmpt2g  6772  elrnmpt2res  6774  eloprabi  7232  tfrlem12  7485  elqsg  7798  elixp2  7912  isacn  8867  isfin1a  9114  isfin2  9116  isfin4  9119  isfin7  9123  isfin3ds  9151  elwina  9508  elina  9509  iswun  9526  eltskg  9572  elgrug  9614  elnp  9809  elnpi  9810  iscat  16333  isps  17202  isdir  17232  ismgm  17243  elsymgbas2  17801  mdetunilem9  20426  istopg  20700  isbasisg  20751  isptfin  21319  isufl  21717  isusp  22065  2sqlem9  25152  isuhgr  25955  isushgr  25956  isupgr  25979  isumgr  25990  isuspgr  26047  isusgr  26048  iscplgr  26310  isconngr  27049  isconngr1  27050  isfrgr  27122  isplig  27328  isgrpo  27351  elunop  28731  adjeu  28748  isarchi  29736  ispcmp  29924  eulerpartlemelr  30419  eulerpartlemgs2  30442  ballotlemfmpn  30556  ismfs  31446  dfon2lem3  31690  orderseqlem  31749  elno  31799  elaltxp  32082  bj-ismoore  33059  heiborlem1  33610  heiborlem10  33619  isass  33645  isexid  33646  ismgmOLD  33649  elghomlem2OLD  33685  gneispace2  38430  nzss  38516  elrnmptf  39367  issal  40534  isome  40708  ismgmALT  41859  setrec1lem1  42434