Theorem rexbidv 2498

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

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

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-rex 2481

This theorem is referenced by:  rexbii  2504  2rexbidv  2522  rexralbidv  2523  rexeqbi1dv  2706  rexeqbidv  2710  cbvrex2vw  2741  cbvrex2v  2743  rspc2ev  2883  rspc3ev  2885  ceqsrex2v  2896  sbcrext  3067  uniiunlem  3273  eliun  3921  dfiin2g  3950  dfiunv2  3953  nn0suc  4641  rexxpf  4814  elrnmpt  4916  elrnmptg  4919  elimag  5014  funcnvuni  5328  fun11iun  5528  fvelrnb  5611  fvelimab  5620  foco2  5803  elabrex  5807  elabrexg  5808  abrexco  5809  f1oiso  5876  f1oiso2  5877  acexmidlemab  5919  acexmidlemcase  5920  abrexex2g  6186  abrexex2  6190  recseq  6373  tfr0dm  6389  tfr1onlemaccex  6415  tfrcllemsucaccv  6421  tfrcllembxssdm  6423  tfrcllemaccex  6428  tfrcllemres  6429  freceq1  6459  frec0g  6464  freccllem  6469  frecfcllem  6471  frecsuclem  6473  frecsuc  6474  nnaordex  6595  qseq2  6652  elqsg  6653  elixpsn  6803  ixpsnf1o  6804  isfi  6829  enfi  6943  fimax2gtri  6971  elfi  7046  supeq3  7065  supmoti  7068  suplubti  7075  supisolem  7083  cnvinfex  7093  eqinfti  7095  infvalti  7097  infglbti  7100  enomnilem  7213  finomni  7215  exmidomni  7217  fodjum  7221  fodju0  7222  fodjuomnilemres  7223  fodjuomni  7224  ismkvnex  7230  fodjumkvlemres  7234  fodjumkv  7235  enmkvlem  7236  ltexnqq  7492  elinp  7558  prnmaxl  7572  prnminu  7573  prarloclem3  7581  ltdfpr  7590  genpdflem  7591  genipv  7593  genpassl  7608  genpassu  7609  ltexprlemm  7684  ltexprlemloc  7691  cauappcvgprlemm  7729  cauappcvgprlemopl  7730  cauappcvgprlemlol  7731  cauappcvgprlemopu  7732  cauappcvgprlemupu  7733  cauappcvgprlemdisj  7735  cauappcvgprlemloc  7736  cauappcvgprlemladdfu  7738  cauappcvgprlemladdfl  7739  cauappcvgprlemladdru  7740  cauappcvgprlemladdrl  7741  cauappcvgprlem1  7743  cauappcvgprlem2  7744  caucvgprlemm  7752  caucvgprlemopl  7753  caucvgprlemlol  7754  caucvgprlemopu  7755  caucvgprlemupu  7756  caucvgprlemdisj  7758  caucvgprlemloc  7759  caucvgprlemladdfu  7761  caucvgprlemladdrl  7762  caucvgprlem1  7763  caucvgprlem2  7764  caucvgprprlemell  7769  caucvgprprlemelu  7770  caucvgprprlemml  7778  caucvgprprlemmu  7779  caucvgprprlemexbt  7790  caucvgprprlem2  7794  suplocexprlemmu  7802  suplocexprlemru  7803  suplocexprlemdisj  7804  suplocexprlemloc  7805  suplocexprlemub  7807  recexgt0sr  7857  archsr  7866  map2psrprg  7889  suplocsrlemb  7890  axprecex  7964  nntopi  7978  axpre-suploclemres  7985  axpre-suploc  7986  cnegex  8221  apreap  8631  recexap  8697  sup3exmid  9001  creur  9003  creui  9004  cju  9005  supinfneg  9686  infsupneg  9687  infssuzex  10340  nninfdcex  10344  exbtwnzlemshrink  10355  rebtwn2zlemshrink  10360  modqmuladd  10475  hashunlem  10913  iswrd  10954  csbwrdg  10981  shftfvalg  11000  shftfval  11003  rexfiuz  11171  recvguniq  11177  fimaxre2  11409  clim  11463  sumeq1  11537  summodc  11565  fsum3  11569  mertenslemub  11716  mertenslemi1  11717  mertenslem2  11718  mertensabs  11719  prodeq1f  11734  prodeq2w  11738  prodmodc  11760  fprodseq  11765  divides  11971  odd2np1lem  12054  opeo  12079  omeo  12080  divalglemeunn  12103  divalglemeuneg  12105  zeqzmulgcd  12162  bezoutlemnewy  12188  bezoutlemmain  12190  bezoutlemex  12193  bezoutlemaz  12195  exprmfct  12331  nnnn0modprm0  12449  pceu  12489  pcprmpw2  12527  4sqlemafi  12589  4sqexercise1  12592  4sqlem12  12596  ennnfoneleminc  12653  ennnfonelemex  12656  ennnfonelemhom  12657  ennnfonelemnn0  12664  ennnfonelemr  12665  ctinfomlemom  12669  ctinfom  12670  nninfdclemcl  12690  nninfdclemp1  12692  nninfdc  12695  ptex  12966  grpinvalem  13087  igsumvalx  13091  gsumpropd  13094  gsumress  13097  gsum0g  13098  isnsgrp  13108  grpinvex  13212  dfgrp2  13229  grpidinv2  13260  grpidinv  13261  dfgrp3mlem  13300  grp1  13308  imasgrp2  13316  dvdsrd  13726  opprunitd  13742  subrgdvds  13867  lss1d  14015  lspsn  14048  ellspsn  14049  rspsn  14166  znf1o  14283  basis2  14368  eltg2  14373  tg2  14380  neival  14463  isnei  14464  isneip  14466  restbasg  14488  cnpval  14518  iscnp  14519  icnpimaex  14531  lmbr  14533  lmbr2  14534  cnptoprest2  14560  lmff  14569  txbas  14578  txcnp  14591  txrest  14596  blssps  14747  blss  14748  mopni  14802  metss  14814  metrest  14826  metcnp3  14831  divcnap  14885  cncfval  14892  elcncf2  14894  cncfmet  14912  dedekindeulemuub  14937  dedekindeulemloc  14939  dedekindeulemlu  14941  suplociccreex  14944  dedekindicclemuub  14946  dedekindicclemloc  14948  dedekindicclemlu  14950  ivthreinc  14965  limccl  14979  ellimc3apf  14980  limcdifap  14982  limcmpted  14983  plyval  15052  elply2  15055  2lgslem1b  15414  bj-inf2vnlem1  15700  bj-inf2vnlem2  15701  bj-nn0sucALT  15708  sscoll2  15718  subctctexmid  15731  pw1nct  15734  isomninnlem  15761  trilpolemlt1  15772  trirec0  15775  ismkvnnlem  15783