Theorem elab2g 3630

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ∈ wcel 2106  {cab 2714

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815

This theorem is referenced by:  elab2  3632  elab4g  3633  elrab  3643  eldif  3918  elin  3924  elun  4106  elpwg  4561  elsng  4598  elprg  4605  eluni  4866  elint  4911  elintg  4913  eliun  4956  eliin  4957  elopabw  5480  elxpi  5652  elrn2g  5842  eldmg  5850  dmopabelb  5868  elrnmpt  5907  elrnmpt1  5909  elimag  6013  elong  6321  elrnmpog  7483  elrnmpores  7485  eloprabi  7983  orderseqlem  8056  frrlem13  8196  tfrlem12  8302  elqsg  8640  fsetfocdm  8732  elixp2  8772  isacn  9913  isfin1a  10161  isfin2  10163  isfin4  10166  isfin7  10170  isfin3ds  10198  elwina  10555  elina  10556  iswun  10573  eltskg  10619  elgrug  10661  elnp  10856  elnpi  10857  iscat  17486  isps  18391  isdir  18421  ismgm  18432  elefmndbas2  18617  elsymgbas2  19084  mdetunilem9  21882  istopg  22157  isbasisg  22210  isptfin  22780  isufl  23177  isusp  23526  2sqlem9  26688  elno  26907  isuhgr  27788  isushgr  27789  isupgr  27812  isumgr  27823  isuspgr  27880  isusgr  27881  cplgruvtxb  28138  isconngr  28910  isconngr1  28911  isplig  29195  isgrpo  29216  elunop  30591  adjeu  30608  isarchi  31790  ispcmp  32172  eulerpartlemelr  32691  eulerpartlemgs2  32714  ballotlemfmpn  32828  isacycgr  33473  isacycgr1  33474  ismfs  33877  dfon2lem3  34111  elaltxp  34419  bj-ismoore  35435  heiborlem1  36129  heiborlem10  36138  isass  36164  isexid  36165  ismgmOLD  36168  elghomlem2OLD  36204  elcoeleqvrels  36917  eleldisjs  37050  gneispace2  42119  ismnu  42256  nzss  42312  elrnmptf  43101  issal  44247  ismea  44382  isome  44425  ismgmALT  45839  setrec1lem1  46814