Theorem rexbidv 2478

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

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

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-rex 2461

This theorem is referenced by:  rexbii  2484  2rexbidv  2502  rexralbidv  2503  rexeqbi1dv  2682  rexeqbidv  2686  cbvrex2vw  2717  cbvrex2v  2719  rspc2ev  2858  rspc3ev  2860  ceqsrex2v  2871  sbcrext  3042  uniiunlem  3246  eliun  3892  dfiin2g  3921  dfiunv2  3924  nn0suc  4605  rexxpf  4776  elrnmpt  4878  elrnmptg  4881  elimag  4976  funcnvuni  5287  fun11iun  5484  fvelrnb  5565  fvelimab  5574  foco2  5756  elabrex  5760  elabrexg  5761  abrexco  5762  f1oiso  5829  f1oiso2  5830  acexmidlemab  5871  acexmidlemcase  5872  abrexex2g  6123  abrexex2  6127  recseq  6309  tfr0dm  6325  tfr1onlemaccex  6351  tfrcllemsucaccv  6357  tfrcllembxssdm  6359  tfrcllemaccex  6364  tfrcllemres  6365  freceq1  6395  frec0g  6400  freccllem  6405  frecfcllem  6407  frecsuclem  6409  frecsuc  6410  nnaordex  6531  qseq2  6586  elqsg  6587  elixpsn  6737  ixpsnf1o  6738  isfi  6763  enfi  6875  fimax2gtri  6903  elfi  6972  supeq3  6991  supmoti  6994  suplubti  7001  supisolem  7009  cnvinfex  7019  eqinfti  7021  infvalti  7023  infglbti  7026  enomnilem  7138  finomni  7140  exmidomni  7142  fodjum  7146  fodju0  7147  fodjuomnilemres  7148  fodjuomni  7149  ismkvnex  7155  fodjumkvlemres  7159  fodjumkv  7160  enmkvlem  7161  ltexnqq  7409  elinp  7475  prnmaxl  7489  prnminu  7490  prarloclem3  7498  ltdfpr  7507  genpdflem  7508  genipv  7510  genpassl  7525  genpassu  7526  ltexprlemm  7601  ltexprlemloc  7608  cauappcvgprlemm  7646  cauappcvgprlemopl  7647  cauappcvgprlemlol  7648  cauappcvgprlemopu  7649  cauappcvgprlemupu  7650  cauappcvgprlemdisj  7652  cauappcvgprlemloc  7653  cauappcvgprlemladdfu  7655  cauappcvgprlemladdfl  7656  cauappcvgprlemladdru  7657  cauappcvgprlemladdrl  7658  cauappcvgprlem1  7660  cauappcvgprlem2  7661  caucvgprlemm  7669  caucvgprlemopl  7670  caucvgprlemlol  7671  caucvgprlemopu  7672  caucvgprlemupu  7673  caucvgprlemdisj  7675  caucvgprlemloc  7676  caucvgprlemladdfu  7678  caucvgprlemladdrl  7679  caucvgprlem1  7680  caucvgprlem2  7681  caucvgprprlemell  7686  caucvgprprlemelu  7687  caucvgprprlemml  7695  caucvgprprlemmu  7696  caucvgprprlemexbt  7707  caucvgprprlem2  7711  suplocexprlemmu  7719  suplocexprlemru  7720  suplocexprlemdisj  7721  suplocexprlemloc  7722  suplocexprlemub  7724  recexgt0sr  7774  archsr  7783  map2psrprg  7806  suplocsrlemb  7807  axprecex  7881  nntopi  7895  axpre-suploclemres  7902  axpre-suploc  7903  cnegex  8137  apreap  8546  recexap  8612  sup3exmid  8916  creur  8918  creui  8919  cju  8920  supinfneg  9597  infsupneg  9598  exbtwnzlemshrink  10251  rebtwn2zlemshrink  10256  modqmuladd  10368  hashunlem  10786  shftfvalg  10829  shftfval  10832  rexfiuz  11000  recvguniq  11006  fimaxre2  11237  clim  11291  sumeq1  11365  summodc  11393  fsum3  11397  mertenslemub  11544  mertenslemi1  11545  mertenslem2  11546  mertensabs  11547  prodeq1f  11562  prodeq2w  11566  prodmodc  11588  fprodseq  11593  divides  11798  odd2np1lem  11879  opeo  11904  omeo  11905  divalglemeunn  11928  divalglemeuneg  11930  infssuzex  11952  nninfdcex  11956  zeqzmulgcd  11973  bezoutlemnewy  11999  bezoutlemmain  12001  bezoutlemex  12004  bezoutlemaz  12006  exprmfct  12140  nnnn0modprm0  12257  pceu  12297  pcprmpw2  12334  ennnfoneleminc  12414  ennnfonelemex  12417  ennnfonelemhom  12418  ennnfonelemnn0  12425  ennnfonelemr  12426  ctinfomlemom  12430  ctinfom  12431  nninfdclemcl  12451  nninfdclemp1  12453  nninfdc  12456  ptex  12718  grprinvlem  12809  isnsgrp  12817  grpinvex  12892  dfgrp2  12907  grpidinv2  12933  grpidinv  12934  dfgrp3mlem  12973  grp1  12981  dvdsrd  13268  opprunitd  13284  subrgdvds  13361  lss1d  13475  basis2  13587  eltg2  13592  tg2  13599  neival  13682  isnei  13683  isneip  13685  restbasg  13707  cnpval  13737  iscnp  13738  icnpimaex  13750  lmbr  13752  lmbr2  13753  cnptoprest2  13779  lmff  13788  txbas  13797  txcnp  13810  txrest  13815  blssps  13966  blss  13967  mopni  14021  metss  14033  metrest  14045  metcnp3  14050  divcnap  14094  cncfval  14098  elcncf2  14100  cncfmet  14118  dedekindeulemuub  14134  dedekindeulemloc  14136  dedekindeulemlu  14138  suplociccreex  14141  dedekindicclemuub  14143  dedekindicclemloc  14145  dedekindicclemlu  14147  limccl  14167  ellimc3apf  14168  limcdifap  14170  limcmpted  14171  bj-inf2vnlem1  14761  bj-inf2vnlem2  14762  bj-nn0sucALT  14769  sscoll2  14779  subctctexmid  14789  pw1nct  14791  isomninnlem  14817  trilpolemlt1  14828  trirec0  14831  ismkvnnlem  14839