Theorem rexbidv 2507

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

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

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-rex 2490

This theorem is referenced by:  rexbii  2513  2rexbidv  2531  rexralbidv  2532  rexeqbi1dv  2715  rexeqbidv  2719  cbvrex2vw  2750  cbvrex2v  2752  rspc2ev  2892  rspc3ev  2894  ceqsrex2v  2905  sbcrext  3076  uniiunlem  3282  eliun  3931  dfiin2g  3960  dfiunv2  3963  nn0suc  4653  rexxpf  4826  elrnmpt  4928  elrnmptg  4931  elimag  5027  funcnvuni  5344  fun11iun  5545  fvelrnb  5628  fvelimab  5637  foco2  5824  elabrex  5828  elabrexg  5829  abrexco  5830  f1oiso  5897  f1oiso2  5898  acexmidlemab  5940  acexmidlemcase  5941  abrexex2g  6207  abrexex2  6211  recseq  6394  tfr0dm  6410  tfr1onlemaccex  6436  tfrcllemsucaccv  6442  tfrcllembxssdm  6444  tfrcllemaccex  6449  tfrcllemres  6450  freceq1  6480  frec0g  6485  freccllem  6490  frecfcllem  6492  frecsuclem  6494  frecsuc  6495  nnaordex  6616  qseq2  6673  elqsg  6674  elixpsn  6824  ixpsnf1o  6825  isfi  6854  enfi  6972  fimax2gtri  7000  elfi  7075  supeq3  7094  supmoti  7097  suplubti  7104  supisolem  7112  cnvinfex  7122  eqinfti  7124  infvalti  7126  infglbti  7129  enomnilem  7242  finomni  7244  exmidomni  7246  fodjum  7250  fodju0  7251  fodjuomnilemres  7252  fodjuomni  7253  ismkvnex  7259  fodjumkvlemres  7263  fodjumkv  7264  enmkvlem  7265  ltexnqq  7523  elinp  7589  prnmaxl  7603  prnminu  7604  prarloclem3  7612  ltdfpr  7621  genpdflem  7622  genipv  7624  genpassl  7639  genpassu  7640  ltexprlemm  7715  ltexprlemloc  7722  cauappcvgprlemm  7760  cauappcvgprlemopl  7761  cauappcvgprlemlol  7762  cauappcvgprlemopu  7763  cauappcvgprlemupu  7764  cauappcvgprlemdisj  7766  cauappcvgprlemloc  7767  cauappcvgprlemladdfu  7769  cauappcvgprlemladdfl  7770  cauappcvgprlemladdru  7771  cauappcvgprlemladdrl  7772  cauappcvgprlem1  7774  cauappcvgprlem2  7775  caucvgprlemm  7783  caucvgprlemopl  7784  caucvgprlemlol  7785  caucvgprlemopu  7786  caucvgprlemupu  7787  caucvgprlemdisj  7789  caucvgprlemloc  7790  caucvgprlemladdfu  7792  caucvgprlemladdrl  7793  caucvgprlem1  7794  caucvgprlem2  7795  caucvgprprlemell  7800  caucvgprprlemelu  7801  caucvgprprlemml  7809  caucvgprprlemmu  7810  caucvgprprlemexbt  7821  caucvgprprlem2  7825  suplocexprlemmu  7833  suplocexprlemru  7834  suplocexprlemdisj  7835  suplocexprlemloc  7836  suplocexprlemub  7838  recexgt0sr  7888  archsr  7897  map2psrprg  7920  suplocsrlemb  7921  axprecex  7995  nntopi  8009  axpre-suploclemres  8016  axpre-suploc  8017  cnegex  8252  apreap  8662  recexap  8728  sup3exmid  9032  creur  9034  creui  9035  cju  9036  supinfneg  9718  infsupneg  9719  infssuzex  10378  nninfdcex  10382  exbtwnzlemshrink  10393  rebtwn2zlemshrink  10398  modqmuladd  10513  hashunlem  10951  iswrd  10998  csbwrdg  11025  shftfvalg  11162  shftfval  11165  rexfiuz  11333  recvguniq  11339  fimaxre2  11571  clim  11625  sumeq1  11699  summodc  11727  fsum3  11731  mertenslemub  11878  mertenslemi1  11879  mertenslem2  11880  mertensabs  11881  prodeq1f  11896  prodeq2w  11900  prodmodc  11922  fprodseq  11927  divides  12133  odd2np1lem  12216  opeo  12241  omeo  12242  divalglemeunn  12265  divalglemeuneg  12267  zeqzmulgcd  12324  bezoutlemnewy  12350  bezoutlemmain  12352  bezoutlemex  12355  bezoutlemaz  12357  exprmfct  12493  nnnn0modprm0  12611  pceu  12651  pcprmpw2  12689  4sqlemafi  12751  4sqexercise1  12754  4sqlem12  12758  ennnfoneleminc  12815  ennnfonelemex  12818  ennnfonelemhom  12819  ennnfonelemnn0  12826  ennnfonelemr  12827  ctinfomlemom  12831  ctinfom  12832  nninfdclemcl  12852  nninfdclemp1  12854  nninfdc  12857  ptex  13129  grpinvalem  13250  igsumvalx  13254  gsumpropd  13257  gsumress  13260  gsum0g  13261  isnsgrp  13271  grpinvex  13375  dfgrp2  13392  grpidinv2  13423  grpidinv  13424  dfgrp3mlem  13463  grp1  13471  imasgrp2  13479  dvdsrd  13889  opprunitd  13905  subrgdvds  14030  lss1d  14178  lspsn  14211  ellspsn  14212  rspsn  14329  znf1o  14446  basis2  14553  eltg2  14558  tg2  14565  neival  14648  isnei  14649  isneip  14651  restbasg  14673  cnpval  14703  iscnp  14704  icnpimaex  14716  lmbr  14718  lmbr2  14719  cnptoprest2  14745  lmff  14754  txbas  14763  txcnp  14776  txrest  14781  blssps  14932  blss  14933  mopni  14987  metss  14999  metrest  15011  metcnp3  15016  divcnap  15070  cncfval  15077  elcncf2  15079  cncfmet  15097  dedekindeulemuub  15122  dedekindeulemloc  15124  dedekindeulemlu  15126  suplociccreex  15129  dedekindicclemuub  15131  dedekindicclemloc  15133  dedekindicclemlu  15135  ivthreinc  15150  limccl  15164  ellimc3apf  15165  limcdifap  15167  limcmpted  15168  plyval  15237  elply2  15240  2lgslem1b  15599  bj-inf2vnlem1  15943  bj-inf2vnlem2  15944  bj-nn0sucALT  15951  sscoll2  15961  subctctexmid  15974  pw1nct  15977  isomninnlem  16006  trilpolemlt1  16017  trirec0  16020  ismkvnnlem  16028