Theorem elab2 1898

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 1897	. 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 955   e. wcel 957  {cab 1462  Vcvv 1808

This theorem is referenced by:  elint 2535  elom 3130  eldm 3303  elrn2 3345  elec 4272  elqs 4283  aceq3lem 4715  aceq5lem4 4721  kmlem9 4756  1pr 5100  ltexprlem3 5127  ltexprlem4 5128  reclem2pr 5140  suppsr 5205  suppsr3 5207  supsrlem4 5211  supre 5243  infcvgaux2 7172  infcvglem1 7173  infxpidmlem2 7513  minveclem10 8513  minveclem14 8517  efilcp 10504  fisub 10506

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-sb 1171  df-clab 1463  df-cleq 1468  df-clel 1471  df-v 1809

Copyright terms: Public domain