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  4751  rexxpf  4927  elrnmpt  5031  elrnmptg  5034  elimag  5130  funcnvuni  5450  fun11iun  5660  fvelrnb  5750  fvelimab  5759  foco2  5959  elabrex  5963  elabrexg  5964  abrexco  5965  f1oiso  6032  f1oiso2  6033  acexmidlemab  6079  acexmidlemcase  6080  abrexex2g  6349  abrexex2  6353  elabreximd  6356  recseq  6577  tfr0dm  6593  tfr1onlemaccex  6619  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllemaccex  6632  tfrcllemres  6633  freceq1  6663  frec0g  6668  freccllem  6673  frecfcllem  6675  frecsuclem  6677  frecsuc  6678  nnaordex  6801  qseq2  6858  elqsg  6859  elixpsn  7017  ixpsnf1o  7018  isfi  7047  enfi  7175  fimax2gtri  7206  elfi  7305  supeq3  7330  supmoti  7333  suplubti  7340  supisolem  7348  cnvinfex  7358  eqinfti  7360  infvalti  7362  infglbti  7365  enomnilem  7478  finomni  7480  exmidomni  7482  fodjum  7486  fodju0  7487  fodjuomnilemres  7488  fodjuomni  7489  ismkvnex  7495  fodjumkvlemres  7499  fodjumkv  7500  enmkvlem  7501  ltexnqq  7775  elinp  7841  prnmaxl  7855  prnminu  7856  prarloclem3  7864  ltdfpr  7873  genpdflem  7874  genipv  7876  genpassl  7891  genpassu  7892  ltexprlemm  7967  ltexprlemloc  7974  cauappcvgprlemm  8012  cauappcvgprlemopl  8013  cauappcvgprlemlol  8014  cauappcvgprlemopu  8015  cauappcvgprlemupu  8016  cauappcvgprlemdisj  8018  cauappcvgprlemloc  8019  cauappcvgprlemladdfu  8021  cauappcvgprlemladdfl  8022  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  cauappcvgprlem1  8026  cauappcvgprlem2  8027  caucvgprlemm  8035  caucvgprlemopl  8036  caucvgprlemlol  8037  caucvgprlemopu  8038  caucvgprlemupu  8039  caucvgprlemdisj  8041  caucvgprlemloc  8042  caucvgprlemladdfu  8044  caucvgprlemladdrl  8045  caucvgprlem1  8046  caucvgprlem2  8047  caucvgprprlemell  8052  caucvgprprlemelu  8053  caucvgprprlemml  8061  caucvgprprlemmu  8062  caucvgprprlemexbt  8073  caucvgprprlem2  8077  suplocexprlemmu  8085  suplocexprlemru  8086  suplocexprlemdisj  8087  suplocexprlemloc  8088  suplocexprlemub  8090  recexgt0sr  8140  archsr  8149  map2psrprg  8172  suplocsrlemb  8173  axprecex  8247  nntopi  8261  axpre-suploclemres  8268  axpre-suploc  8269  cnegex  8504  apreap  8915  recexap  8981  sup3exmid  9287  creur  9289  creui  9290  cju  9291  supinfneg  9995  infsupneg  9996  infssuzex  10666  nninfdcex  10672  exbtwnzlemshrink  10683  rebtwn2zlemshrink  10688  modqmuladd  10803  hashunlem  11244  iswrd  11306  csbwrdg  11334  shftfvalg  11583  shftfval  11586  rexfiuz  11755  recvguniq  11761  fimaxre2  11993  clim  12047  sumeq1  12121  summodc  12150  fsum3  12154  mertenslemub  12301  mertenslemi1  12302  mertenslem2  12303  mertensabs  12304  prodeq1f  12319  prodeq2w  12323  prodmodc  12345  fprodseq  12350  divides  12556  odd2np1lem  12639  opeo  12664  omeo  12665  divalglemeunn  12688  divalglemeuneg  12690  zeqzmulgcd  12747  bezoutlemnewy  12773  bezoutlemmain  12775  bezoutlemex  12778  bezoutlemaz  12780  exprmfct  12916  nnnn0modprm0  13034  pceu  13074  pcprmpw2  13112  4sqlemafi  13174  4sqexercise1  13177  4sqlem12  13181  ennnfoneleminc  13302  ennnfonelemex  13305  ennnfonelemhom  13306  ennnfonelemnn0  13313  ennnfonelemr  13314  ctinfomlemom  13318  ctinfom  13319  nninfdclemcl  13339  nninfdclemp1  13341  nninfdc  13344  ptex  13618  grpinvalem  13705  gzsumvalx  13709  gzsumress  13712  gzsum0  13713  isnsgrp  13721  grpinvex  13815  dfgrp2  13832  grpidinv2  13863  grpidinv  13864  dfgrp3mlem  13903  grp1  13911  imasgrp2  13913  dvdsrd  14401  opprunitd  14417  subrgdvds  14543  lss1d  14720  lspsn  14753  ellspsn  14754  rspsn  14871  znf1o  14986  basis2  15149  eltg2  15154  tg2  15161  neival  15244  isnei  15245  isneip  15247  restbasg  15269  cnpval  15299  iscnp  15300  icnpimaex  15312  lmbr  15314  lmbr2  15315  cnptoprest2  15341  lmff  15350  txbas  15359  txcnp  15372  txrest  15377  blssps  15528  blss  15529  mopni  15583  metss  15595  metrest  15607  metcnp3  15612  divcnap  15666  cncfval  15673  elcncf2  15675  cncfmet  15693  dedekindeulemuub  15718  dedekindeulemloc  15720  dedekindeulemlu  15722  suplociccreex  15725  dedekindicclemuub  15727  dedekindicclemloc  15729  dedekindicclemlu  15731  ivthreinc  15746  limccl  15760  ellimc3apf  15761  limcdifap  15763  limcmpted  15764  plyval  15833  elply2  15836  2lgslem1b  16208  upgredg2vtx  16389  usgredg4  16456  ushgredgedg  16467  ushgredgedgloop  16469  vtxd0nedgbfi  16540  bj-inf2vnlem1  16996  bj-inf2vnlem2  16997  bj-nn0sucALT  17004  sscoll2  17014  3dom  17018  subctctexmid  17030  pw1nct  17033  isomninnlem  17079  trilpolemlt1  17090  trirec0  17093  qdiff  17098  ismkvnnlem  17102