Theorem elab2g 3576

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812

This theorem is referenced by:  elab2  3578  elab4g  3579  elrab  3589  eldif  3854  elin  3860  elun  4040  elpwg  4492  elsng  4531  elprg  4538  dfopif  4756  eluni  4800  elint  4843  elintg  4845  eliun  4886  eliin  4887  elopab  5383  elxpi  5548  elrn2g  5734  eldmg  5742  dmopabelb  5760  elrnmpt  5800  elrnmpt1  5802  elimag  5908  elong  6181  elrnmpog  7304  elrnmpores  7306  eloprabi  7789  tfrlem12  8057  elqsg  8382  fsetfocdm  8474  elixp2  8514  isacn  9547  isfin1a  9795  isfin2  9797  isfin4  9800  isfin7  9804  isfin3ds  9832  elwina  10189  elina  10190  iswun  10207  eltskg  10253  elgrug  10295  elnp  10490  elnpi  10491  iscat  17049  isps  17931  isdir  17961  ismgm  17972  elefmndbas2  18158  elsymgbas2  18622  mdetunilem9  21374  istopg  21649  isbasisg  21701  isptfin  22270  isufl  22667  isusp  23016  2sqlem9  26166  isuhgr  27008  isushgr  27009  isupgr  27032  isumgr  27043  isuspgr  27100  isusgr  27101  cplgruvtxb  27358  isconngr  28129  isconngr1  28130  isplig  28414  isgrpo  28435  elunop  29810  adjeu  29827  isarchi  31016  ispcmp  31382  eulerpartlemelr  31897  eulerpartlemgs2  31920  ballotlemfmpn  32034  isacycgr  32681  isacycgr1  32682  ismfs  33085  dfon2lem3  33338  orderseqlem  33417  frrlem13  33458  elno  33495  elaltxp  33923  bj-ismoore  34920  heiborlem1  35615  heiborlem10  35624  isass  35650  isexid  35651  ismgmOLD  35654  elghomlem2OLD  35690  elcoeleqvrels  36354  eleldisjs  36485  gneispace2  41311  ismnu  41444  nzss  41496  elrnmptf  42279  issal  43420  ismea  43554  isome  43597  ismgmALT  44981  setrec1lem1  45876