Theorem elab 1897

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 groups:   ps,x   x,A

Proof of Theorem elab

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

Syntax hints:   -> wi 3   <-> wb 146   = wceq 956   e. wcel 958  {cab 1463  Vcvv 1811

This theorem is referenced by:  dfiun2g 2586  dfiin2 2588  brab1 2660  uniuni 2880  dffr2 2919  frirr 2924  onminex 3020  finds 3156  finds2 3158  funcnvuni 3564  tz6.12-2 3739  tfrlem3 3913  mapval2 4335  sbthlem2 4448  ssenen 4504  abfii3OLD 4563  abfii4OLD 4564  tz9.13 4663  kardex 4725  karden 4726  aceq3 4733  aceq5lem3 4737  aceq5lem4 4738  aceq6b 4742  kmlem12 4776  brdom7disj 4804  brdom6disj 4805  cardiun 4859  alephval3 4903  cardcf 4911  cfeq0 4914  cfsuc 4915  genpelv 5103  genpprecl 5104  genpnnp 5108  peano5nn 5926  peano5uz 6203  infcvgaux1 7219  subbasOLD 7644  subbas2OLD 7645  subtop 7646  fctopOLD 7650  cctop 7652  nvvcop 8213  nmosetn0 8428  nmolb 8434  nmoubi 8435  nmlno0lem 8453  circgrp 8740  nmopsetn0 9792  nmfnsetn0 9805  nmoplbt 9831  nmopubt 9832  nmfnlbt 9848  nmfnleubt 9849  nmlnop0ALT 9920  nmopunt 9939  nmcopexlem1 9951  nmcfnexlem1 9980  branmfnt 10038  pjnmop 10075  pjhmopidm 10110  elo 10444  qusp 10555  rcfpfillem6 10595  rcfpfillem6OLD 10596  rcfpfil 10597  rcfpfilOLD 10598

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812

Copyright terms: Public domain