Theorem elab2g 3341

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

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1480   ∈ wcel 1992  {cab 2612

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-v 3193

This theorem is referenced by:  elab2  3342  elab4g  3343  eldif  3570  elun  3736  elin  3779  elsng  4167  elprg  4172  eluni  4410  elintg  4453  eliun  4495  eliin  4496  elopab  4948  elrn2g  5278  eldmg  5284  elrnmpt  5336  elrnmpt1  5338  elimag  5433  elong  5693  elrnmpt2g  6726  elrnmpt2res  6728  eloprabi  7178  tfrlem12  7431  elqsg  7744  elixp2  7857  isacn  8812  isfin1a  9059  isfin2  9061  isfin4  9064  isfin7  9068  isfin3ds  9096  elwina  9453  elina  9454  iswun  9471  eltskg  9517  elgrug  9559  elnp  9754  elnpi  9755  iscat  16249  isps  17118  isdir  17148  ismgm  17159  elsymgbas2  17717  mdetunilem9  20340  istopg  20620  isbasisg  20657  isptfin  21224  isufl  21622  isusp  21970  2sqlem9  25047  isuhgr  25846  isushgr  25847  isupgr  25870  isumgr  25880  isuspgr  25935  isusgr  25936  iscplgr  26191  isconngr  26909  isconngr1  26910  isfrgr  26982  isplig  27176  isgrpo  27191  elunop  28571  adjeu  28588  isarchi  29513  ispcmp  29698  eulerpartlemelr  30192  eulerpartlemgs2  30215  ballotlemfmpn  30329  ismfs  31146  dfon2lem3  31379  orderseqlem  31438  elno  31488  elaltxp  31697  heiborlem1  33209  heiborlem10  33218  isass  33244  isexid  33245  ismgmOLD  33248  elghomlem2OLD  33284  gneispace2  37879  nzss  37965  elrnmptf  38808  issal  39809  isome  39983  ismgmALT  41101  setrec1lem1  41682