Theorem elab2g 3624

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {cab 2715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812

This theorem is referenced by:  elab2  3626  elab4g  3627  elrab  3635  eldif  3900  elin  3906  elun  4094  elpwg  4545  elsng  4582  elprg  4591  eluni  4854  elint  4896  elintg  4898  eliun  4938  eliin  4939  elopabw  5472  elxpi  5644  elrn2g  5837  eldmg  5845  dmopabelb  5863  elrnmpt  5905  elrnmpt1  5907  elimag  6021  elong  6323  elrnmpog  7493  elrnmpores  7496  eloprabi  8007  orderseqlem  8098  frrlem13  8239  tfrlem12  8319  elqsg  8701  fsetfocdm  8799  elixp2  8840  isacn  9955  isfin1a  10203  isfin2  10205  isfin4  10208  isfin7  10212  isfin3ds  10240  elwina  10598  elina  10599  iswun  10616  eltskg  10662  elgrug  10704  elnp  10899  elnpi  10900  iscat  17627  isps  18523  isdir  18553  ismgm  18598  elefmndbas2  18831  elsymgbas2  19337  mdetunilem9  22594  istopg  22869  isbasisg  22921  isptfin  23490  isufl  23887  isusp  24235  2sqlem9  27409  elno  27628  elnoOLD  27629  elz12s  28483  isuhgr  29148  isushgr  29149  isupgr  29172  isumgr  29183  isuspgr  29240  isusgr  29241  cplgruvtxb  29501  isconngr  30279  isconngr1  30280  isplig  30567  isgrpo  30588  elunop  31963  adjeu  31980  isarchi  33263  ispcmp  34022  eulerpartlemelr  34522  eulerpartlemgs2  34545  ballotlemfmpn  34660  isacycgr  35348  isacycgr1  35349  ismfs  35752  dfon2lem3  35986  elaltxp  36178  elttcirr  36734  bj-ismoore  37430  heiborlem1  38143  heiborlem10  38152  isass  38178  isexid  38179  ismgmOLD  38182  elghomlem2OLD  38218  elcoeleqvrels  39011  eleldisjs  39160  gneispace2  44574  ismnu  44703  nzss  44759  elrnmptf  45626  issal  46757  ismea  46894  isome  46937  ismgmALT  48696  eloprab1st2nd  49340  setrec1lem1  50159