Theorem rexbidv 1711

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

Syntax hints:   -> wi 3   <-> wb 153  E.wrex 1693

This theorem is referenced by:  2rexbidv 1728  rexralbidv 1729  rexeqd 1839  rexeq12d 1842  rcla42ev 1928  ceqsrex2v 1937  uniiunlem 2183  eliun 2624  dfiun2g 2640  dfiin2 2642  iunrab 2650  iununi 2671  orduninsuc 3171  elimag 3464  funcnvuni 3621  fvelrnb 3817  fvelima 3821  abrexexlem2 3916  funiunfv 3923  abrexex2 3928  f1oiso 3962  f1oweALT 3964  tfrlem3 3971  tfrlem12 3980  rdgeq1 3992  rdgeq2 3993  elrnoprabg 4182  nneob 4313  qseq2 4347  elqs 4348  elqsOLD 4349  elqsi 4350  isfi 4443  enfi 4598  pssnn 4599  unblem1 4603  unblem2 4604  unbnn2 4608  supmo 4636  suplub 4641  tz9.13 4725  aceq1 4791  aceq2 4793  aceq5lem3 4799  aceq5lem4 4800  aceq6a 4803  aceq6b 4804  kmlem9 4835  kmlem12 4838  kmlem14 4840  numth2 4847  numthcor 4848  zorn2lem7 4856  brdom3 4863  brdom7disj 4866  brdom6disj 4867  cardiun 4924  cflim 4974  prnmax 5164  genpv 5167  axrnegex 5348  axrrecex 5349  cnegex 5413  recex 5749  infm3 6136  infmsup 6150  nnunb 6152  arch 6153  xrsupsslem 6158  xrinfmsslem 6159  xrsupss 6160  xrinfmss 6161  xrub 6162  supxrre 6165  supxrunb1 6171  supxrunb2 6172  qbtwnxr 6332  fsequb 6549  limsupval 6618  creur 6832  creui 6833  reval 6845  imval 6846  replim 6851  cau3iri 7005  sumeq1 7072  dffsum 7088  clm0i 7173  clm0nnsi 7175  clm4a 7180  climabs0i 7203  caucvg3 7258  dfisum 7281  infcvgaux2i 7310  infcvglem1 7311  expcnv 7323  cncfval 7354  negfcncfi 7359  reeff1olem2 7516  unbenlem 7596  basis2 7704  eltg2 7708  tg2 7710  tgval3 7714  tgss2 7726  basgen2 7728  subtop 7733  neival 7802  isnei 7803  isneip 7805  cnpval 7844  iscnp 7845  cnpimaex 7850  isopn 7944  opni 7949  opnin 7954  metcnp 7972  metcnp2 7973  metcnpi 7975  metcnpi2 7976  metcni 7979  metcnss 7983  cncfmet 7990  tgioo 8000  lmbrf 8015  cmscvg 8032  lmss 8038  iscms2lem5 8078  cncms 8083  bcth 8117  isgrp 8126  isgrpi 8127  grpidinvlem3 8135  grpideu 8138  grpidinv2 8144  isgrp2i 8160  ghgrpilem3 8219  ringid 8229  nvcni 8413  nvcni2 8414  nvcni3 8415  va1cnlem 8429  sm1cnilem 8431  nvcnpi3 8506  nvcnpi4 8507  nmofval 8509  nmoval 8510  nmosetn0 8512  nmolb 8518  nmoubi 8519  nmlno0lem 8537  minveclem9 8637  minveclem10 8638  minveclem14 8642  minveclem24 8652  minvecex 8662  spwpr4OLD 8746  spwpr4aOLD 8747  efghgrpilem 8802  efifolem3 8807  circgrp 8823  grothinf 8864  h2hcau 8932  h2hlm 8933  hcau 9134  hhcms 9155  chcompl 9198  hhsscms 9233  projlem8 9276  projlem10 9278  projlem13 9281  projlem15 9283  projlem17 9285  projlem29 9297  pjtheui 9318  pjval 9322  pjeq2 9324  pjpj0i 9338  shsumval 9360  h1de2ci 9562  elspansn 9572  osumlem5 9665  nmopval 9865  elcnop 9866  nmopsetn0 9875  nmfnval 9886  nmfnsetn0 9888  elcnfn 9892  eigvecval 9905  nmoplb 9914  nmopub 9915  cnopc 9920  nmfnlb 9931  nmfnleub 9932  cnfnc 9937  eleigvec 9964  nmlnop0iALT 10003  nmopun 10022  nmcopexlem1 10034  lnopcon 10047  nmcfnexlem1 10063  lnfncon 10074  branmfn 10121  pjnmopi 10158  cvbr 10293  hatomic 10371  chrelat2 10381  cdjreui 10443  cdj3lem2 10446  cayleythlem 10498  hmeogrp 10632  subsp 10648  fgsb 10663  fgsb2 10668  cnfilca 10670  isfuna 10838  isfunb 10839

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1004  ax-17 1012  ax-4 1014  ax-5o 1016

This theorem depends on definitions:  df-bi 154  df-an 232  df-ex 1022  df-rex 1697

Copyright terms: Public domain