Theorem elab2 1904

Description: Membership in a class abstraction, using implicit substitution.

Hypotheses

Ref	Expression
elab2.1	|- A e. V
elab2.2	|- (x = A -> (ph <-> ps))
elab2.3	|- B = {x | ph}

Assertion

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

Distinct variable groups:   ps,x   x,A

Proof of Theorem elab2

Step	Hyp	Ref	Expression
1		elab2.1	. 2 |- A e. V
2		elab2.2	. . 3 |- (x = A -> (ph <-> ps))
3		elab2.3	. . 3 |- B = {x | ph}
4	2, 3	elab2g 1903	. 2 |- (A e. V -> (A e. B <-> ps))
5	1, 4	ax-mp 7	1 |- (A e. B <-> ps)

Syntax hints:   -> wi 3   <-> wb 146   = wceq 958   e. wcel 960  {cab 1466  Vcvv 1814

This theorem is referenced by:  elint 2543  elom 3140  eldm 3313  elrn2 3355  elec 4285  elqs 4296  aceq3lem 4742  aceq5lem4 4748  kmlem9 4783  1pr 5129  ltexprlem3 5156  ltexprlem4 5157  reclem2pr 5169  suppsr 5234  suppsr3 5236  supsrlem4 5240  supre 5272  infcvgaux2 7220  infcvglem1 7221  infxpidmlem2 7554  minveclem10 8550  minveclem14 8554  efilcp 10556  fisub 10558

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-v 1815

Copyright terms: Public domain