Theorem elab2g 3667

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1533   ∈ wcel 2110  {cab 2799

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963

This theorem is referenced by:  elab2  3669  elab4g  3670  elrab  3679  eldif  3945  elun  4124  elin  4168  elpwg  4544  elsng  4574  elprg  4581  eluni  4834  elintg  4876  eliun  4915  eliin  4916  elopab  5406  elrn2g  5755  eldmg  5761  dmopabelb  5779  elrnmpt  5822  elrnmpt1  5824  elimag  5927  elong  6193  elrnmpog  7280  elrnmpores  7282  eloprabi  7755  tfrlem12  8019  elqsg  8342  elixp2  8459  isacn  9464  isfin1a  9708  isfin2  9710  isfin4  9713  isfin7  9717  isfin3ds  9745  elwina  10102  elina  10103  iswun  10120  eltskg  10166  elgrug  10208  elnp  10403  elnpi  10404  iscat  16937  isps  17806  isdir  17836  ismgm  17847  elefmndbas2  18033  elsymgbas2  18495  mdetunilem9  21223  istopg  21497  isbasisg  21549  isptfin  22118  isufl  22515  isusp  22864  2sqlem9  25997  isuhgr  26839  isushgr  26840  isupgr  26863  isumgr  26874  isuspgr  26931  isusgr  26932  cplgruvtxb  27189  isconngr  27962  isconngr1  27963  isplig  28247  isgrpo  28268  elunop  29643  adjeu  29660  isarchi  30806  ispcmp  31116  eulerpartlemelr  31610  eulerpartlemgs2  31633  ballotlemfmpn  31747  isacycgr  32387  isacycgr1  32388  ismfs  32791  dfon2lem3  33025  orderseqlem  33089  frrlem13  33130  elno  33148  elaltxp  33431  bj-ismoore  34391  heiborlem1  35083  heiborlem10  35092  isass  35118  isexid  35119  ismgmOLD  35122  elghomlem2OLD  35158  elcoeleqvrels  35824  eleldisjs  35955  gneispace2  40475  ismnu  40590  nzss  40642  elrnmptf  41434  issal  42593  ismea  42727  isome  42770  ismgmALT  44124  setrec1lem1  44784