Theorem rexbidv 2531

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

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

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-rex 2514

This theorem is referenced by:  rexbii  2537  2rexbidv  2555  rexralbidv  2556  rexeqbi1dv  2741  rexeqbidv  2745  cbvrex2vw  2777  cbvrex2v  2779  rspc2ev  2922  rspc3ev  2924  ceqsrex2v  2935  sbcrext  3106  uniiunlem  3313  eliun  3969  dfiin2g  3998  dfiunv2  4001  nn0suc  4697  rexxpf  4872  elrnmpt  4976  elrnmptg  4979  elimag  5075  funcnvuni  5393  fun11iun  5598  fvelrnb  5686  fvelimab  5695  foco2  5886  elabrex  5890  elabrexg  5891  abrexco  5892  f1oiso  5959  f1oiso2  5960  acexmidlemab  6004  acexmidlemcase  6005  abrexex2g  6274  abrexex2  6278  recseq  6463  tfr0dm  6479  tfr1onlemaccex  6505  tfrcllemsucaccv  6511  tfrcllembxssdm  6513  tfrcllemaccex  6518  tfrcllemres  6519  freceq1  6549  frec0g  6554  freccllem  6559  frecfcllem  6561  frecsuclem  6563  frecsuc  6564  nnaordex  6687  qseq2  6744  elqsg  6745  elixpsn  6895  ixpsnf1o  6896  isfi  6925  enfi  7048  fimax2gtri  7077  elfi  7154  supeq3  7173  supmoti  7176  suplubti  7183  supisolem  7191  cnvinfex  7201  eqinfti  7203  infvalti  7205  infglbti  7208  enomnilem  7321  finomni  7323  exmidomni  7325  fodjum  7329  fodju0  7330  fodjuomnilemres  7331  fodjuomni  7332  ismkvnex  7338  fodjumkvlemres  7342  fodjumkv  7343  enmkvlem  7344  ltexnqq  7611  elinp  7677  prnmaxl  7691  prnminu  7692  prarloclem3  7700  ltdfpr  7709  genpdflem  7710  genipv  7712  genpassl  7727  genpassu  7728  ltexprlemm  7803  ltexprlemloc  7810  cauappcvgprlemm  7848  cauappcvgprlemopl  7849  cauappcvgprlemlol  7850  cauappcvgprlemopu  7851  cauappcvgprlemupu  7852  cauappcvgprlemdisj  7854  cauappcvgprlemloc  7855  cauappcvgprlemladdfu  7857  cauappcvgprlemladdfl  7858  cauappcvgprlemladdru  7859  cauappcvgprlemladdrl  7860  cauappcvgprlem1  7862  cauappcvgprlem2  7863  caucvgprlemm  7871  caucvgprlemopl  7872  caucvgprlemlol  7873  caucvgprlemopu  7874  caucvgprlemupu  7875  caucvgprlemdisj  7877  caucvgprlemloc  7878  caucvgprlemladdfu  7880  caucvgprlemladdrl  7881  caucvgprlem1  7882  caucvgprlem2  7883  caucvgprprlemell  7888  caucvgprprlemelu  7889  caucvgprprlemml  7897  caucvgprprlemmu  7898  caucvgprprlemexbt  7909  caucvgprprlem2  7913  suplocexprlemmu  7921  suplocexprlemru  7922  suplocexprlemdisj  7923  suplocexprlemloc  7924  suplocexprlemub  7926  recexgt0sr  7976  archsr  7985  map2psrprg  8008  suplocsrlemb  8009  axprecex  8083  nntopi  8097  axpre-suploclemres  8104  axpre-suploc  8105  cnegex  8340  apreap  8750  recexap  8816  sup3exmid  9120  creur  9122  creui  9123  cju  9124  supinfneg  9807  infsupneg  9808  infssuzex  10470  nninfdcex  10474  exbtwnzlemshrink  10485  rebtwn2zlemshrink  10490  modqmuladd  10605  hashunlem  11043  iswrd  11091  csbwrdg  11119  shftfvalg  11350  shftfval  11353  rexfiuz  11521  recvguniq  11527  fimaxre2  11759  clim  11813  sumeq1  11887  summodc  11915  fsum3  11919  mertenslemub  12066  mertenslemi1  12067  mertenslem2  12068  mertensabs  12069  prodeq1f  12084  prodeq2w  12088  prodmodc  12110  fprodseq  12115  divides  12321  odd2np1lem  12404  opeo  12429  omeo  12430  divalglemeunn  12453  divalglemeuneg  12455  zeqzmulgcd  12512  bezoutlemnewy  12538  bezoutlemmain  12540  bezoutlemex  12543  bezoutlemaz  12545  exprmfct  12681  nnnn0modprm0  12799  pceu  12839  pcprmpw2  12877  4sqlemafi  12939  4sqexercise1  12942  4sqlem12  12946  ennnfoneleminc  13003  ennnfonelemex  13006  ennnfonelemhom  13007  ennnfonelemnn0  13014  ennnfonelemr  13015  ctinfomlemom  13019  ctinfom  13020  nninfdclemcl  13040  nninfdclemp1  13042  nninfdc  13045  ptex  13318  grpinvalem  13439  igsumvalx  13443  gsumpropd  13446  gsumress  13449  gsum0g  13450  isnsgrp  13460  grpinvex  13564  dfgrp2  13581  grpidinv2  13612  grpidinv  13613  dfgrp3mlem  13652  grp1  13660  imasgrp2  13668  dvdsrd  14079  opprunitd  14095  subrgdvds  14220  lss1d  14368  lspsn  14401  ellspsn  14402  rspsn  14519  znf1o  14636  basis2  14743  eltg2  14748  tg2  14755  neival  14838  isnei  14839  isneip  14841  restbasg  14863  cnpval  14893  iscnp  14894  icnpimaex  14906  lmbr  14908  lmbr2  14909  cnptoprest2  14935  lmff  14944  txbas  14953  txcnp  14966  txrest  14971  blssps  15122  blss  15123  mopni  15177  metss  15189  metrest  15201  metcnp3  15206  divcnap  15260  cncfval  15267  elcncf2  15269  cncfmet  15287  dedekindeulemuub  15312  dedekindeulemloc  15314  dedekindeulemlu  15316  suplociccreex  15319  dedekindicclemuub  15321  dedekindicclemloc  15323  dedekindicclemlu  15325  ivthreinc  15340  limccl  15354  ellimc3apf  15355  limcdifap  15357  limcmpted  15358  plyval  15427  elply2  15430  2lgslem1b  15789  upgredg2vtx  15967  usgredg4  16034  ushgredgedg  16045  ushgredgedgloop  16047  vtxd0nedgbfi  16085  bj-inf2vnlem1  16442  bj-inf2vnlem2  16443  bj-nn0sucALT  16450  sscoll2  16460  3dom  16465  subctctexmid  16479  pw1nct  16482  isomninnlem  16512  trilpolemlt1  16523  trirec0  16526  ismkvnnlem  16534