Theorem elab 1943

Description: Membership in a class abstraction, using implicit substitition. 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 1007	. 2 |- (ps -> A.xps)
2		elab.1	. 2 |- A e. V
3		elab.2	. 2 |- (x = A -> (ph <-> ps))
4	1, 2, 3	elabf 1942	1 |- (A e. {x | ph} <-> ps)

Syntax hints:   -> wi 3   <-> wb 144   = wceq 992   e. wcel 994  {cab 1505  Vcvv 1857

This theorem is referenced by:  dfiun2g 2654  dfiin2 2656  brab1 2733  dffr2 2949  frirr 2954  uniuni 3104  onminex 3164  finds 3244  finds2 3246  funcnvuni 3669  tz6.12-2 3850  onopriun 4211  tfrlem3 4214  mapval2 4476  sbthlem2 4593  ssenen 4651  abfii3 4706  abfii4 4707  tz9.13 4809  kardex 4871  karden 4872  aceq3 4879  aceq5lem3 4883  aceq5lem4 4884  aceq6b 4888  kmlem12 4922  brdom7disj 4950  brdom6disj 4951  cardiun 5009  alephval3 5053  cardcf 5061  cfeq0 5064  cfsuc 5065  genpelv 5257  genpprecl 5258  genpnnp 5262  peano5nni 6071  peano5uzi 6374  infcvgaux1i 7423  subbas 7856  subbas2 7857  subtop 7858  cctop 7862  nvvcop 8460  nmosetn0 8682  nmolb 8688  nmoubi 8689  nmlno0lem 8708  circgrp 9012  nmopsetn0 10072  nmfnsetn0 10085  nmoplb 10111  nmopub 10112  nmfnlb 10128  nmfnleub 10129  nmlnop0iALT 10199  nmopun 10218  nmcopexlem1 10230  nmcfnexlem1 10259  branmfn 10317  branmfnOLD 10318  pjnmopi 10355  pjhmopidm 10390  elo 10733  prj1 10809  qusp 11068  rcfpfillem6 11094  rcfpfil 11095  dfiin2g 11400  fictblem 11422  fictb 11423  omsublim 11448  compsublem 11487  compsub 11488  hscptsscld 11491  compfipin0 11493  cncomp 11494  comppfsc 11578  neibastop1 11579  neibastop2lem3 11582  neibastop2lem4 11583  neibastop2 11584  neibastop3 11585  fnemeet1 11589  fnemeet2 11590  fnejoin1 11591  fnejoin2 11592  fbasfip 11627  fbunfip 11631  filrn 11643  supfil 11645  ufinffr 11663  ufilen 11664  cnpfillim 11686  elfilmap 11690  filmapss 11696  rnelfmlem 11698  rnelfm 11699  fmfnfmlem3 11702  fmfnfmlem4 11703  fmfnfm 11704  fcluscf 11724  flimfnfcls 11727  fcluscnplem 11729  fcluscomplem 11732  fclusff 11735  filnetlem1 11763  sdc 11877  metsstop 11909  txbas 11973  txuni 11975  uptx 11978  txsubsp 11983  sstotbnd 11992  heiborlem1 12011  rrntotbndlem1 12076  rrntotbnd 12078

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-v 1858

Copyright terms: Public domain