Theorem elab2g 3642

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1563   ∈ wcel 2145  {cab 2743

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840

This theorem is referenced by:  elab2  3644  elab4g  3645  elrab  3653  eldif  3917  elin  3923  elun  4109  elpwg  4561  elsng  4599  elprg  4608  eluni  4871  elintg  4916  eliun  4956  eliin  4957  elopabw  5501  elxpi  5674  elrn2g  5871  eldmg  5879  dmopabelb  5897  elrnmpt  5939  elrnmpt1  5941  elimag  6057  elong  6358  elrnmpog  7535  elrnmpores  7538  eloprabi  8048  orderseqlem  8141  frrlem13  8283  tfrlem12  8364  elqsg  8749  fsetfocdm  8846  elixp2  8887  isacn  10016  isfin1a  10264  isfin2  10266  isfin4  10269  isfin7  10273  isfin3ds  10301  elwina  10659  elina  10660  iswun  10677  eltskg  10723  elgrug  10765  elnp  10960  elnpi  10961  iscat  17718  isps  18614  isdir  18644  ismgm  18689  elefmndbas2  18923  elsymgbas2  19434  mdetunilem9  22738  istopg  23013  isbasisg  23065  isptfin  23634  isufl  24031  isusp  24379  2sqlem9  27549  elno  27768  elz12s  28623  isuhgr  29319  isushgr  29320  isupgr  29343  isumgr  29354  isuspgr  29411  isusgr  29412  cplgruvtxb  29672  isconngr  30449  isconngr1  30450  isplig  30737  isgrpo  30758  elunop  32133  adjeu  32150  isarchi  33415  ispcmp  34164  eulerpartlemelr  34664  eulerpartlemgs2  34687  ballotlemfmpn  34802  isacycgr  35508  isacycgr1  35509  ismfs  35912  dfon2lem3  36146  elaltxp  36338  elttcirr  36904  bj-ismoore  37607  heiborlem1  38322  heiborlem10  38331  isass  38357  isexid  38358  ismgmOLD  38361  elghomlem2OLD  38397  elcoeleqvrels  39190  eleldisjs  39339  gneispace2  44720  ismnu  44835  nzss  44891  elrnmptf  45757  issal  46886  ismea  47023  isome  47066  ismgmALT  48843  eloprab1st2nd  49497  setrec1lem1  50316