Theorem rexbidv 1656

Description: Formula-building rule for restricted existential quantifier (deduction rule).

Hypothesis

Ref	Expression
ralbidv.1	|- (ph -> (ps <-> ch))

Assertion

Ref	Expression
rexbidv	|- (ph -> (E.x e. A ps <-> E.x e. A ch))

Distinct variable group:   ph,x

Proof of Theorem rexbidv

Step	Hyp	Ref	Expression
1		ax-17 968	. 2 |- (ph -> A.xph)
2		ralbidv.1	. 2 |- (ph -> (ps <-> ch))
3	1, 2	rexbid 1654	1 |- (ph -> (E.x e. A ps <-> E.x e. A ch))

Syntax hints:   -> wi 3   <-> wb 146  E.wrex 1638

This theorem is referenced by:  2rexbidv 1673  rexralbidv 1674  rexeqd 1784  rexeq12d 1787  rcla42ev 1872  ceqsrex2v 1881  uniiunlem 2122  eliun 2560  dfiun2g 2576  dfiin2 2578  iunrab 2586  iununi 2606  orduninsuc 3104  elimag 3391  funcnvuni 3550  fvelrnb 3745  fvelima 3749  abrexexlem2 3844  funiunfv 3851  abrexex2 3856  f1oiso 3889  f1oweALT 3891  tfrlem3 3898  tfrlem12 3907  rdgeq1 3919  rdgeq2 3920  elrnoprabg 4108  nneob 4239  qseq2 4273  elqs 4274  pssnn 4513  domfi 4516  unblem1 4517  unblem2 4518  unbnn2 4522  unifi 4532  fiint 4534  abfii3 4537  abfii4 4538  iunfi 4543  pwfi 4545  supmo 4550  suplub 4555  tz9.13 4635  aceq1 4701  aceq2 4703  aceq5lem3 4709  aceq5lem4 4710  aceq6a 4713  aceq6b 4714  kmlem9 4745  kmlem12 4748  kmlem14 4750  numth2 4757  numthcor 4758  zorn2lem7 4766  brdom3 4773  brdom7disj 4776  brdom6disj 4777  cardiun 4831  cflim 4881  prnmax 5071  genpv 5074  axrnegex 5255  axrrecex 5256  cnegext 5320  recext 5657  infm3 6001  infmsup 6015  nnunb 6017  arch 6018  xrsupsslem 6023  xrinfmsslem 6024  xrsupss 6025  xrinfmss 6026  xrub 6027  supxrre 6030  supxrunb1 6036  supxrunb2 6037  qbtwnxr 6217  fsequb 6455  limsupvalt 6461  creur 6673  creui 6674  revalt 6686  imvalt 6687  replimt 6692  cau3ir 6852  sumeq1 6920  dffsum 6936  clm0 7021  clm0nns 7023  clm4at 7028  caucvg3t 7104  dfisum 7127  infcvgaux2 7155  infcvglem1 7156  expcnv 7168  cncfval 7199  negfcncf 7204  reeff1olem2 7365  reeff1olem2OLD 7367  unbenlem 7447  basis2t 7557  eltg2t 7561  tg2t 7563  tgval3t 7567  tgss2t 7579  basgen2t 7581  subbas 7586  subbas2 7587  subtop 7588  fctop 7592  neival 7658  isnei 7659  isneip 7661  cnpval 7699  iscnp 7700  cnpimaex 7704  isopn 7799  opni 7804  opnin 7809  metcnp 7826  metcnp2 7827  metcnpi 7829  metcnpi2 7830  metcni 7833  metcnss 7837  cncfmet 7844  tgioo 7854  lmbrf 7868  cmscvg 7882  lmss 7888  iscms2lem5 7927  cncms 7932  bcth 7966  isgrp 7975  isgrpi 7976  grpidinvlem3 7984  grpideu 7987  grpidinv2 7994  isgrp2i 8011  ghgrpilem3 8072  ringid 8082  nvcni 8266  va1cnlem 8279  sm1cnilem 8281  nvcnpi4 8355  nmofval 8357  nmoval 8358  nmosetn0 8360  nmolb 8366  nmoubi 8367  nmlno0lem 8385  minveclem9 8484  minveclem10 8485  minveclem14 8489  minveclem24 8499  minvecex 8509  efghgrpilem 8634  efifolem3 8639  circgrp 8660  grothinf 8720  h2hcau 8788  h2hlm 8789  hcau 8972  hhcms 8993  chcompl 9036  hhsscms 9067  projlem8 9109  projlem10 9111  projlem13 9114  projlem15 9116  projlem17 9118  projlem29 9130  pjtheu 9150  pjvalt 9154  pjeq2t 9156  pjpj0 9170  shsumvalt 9192  h1de2ct 9395  elspansnt 9405  osumlem5 9499  nmopvalt 9699  elcnopt 9700  nmopsetn0 9709  nmfnvalt 9720  nmfnsetn0 9722  elcnfnt 9726  eigvecvalt 9739  nmoplbt 9748  nmopubt 9749  cnopct 9753  nmfnlbt 9764  nmfnleubt 9765  cnfnct 9770  eleigvect 9797  nmlnop0ALT 9835  nmopunt 9854  nmcopexlem1 9866  lnopcont 9879  nmcfnexlem1 9895  lnfncont 9906  branmfnt 9951  pjnmop 9986  cvbrt 10119  hatomict 10195  chrelat2t 10205  cdjreu 10264  cdj3lem2 10267  cayleythlem 10320  infi1 10347  fine 10348  abfi 10349  ficli 10368  hmeogrp 10425  subsp 10429  fipfil2 10439  fgsb 10444  filint2 10446  infi 10448  fgsb2 10449  cnfilca 10451  isfuna 10592  isfunb 10593

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-rex 1642

Copyright terms: Public domain