Theorem rexbidv 2545

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 2543	1 |- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )

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

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 2528

This theorem is referenced by:  rexbii  2551  2rexbidv  2569  rexralbidv  2570  rexeqbi1dv  2756  rexeqbidv  2760  cbvrex2vw  2792  cbvrex2v  2794  rspc2ev  2939  rspc3ev  2941  ceqsrex2v  2952  sbcrext  3123  uniiunlem  3332  eliun  4000  dfiin2g  4029  dfiunv2  4032  nn0suc  4731  rexxpf  4907  elrnmpt  5011  elrnmptg  5014  elimag  5110  funcnvuni  5430  fun11iun  5640  fvelrnb  5729  fvelimab  5738  foco2  5932  elabrex  5936  elabrexg  5937  abrexco  5938  f1oiso  6005  f1oiso2  6006  acexmidlemab  6052  acexmidlemcase  6053  abrexex2g  6322  abrexex2  6326  elabreximd  6329  recseq  6550  tfr0dm  6566  tfr1onlemaccex  6592  tfrcllemsucaccv  6598  tfrcllembxssdm  6600  tfrcllemaccex  6605  tfrcllemres  6606  freceq1  6636  frec0g  6641  freccllem  6646  frecfcllem  6648  frecsuclem  6650  frecsuc  6651  nnaordex  6774  qseq2  6831  elqsg  6832  elixpsn  6983  ixpsnf1o  6984  isfi  7013  enfi  7141  fimax2gtri  7172  elfi  7271  supeq3  7294  supmoti  7297  suplubti  7304  supisolem  7312  cnvinfex  7322  eqinfti  7324  infvalti  7326  infglbti  7329  enomnilem  7442  finomni  7444  exmidomni  7446  fodjum  7450  fodju0  7451  fodjuomnilemres  7452  fodjuomni  7453  ismkvnex  7459  fodjumkvlemres  7463  fodjumkv  7464  enmkvlem  7465  ltexnqq  7739  elinp  7805  prnmaxl  7819  prnminu  7820  prarloclem3  7828  ltdfpr  7837  genpdflem  7838  genipv  7840  genpassl  7855  genpassu  7856  ltexprlemm  7931  ltexprlemloc  7938  cauappcvgprlemm  7976  cauappcvgprlemopl  7977  cauappcvgprlemlol  7978  cauappcvgprlemopu  7979  cauappcvgprlemupu  7980  cauappcvgprlemdisj  7982  cauappcvgprlemloc  7983  cauappcvgprlemladdfu  7985  cauappcvgprlemladdfl  7986  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  cauappcvgprlem1  7990  cauappcvgprlem2  7991  caucvgprlemm  7999  caucvgprlemopl  8000  caucvgprlemlol  8001  caucvgprlemopu  8002  caucvgprlemupu  8003  caucvgprlemdisj  8005  caucvgprlemloc  8006  caucvgprlemladdfu  8008  caucvgprlemladdrl  8009  caucvgprlem1  8010  caucvgprlem2  8011  caucvgprprlemell  8016  caucvgprprlemelu  8017  caucvgprprlemml  8025  caucvgprprlemmu  8026  caucvgprprlemexbt  8037  caucvgprprlem2  8041  suplocexprlemmu  8049  suplocexprlemru  8050  suplocexprlemdisj  8051  suplocexprlemloc  8052  suplocexprlemub  8054  recexgt0sr  8104  archsr  8113  map2psrprg  8136  suplocsrlemb  8137  axprecex  8211  nntopi  8225  axpre-suploclemres  8232  axpre-suploc  8233  cnegex  8467  apreap  8878  recexap  8944  sup3exmid  9248  creur  9250  creui  9251  cju  9252  supinfneg  9945  infsupneg  9946  infssuzex  10615  nninfdcex  10621  exbtwnzlemshrink  10632  rebtwn2zlemshrink  10637  modqmuladd  10752  hashunlem  11193  iswrd  11251  csbwrdg  11279  shftfvalg  11528  shftfval  11531  rexfiuz  11699  recvguniq  11705  fimaxre2  11937  clim  11991  sumeq1  12065  summodc  12094  fsum3  12098  mertenslemub  12245  mertenslemi1  12246  mertenslem2  12247  mertensabs  12248  prodeq1f  12263  prodeq2w  12267  prodmodc  12289  fprodseq  12294  divides  12500  odd2np1lem  12583  opeo  12608  omeo  12609  divalglemeunn  12632  divalglemeuneg  12634  zeqzmulgcd  12691  bezoutlemnewy  12717  bezoutlemmain  12719  bezoutlemex  12722  bezoutlemaz  12724  exprmfct  12860  nnnn0modprm0  12978  pceu  13018  pcprmpw2  13056  4sqlemafi  13118  4sqexercise1  13121  4sqlem12  13125  ennnfoneleminc  13246  ennnfonelemex  13249  ennnfonelemhom  13250  ennnfonelemnn0  13257  ennnfonelemr  13258  ctinfomlemom  13262  ctinfom  13263  nninfdclemcl  13283  nninfdclemp1  13285  nninfdc  13288  ptex  13561  grpinvalem  13648  igsumvalx  13652  gsumpropd  13655  gsumress  13658  gsum0g  13659  isnsgrp  13669  grpinvex  13765  dfgrp2  13782  grpidinv2  13813  grpidinv  13814  dfgrp3mlem  13853  grp1  13861  imasgrp2  13863  dvdsrd  14339  opprunitd  14355  subrgdvds  14481  lss1d  14657  lspsn  14690  ellspsn  14691  rspsn  14808  znf1o  14925  basis2  15039  eltg2  15044  tg2  15051  neival  15134  isnei  15135  isneip  15137  restbasg  15159  cnpval  15189  iscnp  15190  icnpimaex  15202  lmbr  15204  lmbr2  15205  cnptoprest2  15231  lmff  15240  txbas  15249  txcnp  15262  txrest  15267  blssps  15418  blss  15419  mopni  15473  metss  15485  metrest  15497  metcnp3  15502  divcnap  15556  cncfval  15563  elcncf2  15565  cncfmet  15583  dedekindeulemuub  15608  dedekindeulemloc  15610  dedekindeulemlu  15612  suplociccreex  15615  dedekindicclemuub  15617  dedekindicclemloc  15619  dedekindicclemlu  15621  ivthreinc  15636  limccl  15650  ellimc3apf  15651  limcdifap  15653  limcmpted  15654  plyval  15723  elply2  15726  2lgslem1b  16088  upgredg2vtx  16269  usgredg4  16336  ushgredgedg  16347  ushgredgedgloop  16349  vtxd0nedgbfi  16420  bj-inf2vnlem1  16866  bj-inf2vnlem2  16867  bj-nn0sucALT  16874  sscoll2  16884  3dom  16888  subctctexmid  16900  pw1nct  16903  isomninnlem  16940  trilpolemlt1  16951  trirec0  16954  qdiff  16959  ismkvnnlem  16963