Theorem rexbidv 2551

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

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   E.wrex 2529

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587

This proof depends on definitions:  df-bi 117  df-nf 1514  df-rex 2534

This theorem is used by:  rexbii  2557  2rexbidv  2575  rexralbidv  2576  rexeqbi1dv  2762  rexeqbidv  2766  cbvrex2vw  2798  cbvrex2v  2800  rspc2ev  2945  rspc3ev  2947  ceqsrex2v  2958  sbcrext  3129  uniiunlem  3338  eliun  4016  dfiin2g  4045  dfiunv2  4048  nn0suc  4753  rexxpf  4929  elrnmpt  5033  elrnmptg  5036  elimag  5133  funcnvuni  5453  fun11iun  5663  fvelrnb  5753  fvelimab  5762  foco2  5962  elabrex  5966  elabrexg  5967  abrexco  5968  f1oiso  6035  f1oiso2  6036  acexmidlemab  6082  acexmidlemcase  6083  abrexex2g  6353  abrexex2  6357  elabreximd  6360  recseq  6582  tfr0dm  6598  tfr1onlemaccex  6624  tfrcllemsucaccv  6630  tfrcllembxssdm  6632  tfrcllemaccex  6637  tfrcllemres  6638  freceq1  6668  frec0g  6673  freccllem  6678  frecfcllem  6680  frecsuclem  6682  frecsuc  6683  nnaordex  6806  qseq2  6863  elqsg  6864  elixpsn  7023  ixpsnf1o  7024  isfi  7053  enfi  7181  fimax2gtri  7212  elfi  7310  supeq3  7336  supmoti  7339  suplubti  7346  supisolem  7354  cnvinfex  7364  eqinfti  7366  infvalti  7368  infglbti  7371  enomnilem  7484  finomni  7486  exmidomni  7488  fodjum  7492  fodju0  7493  fodjuomnilemres  7494  fodjuomni  7495  ismkvnex  7501  fodjumkvlemres  7505  fodjumkv  7506  enmkvlem  7507  ltexnqq  7781  elinp  7847  prnmaxl  7861  prnminu  7862  prarloclem3  7870  ltdfpr  7879  genpdflem  7880  genipv  7882  genpassl  7897  genpassu  7898  ltexprlemm  7973  ltexprlemloc  7980  cauappcvgprlemm  8018  cauappcvgprlemopl  8019  cauappcvgprlemlol  8020  cauappcvgprlemopu  8021  cauappcvgprlemupu  8022  cauappcvgprlemdisj  8024  cauappcvgprlemloc  8025  cauappcvgprlemladdfu  8027  cauappcvgprlemladdfl  8028  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  cauappcvgprlem1  8032  cauappcvgprlem2  8033  caucvgprlemm  8041  caucvgprlemopl  8042  caucvgprlemlol  8043  caucvgprlemopu  8044  caucvgprlemupu  8045  caucvgprlemdisj  8047  caucvgprlemloc  8048  caucvgprlemladdfu  8050  caucvgprlemladdrl  8051  caucvgprlem1  8052  caucvgprlem2  8053  caucvgprprlemell  8058  caucvgprprlemelu  8059  caucvgprprlemml  8067  caucvgprprlemmu  8068  caucvgprprlemexbt  8079  caucvgprprlem2  8083  suplocexprlemmu  8091  suplocexprlemru  8092  suplocexprlemdisj  8093  suplocexprlemloc  8094  suplocexprlemub  8096  recexgt0sr  8146  archsr  8155  map2psrprg  8178  suplocsrlemb  8179  axprecex  8253  nntopi  8267  axpre-suploclemres  8274  axpre-suploc  8275  cnegex  8511  apreap  8923  recexap  8989  sup3exmid  9295  creur  9297  creui  9298  cju  9299  supinfneg  10010  infsupneg  10011  infssuzex  10682  nninfdcex  10688  exbtwnzlemshrink  10699  rebtwn2zlemshrink  10704  modqmuladd  10823  hashunlem  11265  iswrd  11327  csbwrdg  11355  shftfvalg  11604  shftfval  11607  rexfiuz  11776  recvguniq  11782  fimaxre2  12015  fiidxsupcl  12017  clim  12071  sumeq1  12145  summodc  12174  fsum3  12178  mertenslemub  12325  mertenslemi1  12326  mertenslem2  12327  mertensabs  12328  prodeq1f  12343  prodeq2w  12347  prodmodc  12369  fprodseq  12374  divides  12580  odd2np1lem  12663  opeo  12688  omeo  12689  divalglemeunn  12712  divalglemeuneg  12714  zeqzmulgcd  12771  bezoutlemnewy  12797  bezoutlemmain  12799  bezoutlemex  12802  bezoutlemaz  12804  exprmfct  12941  nnnn0modprm0  13062  pceu  13102  pcprmpw2  13140  4sqlemafi  13202  4sqexercise1  13205  4sqlem12  13209  ennnfoneleminc  13359  ennnfonelemex  13362  ennnfonelemhom  13363  ennnfonelemnn0  13370  ennnfonelemr  13371  ctinfomlemom  13375  ctinfom  13376  nninfdclemcl  13396  nninfdclemp1  13398  nninfdc  13401  ptex  13676  grpinvalem  13763  gzsumvalx  13767  gzsumress  13770  gzsum0  13771  isnsgrp  13779  grpinvex  13873  dfgrp2  13890  grpidinv2  13921  grpidinv  13922  dfgrp3mlem  13961  grp1  13969  imasgrp2  13971  dvdsrd  14509  opprunitd  14525  subrgdvds  14651  lss1d  14828  lspsn  14861  ellspsn  14862  rspsn  14979  znf1o  15094  psrbagmaxlem1  15178  basis2  15291  eltg2  15296  tg2  15303  neival  15386  isnei  15387  isneip  15389  restbasg  15411  cnpval  15441  iscnp  15442  icnpimaex  15454  lmbr  15456  lmbr2  15457  cnptoprest2  15483  lmff  15492  txbas  15501  txcnp  15514  txrest  15519  blssps  15670  blss  15671  mopni  15725  metss  15737  metrest  15749  metcnp3  15754  divcnap  15808  cncfval  15815  elcncf2  15817  cncfmet  15835  dedekindeulemuub  15860  dedekindeulemloc  15862  dedekindeulemlu  15864  suplociccreex  15867  dedekindicclemuub  15869  dedekindicclemloc  15871  dedekindicclemlu  15873  ivthreinc  15888  limccl  15902  ellimc3apf  15903  limcdifap  15905  limcmpted  15906  plyval  15975  elply2  15978  2lgslem1b  16430  upgredg2vtx  16611  usgredg4  16678  ushgredgedg  16689  ushgredgedgloop  16691  vtxd0nedgbfi  16762  bj-inf2vnlem1  17218  bj-inf2vnlem2  17219  bj-nn0sucALT  17226  sscoll2  17236  3dom  17240  subctctexmid  17252  pw1nct  17255  isomninnlem  17302  trilpolemlt1  17314  trirec0  17317  qdiff  17322  ismkvnnlem  17326