Theorem rexbidv 2534

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

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

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-rex 2517

This theorem is referenced by:  rexbii  2540  2rexbidv  2558  rexralbidv  2559  rexeqbi1dv  2744  rexeqbidv  2748  cbvrex2vw  2780  cbvrex2v  2782  rspc2ev  2926  rspc3ev  2928  ceqsrex2v  2939  sbcrext  3110  uniiunlem  3318  eliun  3979  dfiin2g  4008  dfiunv2  4011  nn0suc  4708  rexxpf  4883  elrnmpt  4987  elrnmptg  4990  elimag  5086  funcnvuni  5406  fun11iun  5613  fvelrnb  5702  fvelimab  5711  foco2  5904  elabrex  5908  elabrexg  5909  abrexco  5910  f1oiso  5977  f1oiso2  5978  acexmidlemab  6022  acexmidlemcase  6023  abrexex2g  6291  abrexex2  6295  recseq  6515  tfr0dm  6531  tfr1onlemaccex  6557  tfrcllemsucaccv  6563  tfrcllembxssdm  6565  tfrcllemaccex  6570  tfrcllemres  6571  freceq1  6601  frec0g  6606  freccllem  6611  frecfcllem  6613  frecsuclem  6615  frecsuc  6616  nnaordex  6739  qseq2  6796  elqsg  6797  elixpsn  6947  ixpsnf1o  6948  isfi  6977  enfi  7103  fimax2gtri  7134  elfi  7230  supeq3  7249  supmoti  7252  suplubti  7259  supisolem  7267  cnvinfex  7277  eqinfti  7279  infvalti  7281  infglbti  7284  enomnilem  7397  finomni  7399  exmidomni  7401  fodjum  7405  fodju0  7406  fodjuomnilemres  7407  fodjuomni  7408  ismkvnex  7414  fodjumkvlemres  7418  fodjumkv  7419  enmkvlem  7420  ltexnqq  7688  elinp  7754  prnmaxl  7768  prnminu  7769  prarloclem3  7777  ltdfpr  7786  genpdflem  7787  genipv  7789  genpassl  7804  genpassu  7805  ltexprlemm  7880  ltexprlemloc  7887  cauappcvgprlemm  7925  cauappcvgprlemopl  7926  cauappcvgprlemlol  7927  cauappcvgprlemopu  7928  cauappcvgprlemupu  7929  cauappcvgprlemdisj  7931  cauappcvgprlemloc  7932  cauappcvgprlemladdfu  7934  cauappcvgprlemladdfl  7935  cauappcvgprlemladdru  7936  cauappcvgprlemladdrl  7937  cauappcvgprlem1  7939  cauappcvgprlem2  7940  caucvgprlemm  7948  caucvgprlemopl  7949  caucvgprlemlol  7950  caucvgprlemopu  7951  caucvgprlemupu  7952  caucvgprlemdisj  7954  caucvgprlemloc  7955  caucvgprlemladdfu  7957  caucvgprlemladdrl  7958  caucvgprlem1  7959  caucvgprlem2  7960  caucvgprprlemell  7965  caucvgprprlemelu  7966  caucvgprprlemml  7974  caucvgprprlemmu  7975  caucvgprprlemexbt  7986  caucvgprprlem2  7990  suplocexprlemmu  7998  suplocexprlemru  7999  suplocexprlemdisj  8000  suplocexprlemloc  8001  suplocexprlemub  8003  recexgt0sr  8053  archsr  8062  map2psrprg  8085  suplocsrlemb  8086  axprecex  8160  nntopi  8174  axpre-suploclemres  8181  axpre-suploc  8182  cnegex  8416  apreap  8826  recexap  8892  sup3exmid  9196  creur  9198  creui  9199  cju  9200  supinfneg  9890  infsupneg  9891  infssuzex  10556  nninfdcex  10560  exbtwnzlemshrink  10571  rebtwn2zlemshrink  10576  modqmuladd  10691  hashunlem  11130  iswrd  11181  csbwrdg  11209  shftfvalg  11458  shftfval  11461  rexfiuz  11629  recvguniq  11635  fimaxre2  11867  clim  11921  sumeq1  11995  summodc  12024  fsum3  12028  mertenslemub  12175  mertenslemi1  12176  mertenslem2  12177  mertensabs  12178  prodeq1f  12193  prodeq2w  12197  prodmodc  12219  fprodseq  12224  divides  12430  odd2np1lem  12513  opeo  12538  omeo  12539  divalglemeunn  12562  divalglemeuneg  12564  zeqzmulgcd  12621  bezoutlemnewy  12647  bezoutlemmain  12649  bezoutlemex  12652  bezoutlemaz  12654  exprmfct  12790  nnnn0modprm0  12908  pceu  12948  pcprmpw2  12986  4sqlemafi  13048  4sqexercise1  13051  4sqlem12  13055  ennnfoneleminc  13112  ennnfonelemex  13115  ennnfonelemhom  13116  ennnfonelemnn0  13123  ennnfonelemr  13124  ctinfomlemom  13128  ctinfom  13129  nninfdclemcl  13149  nninfdclemp1  13151  nninfdc  13154  ptex  13427  grpinvalem  13548  igsumvalx  13552  gsumpropd  13555  gsumress  13558  gsum0g  13559  isnsgrp  13569  grpinvex  13673  dfgrp2  13690  grpidinv2  13721  grpidinv  13722  dfgrp3mlem  13761  grp1  13769  imasgrp2  13777  dvdsrd  14189  opprunitd  14205  subrgdvds  14330  lss1d  14479  lspsn  14512  ellspsn  14513  rspsn  14630  znf1o  14747  basis2  14859  eltg2  14864  tg2  14871  neival  14954  isnei  14955  isneip  14957  restbasg  14979  cnpval  15009  iscnp  15010  icnpimaex  15022  lmbr  15024  lmbr2  15025  cnptoprest2  15051  lmff  15060  txbas  15069  txcnp  15082  txrest  15087  blssps  15238  blss  15239  mopni  15293  metss  15305  metrest  15317  metcnp3  15322  divcnap  15376  cncfval  15383  elcncf2  15385  cncfmet  15403  dedekindeulemuub  15428  dedekindeulemloc  15430  dedekindeulemlu  15432  suplociccreex  15435  dedekindicclemuub  15437  dedekindicclemloc  15439  dedekindicclemlu  15441  ivthreinc  15456  limccl  15470  ellimc3apf  15471  limcdifap  15473  limcmpted  15474  plyval  15543  elply2  15546  2lgslem1b  15908  upgredg2vtx  16089  usgredg4  16156  ushgredgedg  16167  ushgredgedgloop  16169  vtxd0nedgbfi  16240  bj-inf2vnlem1  16686  bj-inf2vnlem2  16687  bj-nn0sucALT  16694  sscoll2  16704  3dom  16708  subctctexmid  16722  pw1nct  16725  isomninnlem  16762  trilpolemlt1  16773  trirec0  16776  qdiff  16781  ismkvnnlem  16785