Theorem rexbidv 1667

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

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

This theorem is referenced by:  2rexbidv 1684  rexralbidv 1685  rexeqd 1795  rexeq12d 1798  rcla42ev 1884  ceqsrex2v 1893  uniiunlem 2135  eliun 2574  dfiun2g 2590  dfiin2 2592  iunrab 2600  iununi 2621  orduninsuc 3120  elimag 3413  funcnvuni 3570  fvelrnb 3766  fvelima 3770  abrexexlem2 3865  funiunfv 3872  abrexex2 3877  f1oiso 3910  f1oweALT 3912  tfrlem3 3919  tfrlem12 3928  rdgeq1 3940  rdgeq2 3941  elrnoprabg 4130  nneob 4261  qseq2 4295  elqs 4296  isfi 4388  enfi 4543  pssnn 4544  domfiOLD 4550  unblem1 4551  unblem2 4552  unbnn2 4556  unifiOLD 4570  fiintOLD 4573  pwfiOLD 4580  supmo 4585  suplub 4590  tz9.13 4673  aceq1 4739  aceq2 4741  aceq5lem3 4747  aceq5lem4 4748  aceq6a 4751  aceq6b 4752  kmlem9 4783  kmlem12 4786  kmlem14 4788  numth2 4795  numthcor 4796  zorn2lem7 4804  brdom3 4811  brdom7disj 4814  brdom6disj 4815  cardiun 4870  cflim 4921  prnmax 5111  genpv 5114  axrnegex 5295  axrrecex 5296  cnegext 5360  recext 5696  infm3 6056  infmsup 6070  nnunb 6072  arch 6073  xrsupsslem 6078  xrinfmsslem 6079  xrsupss 6080  xrinfmss 6081  xrub 6082  supxrre 6085  supxrunb1 6091  supxrunb2 6092  qbtwnxr 6280  fsequb 6524  limsupvalt 6530  creur 6743  creui 6744  revalt 6756  imvalt 6757  replimt 6762  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 7505  basis2t 7614  eltg2t 7618  tg2t 7620  tgval3t 7624  tgss2t 7636  basgen2t 7638  subtop 7643  fctopOLD 7647  neival 7714  isnei 7715  isneip 7717  cnpval 7756  iscnp 7757  cnpimaex 7762  isopn 7856  opni 7861  opnin 7866  metcnp 7884  metcnp2 7885  metcnpi 7887  metcnpi2 7888  metcni 7891  metcnss 7895  cncfmet 7902  tgioo 7912  lmbrf 7927  cmscvg 7944  lmss 7950  iscms2lem5 7990  cncms 7995  bcth 8029  isgrp 8038  isgrpi 8039  grpidinvlem3 8047  grpideu 8050  grpidinv2 8056  isgrp2i 8072  ghgrpilem3 8131  ringid 8141  nvcni 8325  nvcni2 8326  nvcni3 8327  va1cnlem 8341  sm1cnilem 8343  nvcnpi3 8418  nvcnpi4 8419  nmofval 8421  nmoval 8422  nmosetn0 8424  nmolb 8430  nmoubi 8431  nmlno0lem 8449  minveclem9 8549  minveclem10 8550  minveclem14 8554  minveclem24 8564  minvecex 8574  spwpr4OLD 8658  spwpr4aOLD 8659  efghgrpilem 8714  efifolem3 8719  circgrp 8735  grothinf 8776  h2hcau 8844  h2hlm 8845  hcau 9046  hhcms 9067  chcompl 9110  hhsscms 9145  projlem8 9188  projlem10 9190  projlem13 9193  projlem15 9195  projlem17 9197  projlem29 9209  pjtheu 9230  pjvalt 9234  pjeq2t 9236  pjpj0 9250  shsumvalt 9272  h1de2ct 9474  elspansnt 9484  osumlem5 9577  nmopvalt 9777  elcnopt 9778  nmopsetn0 9787  nmfnvalt 9798  nmfnsetn0 9800  elcnfnt 9804  eigvecvalt 9817  nmoplbt 9826  nmopubt 9827  cnopct 9832  nmfnlbt 9843  nmfnleubt 9844  cnfnct 9849  eleigvect 9876  nmlnop0ALT 9915  nmopunt 9934  nmcopexlem1 9946  lnopcont 9959  nmcfnexlem1 9975  lnfncont 9986  branmfnt 10033  pjnmop 10070  cvbrt 10204  hatomict 10282  chrelat2t 10292  cdjreu 10354  cdj3lem2 10357  cayleythlem 10408  hmeogrp 10524  subsp 10540  fgsb 10555  fgsb2 10560  cnfilca 10562  isfuna 10725  isfunb 10726

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

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-rex 1653

Copyright terms: Public domain