Theorem rexbidv 1671

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

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

This theorem is referenced by:  2rexbidv 1688  rexralbidv 1689  rexeqd 1799  rexeq12d 1802  rcla42ev 1888  ceqsrex2v 1897  uniiunlem 2143  eliun 2584  dfiun2g 2600  dfiin2 2602  iunrab 2610  iununi 2631  orduninsuc 3130  elimag 3423  funcnvuni 3580  fvelrnb 3776  fvelima 3780  abrexexlem2 3875  funiunfv 3882  abrexex2 3887  f1oiso 3920  f1oweALT 3922  tfrlem3 3929  tfrlem12 3938  rdgeq1 3950  rdgeq2 3951  elrnoprabg 4140  nneob 4271  qseq2 4305  elqs 4306  elqsOLD 4307  elqsi 4308  isfi 4400  enfi 4553  pssnn 4554  unblem1 4558  unblem2 4559  unbnn2 4563  supmo 4591  suplub 4596  tz9.13 4680  aceq1 4746  aceq2 4748  aceq5lem3 4754  aceq5lem4 4755  aceq6a 4758  aceq6b 4759  kmlem9 4790  kmlem12 4793  kmlem14 4795  numth2 4802  numthcor 4803  zorn2lem7 4811  brdom3 4818  brdom7disj 4821  brdom6disj 4822  cardiun 4879  cflim 4929  prnmax 5119  genpv 5122  axrnegex 5303  axrrecex 5304  cnegex 5368  recex 5704  infm3 6086  infmsup 6100  nnunb 6102  arch 6103  xrsupsslem 6108  xrinfmsslem 6109  xrsupss 6110  xrinfmss 6111  xrub 6112  supxrre 6115  supxrunb1 6121  supxrunb2 6122  qbtwnxr 6281  fsequb 6491  limsupval 6560  creur 6774  creui 6775  reval 6787  imval 6788  replim 6793  cau3iri 6947  sumeq1 7014  dffsum 7030  clm0i 7115  clm0nnsi 7117  clm4ati 7122  climabs0i 7145  caucvg3 7200  dfisum 7223  infcvgaux2i 7252  infcvglem1 7253  expcnvi 7265  cncfval 7296  negfcncfi 7301  reeff1olem2 7457  unbenlem 7537  basis2 7645  eltg2 7649  tg2 7651  tgval3 7655  tgss2 7667  basgen2 7669  subtop 7674  neival 7743  isnei 7744  isneip 7746  cnpval 7785  iscnp 7786  cnpimaex 7791  isopn 7885  opni 7890  opnin 7895  metcnp 7913  metcnp2 7914  metcnpi 7916  metcnpi2 7917  metcni 7920  metcnss 7924  cncfmet 7931  tgioo 7941  lmbrf 7956  cmscvg 7973  lmss 7979  iscms2lem5 8019  cncms 8024  bcth 8058  isgrp 8067  isgrpi 8068  grpidinvlem3 8076  grpideu 8079  grpidinv2 8085  isgrp2i 8101  ghgrpilem3 8160  ringid 8170  nvcni 8354  nvcni2 8355  nvcni3 8356  va1cnlem 8370  sm1cnilem 8372  nvcnpi3 8447  nvcnpi4 8448  nmofval 8450  nmoval 8451  nmosetn0 8453  nmolb 8459  nmoubi 8460  nmlno0lem 8478  minveclem9 8578  minveclem10 8579  minveclem14 8583  minveclem24 8593  minvecex 8603  spwpr4OLD 8687  spwpr4aOLD 8688  efghgrpilem 8743  efifolem3 8748  circgrp 8764  grothinf 8805  h2hcau 8873  h2hlm 8874  hcau 9075  hhcms 9096  chcompl 9139  hhsscms 9174  projlem8 9217  projlem10 9219  projlem13 9222  projlem15 9224  projlem17 9226  projlem29 9238  pjtheui 9259  pjval 9263  pjeq2 9265  pjpj0i 9279  shsumval 9301  h1de2cti 9503  elspansn 9513  osumlem5 9606  nmopval 9806  elcnop 9807  nmopsetn0 9816  nmfnval 9827  nmfnsetn0 9829  elcnfn 9833  eigvecval 9846  nmoplb 9855  nmopub 9856  cnopc 9861  nmfnlb 9872  nmfnleub 9873  cnfnc 9878  eleigvec 9905  nmlnop0iALT 9944  nmopun 9963  nmcopexlem1 9975  lnopcon 9988  nmcfnexlem1 10004  lnfncon 10015  branmfn 10062  pjnmopi 10099  cvbr 10234  hatomic 10312  chrelat2 10322  cdjreui 10384  cdj3lem2 10387  cayleythlem 10438  hmeogrp 10571  subsp 10587  fgsb 10602  fgsb2 10607  cnfilca 10609  isfuna 10777  isfunb 10778

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

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 985  df-rex 1657

Copyright terms: Public domain