Theorem elab 2403

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 1317	. 2 |- (ps -> A.xps)
2		elab.1	. 2 |- A e. _V
3		elab.2	. 2 |- (x = A -> (ph <-> ps))
4	1, 2, 3	elabf 2402	1 |- (A e. {x | ph} <-> ps)

Syntax hints:   -> wi 3   <-> wb 163   = wceq 1298   e. wcel 1300  {cab 1871  _Vcvv 2292

This theorem is referenced by:  ralab 2417  dfiun2gOLD 3284  dfiin2g 3286  dfiin2OLD 3288  brab1OLD 3385  dffr2OLD 3628  frirr 3634  uniuni 3806  onminex 3888  finds 3979  finds2 3981  funcnvuni 4482  tz6.12-2 4696  onopriun 5118  tfrlem3 5121  mapval2 5394  sbthlem2 5511  ssenen 5598  abfii3 5653  abfii4 5654  tz9.13 5774  kardex 5855  karden 5856  omsublim 5887  aceq3 5895  aceq5lem3 5899  aceq5lem4 5900  aceq6b 5904  kmlem12 5938  brdom7disj 5966  brdom6disj 5967  cardiun 6011  alephval3 6051  cardcf 6059  cfeq0 6062  cfsuc 6063  genpelv 6255  genpprecl 6256  genpnnp 6260  peano5nni 7109  peano5uzi 7415  infcvgaux1i 8480  subbas 8914  subbas2 8915  subtop 8916  fctop 8920  cctop 8922  txbas 8933  txuni 8935  nvvcop 9545  nmosetn0 9767  nmolb 9773  nmoubi 9774  nmlno0lem 9793  circgrp 10094  uptx 10226  fbunfip 10282  filrn 10293  filmapss 10309  elfilmap 10312  cncomp 10331  nmopsetn0 11429  nmfnsetn0 11442  nmoplb 11468  nmopub 11469  nmfnlb 11485  nmfnleub 11486  nmlnop0iALT 11557  nmopun 11576  nmcopexlem1 11588  nmcfnexlem1 11617  branmfn 11675  branmfnOLD 11676  pjnmopi 11719  pjhmopidm 11754  bnj64 13201  dfon2lem3 13851  dfon2lem7 13855  axfelem15 14045  axfelem16 14046  elo 14342  prj1 14395  valcurfn 14551  curgrpact 14735  qusp 14908  rcfpfillem6 14933  rcfpfil 14934  bpmp 15251  dfiin2gOLD 15356  fictblem 15370  fictb 15371  omsublimOLD 15396  compsublem 15430  compsub 15431  hscptsscld 15434  compfipin0 15436  comppfsc 15517  neibastop1 15518  neibastop2lem3 15521  neibastop2lem4 15522  neibastop2 15523  neibastop3 15524  fnemeet1 15528  fnemeet2 15529  fnejoin1 15530  fnejoin2 15531  fbasfip 15556  supfil 15560  ufinffr 15578  ufilen 15579  cnpfillim 15589  rnelfmlem 15592  rnelfm 15593  fmfnfmlem3 15596  fmfnfmlem4 15597  fmfnfm 15598  fcluscf 15612  flimfnfcls 15615  fcluscnplem 15617  fcluscomplem 15620  fclusff 15623  filnetlem1 15640  ralabOLD 15669  sdc 15811  txsubsp 15912  txmet 15925  sstotbnd 15936  heiborlem1 15955  rrntotbndlem1 16020  rrntotbnd 16022  glbconx 17029  pmapglbx 17251

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-v 2294

Copyright terms: Public domain