Theorem rexbidv 2436

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 2434	1 |- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )

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

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 2420

This theorem is referenced by:  rexbii  2440  2rexbidv  2458  rexralbidv  2459  rexeqbi1dv  2633  rexeqbidv  2637  cbvrex2v  2661  rspc2ev  2799  rspc3ev  2801  ceqsrex2v  2812  sbcrext  2981  uniiunlem  3180  eliun  3812  dfiin2g  3841  dfiunv2  3844  nn0suc  4513  rexxpf  4681  elrnmpt  4783  elrnmptg  4786  elimag  4880  funcnvuni  5187  fun11iun  5381  fvelrnb  5462  fvelimab  5470  foco2  5648  elabrex  5652  abrexco  5653  f1oiso  5720  f1oiso2  5721  acexmidlemab  5761  acexmidlemcase  5762  grprinvlem  5958  abrexex2g  6011  abrexex2  6015  recseq  6196  tfr0dm  6212  tfr1onlemaccex  6238  tfrcllemsucaccv  6244  tfrcllembxssdm  6246  tfrcllemaccex  6251  tfrcllemres  6252  freceq1  6282  frec0g  6287  freccllem  6292  frecfcllem  6294  frecsuclem  6296  frecsuc  6297  nnaordex  6416  qseq2  6471  elqsg  6472  elixpsn  6622  ixpsnf1o  6623  isfi  6648  enfi  6760  fimax2gtri  6788  elfi  6852  supeq3  6870  supmoti  6873  suplubti  6880  supisolem  6888  cnvinfex  6898  eqinfti  6900  infvalti  6902  infglbti  6905  enomnilem  7003  finomni  7005  exmidomni  7007  fodjum  7011  fodju0  7012  fodjuomnilemres  7013  fodjuomni  7014  ismkvnex  7022  fodjumkvlemres  7026  fodjumkv  7027  ltexnqq  7209  elinp  7275  prnmaxl  7289  prnminu  7290  prarloclem3  7298  ltdfpr  7307  genpdflem  7308  genipv  7310  genpassl  7325  genpassu  7326  ltexprlemm  7401  ltexprlemloc  7408  cauappcvgprlemm  7446  cauappcvgprlemopl  7447  cauappcvgprlemlol  7448  cauappcvgprlemopu  7449  cauappcvgprlemupu  7450  cauappcvgprlemdisj  7452  cauappcvgprlemloc  7453  cauappcvgprlemladdfu  7455  cauappcvgprlemladdfl  7456  cauappcvgprlemladdru  7457  cauappcvgprlemladdrl  7458  cauappcvgprlem1  7460  cauappcvgprlem2  7461  caucvgprlemm  7469  caucvgprlemopl  7470  caucvgprlemlol  7471  caucvgprlemopu  7472  caucvgprlemupu  7473  caucvgprlemdisj  7475  caucvgprlemloc  7476  caucvgprlemladdfu  7478  caucvgprlemladdrl  7479  caucvgprlem1  7480  caucvgprlem2  7481  caucvgprprlemell  7486  caucvgprprlemelu  7487  caucvgprprlemml  7495  caucvgprprlemmu  7496  caucvgprprlemexbt  7507  caucvgprprlem2  7511  suplocexprlemmu  7519  suplocexprlemru  7520  suplocexprlemdisj  7521  suplocexprlemloc  7522  suplocexprlemub  7524  recexgt0sr  7574  archsr  7583  map2psrprg  7606  suplocsrlemb  7607  axprecex  7681  nntopi  7695  axpre-suploclemres  7702  axpre-suploc  7703  cnegex  7933  apreap  8342  recexap  8407  sup3exmid  8708  creur  8710  creui  8711  cju  8712  supinfneg  9383  infsupneg  9384  exbtwnzlemshrink  10019  rebtwn2zlemshrink  10024  modqmuladd  10132  hashunlem  10543  shftfvalg  10583  shftfval  10586  rexfiuz  10754  recvguniq  10760  fimaxre2  10991  clim  11043  sumeq1  11117  summodc  11145  fsum3  11149  mertenslemub  11296  mertenslemi1  11297  mertenslem2  11298  mertensabs  11299  prodeq1f  11314  prodeq2w  11318  divides  11484  odd2np1lem  11558  opeo  11583  omeo  11584  divalglemeunn  11607  divalglemeuneg  11609  infssuzex  11631  zeqzmulgcd  11648  bezoutlemnewy  11673  bezoutlemmain  11675  bezoutlemex  11678  bezoutlemaz  11680  exprmfct  11807  ennnfoneleminc  11913  ennnfonelemex  11916  ennnfonelemhom  11917  ennnfonelemnn0  11924  ennnfonelemr  11925  ctinfomlemom  11929  ctinfom  11930  basis2  12204  eltg2  12211  tg2  12218  neival  12301  isnei  12302  isneip  12304  restbasg  12326  cnpval  12356  iscnp  12357  icnpimaex  12369  lmbr  12371  lmbr2  12372  cnptoprest2  12398  lmff  12407  txbas  12416  txcnp  12429  txrest  12434  blssps  12585  blss  12586  mopni  12640  metss  12652  metrest  12664  metcnp3  12669  divcnap  12713  cncfval  12717  elcncf2  12719  cncfmet  12737  dedekindeulemuub  12753  dedekindeulemloc  12755  dedekindeulemlu  12757  suplociccreex  12760  dedekindicclemuub  12762  dedekindicclemloc  12764  dedekindicclemlu  12766  limccl  12786  ellimc3apf  12787  limcdifap  12789  limcmpted  12790  bj-inf2vnlem1  13157  bj-inf2vnlem2  13158  bj-nn0sucALT  13165  subctctexmid  13185  isomninnlem  13214  trilpolemlt1  13223