Theorem elab2g 2987

Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995.)

Hypotheses

Ref	Expression
elab2g.1	⊢ (x = A → (φ ↔ ψ))
elab2g.2	⊢ B = {x ∣ φ}

Assertion

Ref	Expression
elab2g	⊢ (A ∈ V → (A ∈ B ↔ ψ))

Distinct variable groups:   ψ,x   x,A

Allowed substitution hints:   φ(x)   B(x)   V(x)

Proof of Theorem elab2g

Step	Hyp	Ref	Expression
1		elab2g.2	. . 3 ⊢ B = {x ∣ φ}
2	1	eleq2i 2417	. 2 ⊢ (A ∈ B ↔ A ∈ {x ∣ φ})
3		elab2g.1	. . 3 ⊢ (x = A → (φ ↔ ψ))
4	3	elabg 2986	. 2 ⊢ (A ∈ V → (A ∈ {x ∣ φ} ↔ ψ))
5	2, 4	syl5bb 248	1 ⊢ (A ∈ V → (A ∈ B ↔ ψ))

Syntax hints:   → wi 4   ↔ wb 176   = wceq 1642   ∈ wcel 1710  {cab 2339

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-v 2861

This theorem is referenced by:  elab2  2988  elab4g  2989  elning  3217  elprg  3750  elsncg  3755  eluni  3894  eliun  3973  eliin  3974  el1c  4139  elxpk  4196  elimakg  4257  elp6  4263  eladdc  4398  evennn  4506  oddnn  4507  evennnul  4508  oddnnul  4509  sucevenodd  4510  sucoddeven  4511  eventfin  4517  oddtfin  4518  elopab  4696  elima  4754  opeliunxp  4820  elqsg  5976  elcan  6329  elscan  6330