Theorem rexbidv 2533

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

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

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-rex 2516

This theorem is referenced by:  rexbii  2539  2rexbidv  2557  rexralbidv  2558  rexeqbi1dv  2743  rexeqbidv  2747  cbvrex2vw  2779  cbvrex2v  2781  rspc2ev  2925  rspc3ev  2927  ceqsrex2v  2938  sbcrext  3109  uniiunlem  3316  eliun  3974  dfiin2g  4003  dfiunv2  4006  nn0suc  4702  rexxpf  4877  elrnmpt  4981  elrnmptg  4984  elimag  5080  funcnvuni  5399  fun11iun  5604  fvelrnb  5693  fvelimab  5702  foco2  5894  elabrex  5898  elabrexg  5899  abrexco  5900  f1oiso  5967  f1oiso2  5968  acexmidlemab  6012  acexmidlemcase  6013  abrexex2g  6282  abrexex2  6286  recseq  6472  tfr0dm  6488  tfr1onlemaccex  6514  tfrcllemsucaccv  6520  tfrcllembxssdm  6522  tfrcllemaccex  6527  tfrcllemres  6528  freceq1  6558  frec0g  6563  freccllem  6568  frecfcllem  6570  frecsuclem  6572  frecsuc  6573  nnaordex  6696  qseq2  6753  elqsg  6754  elixpsn  6904  ixpsnf1o  6905  isfi  6934  enfi  7060  fimax2gtri  7091  elfi  7170  supeq3  7189  supmoti  7192  suplubti  7199  supisolem  7207  cnvinfex  7217  eqinfti  7219  infvalti  7221  infglbti  7224  enomnilem  7337  finomni  7339  exmidomni  7341  fodjum  7345  fodju0  7346  fodjuomnilemres  7347  fodjuomni  7348  ismkvnex  7354  fodjumkvlemres  7358  fodjumkv  7359  enmkvlem  7360  ltexnqq  7628  elinp  7694  prnmaxl  7708  prnminu  7709  prarloclem3  7717  ltdfpr  7726  genpdflem  7727  genipv  7729  genpassl  7744  genpassu  7745  ltexprlemm  7820  ltexprlemloc  7827  cauappcvgprlemm  7865  cauappcvgprlemopl  7866  cauappcvgprlemlol  7867  cauappcvgprlemopu  7868  cauappcvgprlemupu  7869  cauappcvgprlemdisj  7871  cauappcvgprlemloc  7872  cauappcvgprlemladdfu  7874  cauappcvgprlemladdfl  7875  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  cauappcvgprlem1  7879  cauappcvgprlem2  7880  caucvgprlemm  7888  caucvgprlemopl  7889  caucvgprlemlol  7890  caucvgprlemopu  7891  caucvgprlemupu  7892  caucvgprlemdisj  7894  caucvgprlemloc  7895  caucvgprlemladdfu  7897  caucvgprlemladdrl  7898  caucvgprlem1  7899  caucvgprlem2  7900  caucvgprprlemell  7905  caucvgprprlemelu  7906  caucvgprprlemml  7914  caucvgprprlemmu  7915  caucvgprprlemexbt  7926  caucvgprprlem2  7930  suplocexprlemmu  7938  suplocexprlemru  7939  suplocexprlemdisj  7940  suplocexprlemloc  7941  suplocexprlemub  7943  recexgt0sr  7993  archsr  8002  map2psrprg  8025  suplocsrlemb  8026  axprecex  8100  nntopi  8114  axpre-suploclemres  8121  axpre-suploc  8122  cnegex  8357  apreap  8767  recexap  8833  sup3exmid  9137  creur  9139  creui  9140  cju  9141  supinfneg  9829  infsupneg  9830  infssuzex  10494  nninfdcex  10498  exbtwnzlemshrink  10509  rebtwn2zlemshrink  10514  modqmuladd  10629  hashunlem  11068  iswrd  11119  csbwrdg  11147  shftfvalg  11396  shftfval  11399  rexfiuz  11567  recvguniq  11573  fimaxre2  11805  clim  11859  sumeq1  11933  summodc  11962  fsum3  11966  mertenslemub  12113  mertenslemi1  12114  mertenslem2  12115  mertensabs  12116  prodeq1f  12131  prodeq2w  12135  prodmodc  12157  fprodseq  12162  divides  12368  odd2np1lem  12451  opeo  12476  omeo  12477  divalglemeunn  12500  divalglemeuneg  12502  zeqzmulgcd  12559  bezoutlemnewy  12585  bezoutlemmain  12587  bezoutlemex  12590  bezoutlemaz  12592  exprmfct  12728  nnnn0modprm0  12846  pceu  12886  pcprmpw2  12924  4sqlemafi  12986  4sqexercise1  12989  4sqlem12  12993  ennnfoneleminc  13050  ennnfonelemex  13053  ennnfonelemhom  13054  ennnfonelemnn0  13061  ennnfonelemr  13062  ctinfomlemom  13066  ctinfom  13067  nninfdclemcl  13087  nninfdclemp1  13089  nninfdc  13092  ptex  13365  grpinvalem  13486  igsumvalx  13490  gsumpropd  13493  gsumress  13496  gsum0g  13497  isnsgrp  13507  grpinvex  13611  dfgrp2  13628  grpidinv2  13659  grpidinv  13660  dfgrp3mlem  13699  grp1  13707  imasgrp2  13715  dvdsrd  14127  opprunitd  14143  subrgdvds  14268  lss1d  14416  lspsn  14449  ellspsn  14450  rspsn  14567  znf1o  14684  basis2  14791  eltg2  14796  tg2  14803  neival  14886  isnei  14887  isneip  14889  restbasg  14911  cnpval  14941  iscnp  14942  icnpimaex  14954  lmbr  14956  lmbr2  14957  cnptoprest2  14983  lmff  14992  txbas  15001  txcnp  15014  txrest  15019  blssps  15170  blss  15171  mopni  15225  metss  15237  metrest  15249  metcnp3  15254  divcnap  15308  cncfval  15315  elcncf2  15317  cncfmet  15335  dedekindeulemuub  15360  dedekindeulemloc  15362  dedekindeulemlu  15364  suplociccreex  15367  dedekindicclemuub  15369  dedekindicclemloc  15371  dedekindicclemlu  15373  ivthreinc  15388  limccl  15402  ellimc3apf  15403  limcdifap  15405  limcmpted  15406  plyval  15475  elply2  15478  2lgslem1b  15837  upgredg2vtx  16018  usgredg4  16085  ushgredgedg  16096  ushgredgedgloop  16098  vtxd0nedgbfi  16169  bj-inf2vnlem1  16616  bj-inf2vnlem2  16617  bj-nn0sucALT  16624  sscoll2  16634  3dom  16638  subctctexmid  16652  pw1nct  16655  isomninnlem  16685  trilpolemlt1  16696  trirec0  16699  qdiff  16704  ismkvnnlem  16708