Theorem elab2g 3616

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   ∈ wcel 2111  {cab 2776

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938

This theorem is referenced by:  elab2  3618  elab4g  3619  elrab  3628  eliun  4885  eliin  4886  elopab  5379  elrn2g  5725  eldmg  5731  dmopabelb  5749  elrnmpt  5792  elrnmpt1  5794  elimag  5900  elrnmpog  7265  elrnmpores  7267  eloprabi  7743  tfrlem12  8008  elqsg  8331  elixp2  8448  isacn  9455  isfin1a  9703  isfin4  9708  isfin7  9712  isfin3ds  9740  elwina  10097  elina  10098  eltskg  10161  elgrug  10203  elnp  10398  iscat  16935  isps  17804  isdir  17834  ismgm  17845  elefmndbas2  18031  elsymgbas2  18493  mdetunilem9  21225  istopg  21500  isbasisg  21552  isptfin  22121  isufl  22518  isusp  22867  2sqlem9  26011  isuhgr  26853  isushgr  26854  isupgr  26877  isumgr  26888  isuspgr  26945  isusgr  26946  cplgruvtxb  27203  isconngr  27974  isconngr1  27975  isplig  28259  isgrpo  28280  elunop  29655  adjeu  29672  isarchi  30861  ispcmp  31210  eulerpartlemelr  31725  eulerpartlemgs2  31748  ballotlemfmpn  31862  isacycgr  32505  isacycgr1  32506  ismfs  32909  dfon2lem3  33143  orderseqlem  33207  frrlem13  33248  elno  33266  elaltxp  33549  bj-ismoore  34520  heiborlem1  35249  heiborlem10  35258  isass  35284  isexid  35285  ismgmOLD  35288  elghomlem2OLD  35324  elcoeleqvrels  35990  eleldisjs  36121  gneispace2  40835  ismnu  40969  nzss  41021  elrnmptf  41807  ismea  43090  isome  43133  ismgmALT  44483  setrec1lem1  45217