Theorem rexbidv 2476

Description: Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 20-Nov-1994.)

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

Allowed substitution hints:   ps( x)   ch( x)   A( x)

Proof of Theorem rexbidv

Step	Hyp	Ref	Expression
1		nfv 1526	. 2 |- F/ x ph
2		ralbidv.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	rexbid 2474	1 |- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )

Syntax hints:   -> wi 4   <-> wb 105   E.wrex 2454

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1445  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-4 1508  ax-17 1524  ax-ial 1532

This theorem depends on definitions:  df-bi 117  df-nf 1459  df-rex 2459

This theorem is referenced by:  rexbii  2482  2rexbidv  2500  rexralbidv  2501  rexeqbi1dv  2679  rexeqbidv  2683  cbvrex2vw  2713  cbvrex2v  2715  rspc2ev  2854  rspc3ev  2856  ceqsrex2v  2867  sbcrext  3038  uniiunlem  3242  eliun  3886  dfiin2g  3915  dfiunv2  3918  nn0suc  4597  rexxpf  4767  elrnmpt  4869  elrnmptg  4872  elimag  4967  funcnvuni  5277  fun11iun  5474  fvelrnb  5555  fvelimab  5564  foco2  5745  elabrex  5749  abrexco  5750  f1oiso  5817  f1oiso2  5818  acexmidlemab  5859  acexmidlemcase  5860  abrexex2g  6111  abrexex2  6115  recseq  6297  tfr0dm  6313  tfr1onlemaccex  6339  tfrcllemsucaccv  6345  tfrcllembxssdm  6347  tfrcllemaccex  6352  tfrcllemres  6353  freceq1  6383  frec0g  6388  freccllem  6393  frecfcllem  6395  frecsuclem  6397  frecsuc  6398  nnaordex  6519  qseq2  6574  elqsg  6575  elixpsn  6725  ixpsnf1o  6726  isfi  6751  enfi  6863  fimax2gtri  6891  elfi  6960  supeq3  6979  supmoti  6982  suplubti  6989  supisolem  6997  cnvinfex  7007  eqinfti  7009  infvalti  7011  infglbti  7014  enomnilem  7126  finomni  7128  exmidomni  7130  fodjum  7134  fodju0  7135  fodjuomnilemres  7136  fodjuomni  7137  ismkvnex  7143  fodjumkvlemres  7147  fodjumkv  7148  enmkvlem  7149  ltexnqq  7382  elinp  7448  prnmaxl  7462  prnminu  7463  prarloclem3  7471  ltdfpr  7480  genpdflem  7481  genipv  7483  genpassl  7498  genpassu  7499  ltexprlemm  7574  ltexprlemloc  7581  cauappcvgprlemm  7619  cauappcvgprlemopl  7620  cauappcvgprlemlol  7621  cauappcvgprlemopu  7622  cauappcvgprlemupu  7623  cauappcvgprlemdisj  7625  cauappcvgprlemloc  7626  cauappcvgprlemladdfu  7628  cauappcvgprlemladdfl  7629  cauappcvgprlemladdru  7630  cauappcvgprlemladdrl  7631  cauappcvgprlem1  7633  cauappcvgprlem2  7634  caucvgprlemm  7642  caucvgprlemopl  7643  caucvgprlemlol  7644  caucvgprlemopu  7645  caucvgprlemupu  7646  caucvgprlemdisj  7648  caucvgprlemloc  7649  caucvgprlemladdfu  7651  caucvgprlemladdrl  7652  caucvgprlem1  7653  caucvgprlem2  7654  caucvgprprlemell  7659  caucvgprprlemelu  7660  caucvgprprlemml  7668  caucvgprprlemmu  7669  caucvgprprlemexbt  7680  caucvgprprlem2  7684  suplocexprlemmu  7692  suplocexprlemru  7693  suplocexprlemdisj  7694  suplocexprlemloc  7695  suplocexprlemub  7697  recexgt0sr  7747  archsr  7756  map2psrprg  7779  suplocsrlemb  7780  axprecex  7854  nntopi  7868  axpre-suploclemres  7875  axpre-suploc  7876  cnegex  8109  apreap  8518  recexap  8583  sup3exmid  8887  creur  8889  creui  8890  cju  8891  supinfneg  9568  infsupneg  9569  exbtwnzlemshrink  10219  rebtwn2zlemshrink  10224  modqmuladd  10336  hashunlem  10752  shftfvalg  10795  shftfval  10798  rexfiuz  10966  recvguniq  10972  fimaxre2  11203  clim  11257  sumeq1  11331  summodc  11359  fsum3  11363  mertenslemub  11510  mertenslemi1  11511  mertenslem2  11512  mertensabs  11513  prodeq1f  11528  prodeq2w  11532  prodmodc  11554  fprodseq  11559  divides  11764  odd2np1lem  11844  opeo  11869  omeo  11870  divalglemeunn  11893  divalglemeuneg  11895  infssuzex  11917  nninfdcex  11921  zeqzmulgcd  11938  bezoutlemnewy  11964  bezoutlemmain  11966  bezoutlemex  11969  bezoutlemaz  11971  exprmfct  12105  nnnn0modprm0  12222  pceu  12262  pcprmpw2  12299  ennnfoneleminc  12379  ennnfonelemex  12382  ennnfonelemhom  12383  ennnfonelemnn0  12390  ennnfonelemr  12391  ctinfomlemom  12395  ctinfom  12396  nninfdclemcl  12416  nninfdclemp1  12418  nninfdc  12421  grprinvlem  12679  isnsgrp  12687  grpinvex  12758  dfgrp2  12773  grpidinv2  12799  grpidinv  12800  dfgrp3mlem  12838  grp1  12846  basis2  13126  eltg2  13133  tg2  13140  neival  13223  isnei  13224  isneip  13226  restbasg  13248  cnpval  13278  iscnp  13279  icnpimaex  13291  lmbr  13293  lmbr2  13294  cnptoprest2  13320  lmff  13329  txbas  13338  txcnp  13351  txrest  13356  blssps  13507  blss  13508  mopni  13562  metss  13574  metrest  13586  metcnp3  13591  divcnap  13635  cncfval  13639  elcncf2  13641  cncfmet  13659  dedekindeulemuub  13675  dedekindeulemloc  13677  dedekindeulemlu  13679  suplociccreex  13682  dedekindicclemuub  13684  dedekindicclemloc  13686  dedekindicclemlu  13688  limccl  13708  ellimc3apf  13709  limcdifap  13711  limcmpted  13712  bj-inf2vnlem1  14291  bj-inf2vnlem2  14292  bj-nn0sucALT  14299  sscoll2  14309  subctctexmid  14320  pw1nct  14322  isomninnlem  14348  trilpolemlt1  14359  trirec0  14362  ismkvnnlem  14370