Theorem elab 1415

Description: Membership in a class abstraction with implicit substitution. Compare Theorem 6.13 of [Quine] p. 44.

Hypotheses

Ref	Expression
elab.1	|- A e. V
elab.2	|- (x = A -> (ph <-> ps))

Assertion

Ref	Expression
elab	|- (A e. {x | ph} <-> ps)

Distinct variable group(s):   ps,x   x,A

Proof of Theorem elab

Step	Hyp	Ref	Expression
1		ax-17 925	. 2 |- (ps -> A.xps)
2		elab.1	. 2 |- A e. V
3		elab.2	. 2 |- (x = A -> (ph <-> ps))
4	1, 2, 3	elabf 1414	1 |- (A e. {x | ph} <-> ps)

Syntax hints:   -> wi 2   <-> wb 127  {cab 1090   = wceq 1091   e. wcel 1092  Vcvv 1348

This theorem is referenced by:  dfiun2 2014  dfiin2 2015  brab1 2096  dffr2 2171  frirr 2176  onminex 2275  finds 2397  finds2 2399  funcnvuni 2706  tz6.12-2 2845  tfrlem3 2951  sbthlem2 3350  ssenen 3399  tz9.13 3507  kardex 3550  karden 3551  aceq3 3556  aceq5lem3 3560  aceq5lem4 3561  aceq6b 3565  kmlem11 3590  cardiun 3665  cardcf 3706  cfsuc 3709  genpelv 3897  genpprecl 3898  genpnnp 3902  peano5nn 4424  nnind 4434  hosmvalt 5487  hodmvalt 5488

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349

metamath.org