Theorem rexbidv 2438

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 1508	. 2 |- F/ x ph
2		ralbidv.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	rexbid 2436	1 |- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )

Syntax hints:   -> wi 4   <-> wb 104   E.wrex 2417

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-rex 2422

This theorem is referenced by:  rexbii  2442  2rexbidv  2460  rexralbidv  2461  rexeqbi1dv  2635  rexeqbidv  2639  cbvrex2v  2666  rspc2ev  2804  rspc3ev  2806  ceqsrex2v  2817  sbcrext  2986  uniiunlem  3185  eliun  3817  dfiin2g  3846  dfiunv2  3849  nn0suc  4518  rexxpf  4686  elrnmpt  4788  elrnmptg  4791  elimag  4885  funcnvuni  5192  fun11iun  5388  fvelrnb  5469  fvelimab  5477  foco2  5655  elabrex  5659  abrexco  5660  f1oiso  5727  f1oiso2  5728  acexmidlemab  5768  acexmidlemcase  5769  grprinvlem  5965  abrexex2g  6018  abrexex2  6022  recseq  6203  tfr0dm  6219  tfr1onlemaccex  6245  tfrcllemsucaccv  6251  tfrcllembxssdm  6253  tfrcllemaccex  6258  tfrcllemres  6259  freceq1  6289  frec0g  6294  freccllem  6299  frecfcllem  6301  frecsuclem  6303  frecsuc  6304  nnaordex  6423  qseq2  6478  elqsg  6479  elixpsn  6629  ixpsnf1o  6630  isfi  6655  enfi  6767  fimax2gtri  6795  elfi  6859  supeq3  6877  supmoti  6880  suplubti  6887  supisolem  6895  cnvinfex  6905  eqinfti  6907  infvalti  6909  infglbti  6912  enomnilem  7010  finomni  7012  exmidomni  7014  fodjum  7018  fodju0  7019  fodjuomnilemres  7020  fodjuomni  7021  ismkvnex  7029  fodjumkvlemres  7033  fodjumkv  7034  ltexnqq  7216  elinp  7282  prnmaxl  7296  prnminu  7297  prarloclem3  7305  ltdfpr  7314  genpdflem  7315  genipv  7317  genpassl  7332  genpassu  7333  ltexprlemm  7408  ltexprlemloc  7415  cauappcvgprlemm  7453  cauappcvgprlemopl  7454  cauappcvgprlemlol  7455  cauappcvgprlemopu  7456  cauappcvgprlemupu  7457  cauappcvgprlemdisj  7459  cauappcvgprlemloc  7460  cauappcvgprlemladdfu  7462  cauappcvgprlemladdfl  7463  cauappcvgprlemladdru  7464  cauappcvgprlemladdrl  7465  cauappcvgprlem1  7467  cauappcvgprlem2  7468  caucvgprlemm  7476  caucvgprlemopl  7477  caucvgprlemlol  7478  caucvgprlemopu  7479  caucvgprlemupu  7480  caucvgprlemdisj  7482  caucvgprlemloc  7483  caucvgprlemladdfu  7485  caucvgprlemladdrl  7486  caucvgprlem1  7487  caucvgprlem2  7488  caucvgprprlemell  7493  caucvgprprlemelu  7494  caucvgprprlemml  7502  caucvgprprlemmu  7503  caucvgprprlemexbt  7514  caucvgprprlem2  7518  suplocexprlemmu  7526  suplocexprlemru  7527  suplocexprlemdisj  7528  suplocexprlemloc  7529  suplocexprlemub  7531  recexgt0sr  7581  archsr  7590  map2psrprg  7613  suplocsrlemb  7614  axprecex  7688  nntopi  7702  axpre-suploclemres  7709  axpre-suploc  7710  cnegex  7940  apreap  8349  recexap  8414  sup3exmid  8715  creur  8717  creui  8718  cju  8719  supinfneg  9390  infsupneg  9391  exbtwnzlemshrink  10026  rebtwn2zlemshrink  10031  modqmuladd  10139  hashunlem  10550  shftfvalg  10590  shftfval  10593  rexfiuz  10761  recvguniq  10767  fimaxre2  10998  clim  11050  sumeq1  11124  summodc  11152  fsum3  11156  mertenslemub  11303  mertenslemi1  11304  mertenslem2  11305  mertensabs  11306  prodeq1f  11321  prodeq2w  11325  prodmodc  11347  divides  11495  odd2np1lem  11569  opeo  11594  omeo  11595  divalglemeunn  11618  divalglemeuneg  11620  infssuzex  11642  zeqzmulgcd  11659  bezoutlemnewy  11684  bezoutlemmain  11686  bezoutlemex  11689  bezoutlemaz  11691  exprmfct  11818  ennnfoneleminc  11924  ennnfonelemex  11927  ennnfonelemhom  11928  ennnfonelemnn0  11935  ennnfonelemr  11936  ctinfomlemom  11940  ctinfom  11941  basis2  12215  eltg2  12222  tg2  12229  neival  12312  isnei  12313  isneip  12315  restbasg  12337  cnpval  12367  iscnp  12368  icnpimaex  12380  lmbr  12382  lmbr2  12383  cnptoprest2  12409  lmff  12418  txbas  12427  txcnp  12440  txrest  12445  blssps  12596  blss  12597  mopni  12651  metss  12663  metrest  12675  metcnp3  12680  divcnap  12724  cncfval  12728  elcncf2  12730  cncfmet  12748  dedekindeulemuub  12764  dedekindeulemloc  12766  dedekindeulemlu  12768  suplociccreex  12771  dedekindicclemuub  12773  dedekindicclemloc  12775  dedekindicclemlu  12777  limccl  12797  ellimc3apf  12798  limcdifap  12800  limcmpted  12801  bj-inf2vnlem1  13168  bj-inf2vnlem2  13169  bj-nn0sucALT  13176  subctctexmid  13196  isomninnlem  13225  trilpolemlt1  13234