Theorem elab2g 3682

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1536   ∈ wcel 2105  {cab 2711

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813

This theorem is referenced by:  elab2  3684  elab4g  3685  elrab  3694  eldif  3972  elin  3978  elun  4162  elpwg  4607  elsng  4644  elprg  4652  eluni  4914  elint  4956  elintg  4958  eliun  4999  eliin  5000  elopabw  5535  elxpi  5710  elrn2g  5903  eldmg  5911  dmopabelb  5929  elrnmpt  5971  elrnmpt1  5973  elimag  6083  elong  6393  elrnmpog  7567  elrnmpores  7570  eloprabi  8086  orderseqlem  8180  frrlem13  8321  tfrlem12  8427  elqsg  8806  fsetfocdm  8899  elixp2  8939  isacn  10081  isfin1a  10329  isfin2  10331  isfin4  10334  isfin7  10338  isfin3ds  10366  elwina  10723  elina  10724  iswun  10741  eltskg  10787  elgrug  10829  elnp  11024  elnpi  11025  iscat  17716  isps  18625  isdir  18655  ismgm  18666  elefmndbas2  18899  elsymgbas2  19404  mdetunilem9  22641  istopg  22916  isbasisg  22969  isptfin  23539  isufl  23936  isusp  24285  2sqlem9  27485  elno  27704  elnoOLD  27705  elzs12  28435  isuhgr  29091  isushgr  29092  isupgr  29115  isumgr  29126  isuspgr  29183  isusgr  29184  cplgruvtxb  29444  isconngr  30217  isconngr1  30218  isplig  30504  isgrpo  30525  elunop  31900  adjeu  31917  isarchi  33171  ispcmp  33817  eulerpartlemelr  34338  eulerpartlemgs2  34361  ballotlemfmpn  34475  isacycgr  35129  isacycgr1  35130  ismfs  35533  dfon2lem3  35766  elaltxp  35956  bj-ismoore  37087  heiborlem1  37797  heiborlem10  37806  isass  37832  isexid  37833  ismgmOLD  37836  elghomlem2OLD  37872  elcoeleqvrels  38576  eleldisjs  38709  gneispace2  44121  ismnu  44256  nzss  44312  elrnmptf  45123  issal  46269  ismea  46406  isome  46449  ismgmALT  48066  setrec1lem1  48917