Theorem rexbidv 2410

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

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-4 1468  ax-17 1487  ax-ial 1495

This theorem depends on definitions:  df-bi 116  df-nf 1418  df-rex 2394

This theorem is referenced by:  rexbii  2414  2rexbidv  2432  rexralbidv  2433  rexeqbi1dv  2607  rexeqbidv  2611  cbvrex2v  2635  rspc2ev  2772  rspc3ev  2774  ceqsrex2v  2785  sbcrext  2952  uniiunlem  3149  eliun  3781  dfiin2g  3810  dfiunv2  3813  nn0suc  4476  rexxpf  4644  elrnmpt  4746  elrnmptg  4749  elimag  4841  funcnvuni  5148  fun11iun  5342  fvelrnb  5421  fvelimab  5429  foco2  5607  elabrex  5611  abrexco  5612  f1oiso  5679  f1oiso2  5680  acexmidlemab  5720  acexmidlemcase  5721  grprinvlem  5917  abrexex2g  5970  abrexex2  5974  recseq  6155  tfr0dm  6171  tfr1onlemaccex  6197  tfrcllemsucaccv  6203  tfrcllembxssdm  6205  tfrcllemaccex  6210  tfrcllemres  6211  freceq1  6241  frec0g  6246  freccllem  6251  frecfcllem  6253  frecsuclem  6255  frecsuc  6256  nnaordex  6375  qseq2  6430  elqsg  6431  elixpsn  6581  ixpsnf1o  6582  isfi  6607  enfi  6718  fimax2gtri  6746  elfi  6809  supeq3  6827  supmoti  6830  suplubti  6837  supisolem  6845  cnvinfex  6855  eqinfti  6857  infvalti  6859  infglbti  6862  enomnilem  6958  finomni  6960  exmidomni  6962  fodjum  6966  fodju0  6967  fodjuomnilemres  6968  fodjuomni  6969  fodjumkvlemres  6980  fodjumkv  6981  ltexnqq  7158  elinp  7224  prnmaxl  7238  prnminu  7239  prarloclem3  7247  ltdfpr  7256  genpdflem  7257  genipv  7259  genpassl  7274  genpassu  7275  ltexprlemm  7350  ltexprlemloc  7357  cauappcvgprlemm  7395  cauappcvgprlemopl  7396  cauappcvgprlemlol  7397  cauappcvgprlemopu  7398  cauappcvgprlemupu  7399  cauappcvgprlemdisj  7401  cauappcvgprlemloc  7402  cauappcvgprlemladdfu  7404  cauappcvgprlemladdfl  7405  cauappcvgprlemladdru  7406  cauappcvgprlemladdrl  7407  cauappcvgprlem1  7409  cauappcvgprlem2  7410  caucvgprlemm  7418  caucvgprlemopl  7419  caucvgprlemlol  7420  caucvgprlemopu  7421  caucvgprlemupu  7422  caucvgprlemdisj  7424  caucvgprlemloc  7425  caucvgprlemladdfu  7427  caucvgprlemladdrl  7428  caucvgprlem1  7429  caucvgprlem2  7430  caucvgprprlemell  7435  caucvgprprlemelu  7436  caucvgprprlemml  7444  caucvgprprlemmu  7445  caucvgprprlemexbt  7456  caucvgprprlem2  7460  recexgt0sr  7510  archsr  7518  axprecex  7609  nntopi  7623  cnegex  7857  apreap  8261  recexap  8321  sup3exmid  8619  creur  8621  creui  8622  cju  8623  supinfneg  9286  infsupneg  9287  exbtwnzlemshrink  9913  rebtwn2zlemshrink  9918  modqmuladd  10026  hashunlem  10437  shftfvalg  10477  shftfval  10480  rexfiuz  10647  recvguniq  10653  fimaxre2  10884  clim  10936  sumeq1  11010  summodc  11038  fsum3  11042  mertenslemub  11189  mertenslemi1  11190  mertenslem2  11191  mertensabs  11192  divides  11337  odd2np1lem  11411  opeo  11436  omeo  11437  divalglemeunn  11460  divalglemeuneg  11462  infssuzex  11484  zeqzmulgcd  11501  bezoutlemnewy  11524  bezoutlemmain  11526  bezoutlemex  11529  bezoutlemaz  11531  exprmfct  11658  ennnfoneleminc  11763  ennnfonelemex  11766  ennnfonelemhom  11767  ennnfonelemnn0  11774  ennnfonelemr  11775  ctinfomlemom  11779  ctinfom  11780  basis2  12052  eltg2  12059  tg2  12066  neival  12149  isnei  12150  isneip  12152  restbasg  12174  cnpval  12203  iscnp  12204  icnpimaex  12216  lmbr  12218  lmbr2  12219  cnptoprest2  12245  lmff  12254  txbas  12263  txcnp  12276  txrest  12281  blssps  12410  blss  12411  mopni  12465  metss  12477  metrest  12489  metcnp3  12494  divcnap  12535  cncfval  12539  elcncf2  12541  cncfmet  12559  limccl  12578  ellimc3apf  12579  limcdifap  12581  limcmpted  12582  bj-inf2vnlem1  12851  bj-inf2vnlem2  12852  bj-nn0sucALT  12859  isomninnlem  12906  trilpolemlt1  12915