Theorem rexbidv 1664

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 971	. 2 |- (ph -> A.xph)
2		ralbidv.1	. 2 |- (ph -> (ps <-> ch))
3	1, 2	rexbid 1662	1 |- (ph -> (E.x e. A ps <-> E.x e. A ch))

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

This theorem is referenced by:  2rexbidv 1681  rexralbidv 1682  rexeqd 1792  rexeq12d 1795  rcla42ev 1881  ceqsrex2v 1890  uniiunlem 2132  eliun 2570  dfiun2g 2586  dfiin2 2588  iunrab 2596  iununi 2616  orduninsuc 3114  elimag 3407  funcnvuni 3564  fvelrnb 3760  fvelima 3764  abrexexlem2 3859  funiunfv 3866  abrexex2 3871  f1oiso 3904  f1oweALT 3906  tfrlem3 3913  tfrlem12 3922  rdgeq1 3934  rdgeq2 3935  elrnoprabg 4124  nneob 4255  qseq2 4289  elqs 4290  isfi 4382  pssnn 4534  domfiOLD 4539  unblem1 4540  unblem2 4541  unbnn2 4545  unifiOLD 4557  fiintOLD 4560  abfii3OLD 4563  abfii4OLD 4564  iunfiOLD 4569  pwfiOLD 4571  supmo 4576  suplub 4581  tz9.13 4663  aceq1 4729  aceq2 4731  aceq5lem3 4737  aceq5lem4 4738  aceq6a 4741  aceq6b 4742  kmlem9 4773  kmlem12 4776  kmlem14 4778  numth2 4785  numthcor 4786  zorn2lem7 4794  brdom3 4801  brdom7disj 4804  brdom6disj 4805  cardiun 4859  cflim 4909  prnmax 5099  genpv 5102  axrnegex 5283  axrrecex 5284  cnegext 5348  recext 5684  infm3 6054  infmsup 6068  nnunb 6070  arch 6071  xrsupsslem 6076  xrinfmsslem 6077  xrsupss 6078  xrinfmss 6079  xrub 6080  supxrre 6083  supxrunb1 6089  supxrunb2 6090  qbtwnxr 6279  fsequb 6523  limsupvalt 6529  creur 6742  creui 6743  revalt 6755  imvalt 6756  replimt 6761  cau3ir 6915  sumeq1 6982  dffsum 6998  clm0 7083  clm0nns 7085  clm4at 7090  climabs0 7113  caucvg3t 7168  dfisum 7191  infcvgaux2 7220  infcvglem1 7221  expcnv 7233  cncfval 7264  negfcncf 7269  reeff1olem2 7425  unbenlem 7504  basis2t 7615  eltg2t 7619  tg2t 7621  tgval3t 7625  tgss2t 7637  basgen2t 7639  subbasOLD 7644  subbas2OLD 7645  subtop 7646  fctopOLD 7650  neival 7717  isnei 7718  isneip 7720  cnpval 7759  iscnp 7760  cnpimaex 7765  isopn 7859  opni 7864  opnin 7869  metcnp 7887  metcnp2 7888  metcnpi 7890  metcnpi2 7891  metcni 7894  metcnss 7898  cncfmet 7905  tgioo 7915  lmbrf 7930  cmscvg 7947  lmss 7953  iscms2lem5 7993  cncms 7998  bcth 8032  isgrp 8041  isgrpi 8042  grpidinvlem3 8050  grpideu 8053  grpidinv2 8060  isgrp2i 8076  ghgrpilem3 8135  ringid 8145  nvcni 8329  nvcni2 8330  nvcni3 8331  va1cnlem 8345  sm1cnilem 8347  nvcnpi3 8422  nvcnpi4 8423  nmofval 8425  nmoval 8426  nmosetn0 8428  nmolb 8434  nmoubi 8435  nmlno0lem 8453  minveclem9 8553  minveclem10 8554  minveclem14 8558  minveclem24 8568  minvecex 8578  spwpr4OLD 8663  spwpr4aOLD 8664  efghgrpilem 8719  efifolem3 8724  circgrp 8740  grothinf 8781  h2hcau 8849  h2hlm 8850  hcau 9051  hhcms 9072  chcompl 9115  hhsscms 9150  projlem8 9193  projlem10 9195  projlem13 9198  projlem15 9200  projlem17 9202  projlem29 9214  pjtheu 9235  pjvalt 9239  pjeq2t 9241  pjpj0 9255  shsumvalt 9277  h1de2ct 9479  elspansnt 9489  osumlem5 9582  nmopvalt 9782  elcnopt 9783  nmopsetn0 9792  nmfnvalt 9803  nmfnsetn0 9805  elcnfnt 9809  eigvecvalt 9822  nmoplbt 9831  nmopubt 9832  cnopct 9837  nmfnlbt 9848  nmfnleubt 9849  cnfnct 9854  eleigvect 9881  nmlnop0ALT 9920  nmopunt 9939  nmcopexlem1 9951  lnopcont 9964  nmcfnexlem1 9980  lnfncont 9991  branmfnt 10038  pjnmop 10075  cvbrt 10209  hatomict 10287  chrelat2t 10297  cdjreu 10359  cdj3lem2 10362  cayleythlem 10413  infi1OLD 10448  fineOLD 10450  abfiOLD 10452  ficliOLD 10473  hmeogrp 10538  subsp 10554  fipfil2OLD 10565  fgsb 10570  fgsbOLD 10571  filint2OLD 10575  infiOLD 10579  fgsb2 10580  cnfilca 10583  cnfilcaOLD 10584  rcfpfillem2OLD 10588  rcfpfillem3OLD 10590  rcfpfillem4OLD 10592  rcfpfillem5OLD 10594  rcfpfillem6OLD 10596  isfuna 10754  isfunb 10755

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-rex 1650

Copyright terms: Public domain