Theorem elab2g 2988

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

Hypotheses

Ref	Expression
elab2g.1	|- (x = A -> (ph <-> ps))
elab2g.2	|- B = {x | ph}

Assertion

Ref	Expression
elab2g	|- (A e. V -> (A e. B <-> ps))

Distinct variable groups:   ps,x   x,A

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

Proof of Theorem elab2g

Step	Hyp	Ref	Expression
1		elab2g.2	. . 3 |- B = {x | ph}
2	1	eleq2i 2417	. 2 |- (A e. B <-> A e. {x | ph})
3		elab2g.1	. . 3 |- (x = A -> (ph <-> ps))
4	3	elabg 2987	. 2 |- (A e. V -> (A e. {x | ph} <-> ps))
5	2, 4	syl5bb 248	1 |- (A e. V -> (A e. B <-> ps))

Syntax hints:   -> wi 4   <-> wb 176   = wceq 1642   e. 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 2479  df-v 2862

This theorem is referenced by:  elab2  2989  elab4g  2990  elning  3218  elprg  3751  elsncg  3756  eluni  3895  eliun  3974  eliin  3975  el1c  4140  elxpk  4197  elimakg  4258  elp6  4264  eladdc  4399  evennn  4507  oddnn  4508  evennnul  4509  oddnnul  4510  sucevenodd  4511  sucoddeven  4512  eventfin  4518  oddtfin  4519  elopab  4697  elima  4755  opeliunxp  4821  elqsg  5977  elcan  6330  elscan  6331