Theorem rexbidv 2531

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

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

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-rex 2514

This theorem is referenced by:  rexbii  2537  2rexbidv  2555  rexralbidv  2556  rexeqbi1dv  2741  rexeqbidv  2745  cbvrex2vw  2777  cbvrex2v  2779  rspc2ev  2922  rspc3ev  2924  ceqsrex2v  2935  sbcrext  3106  uniiunlem  3313  eliun  3969  dfiin2g  3998  dfiunv2  4001  nn0suc  4696  rexxpf  4869  elrnmpt  4973  elrnmptg  4976  elimag  5072  funcnvuni  5390  fun11iun  5595  fvelrnb  5683  fvelimab  5692  foco2  5883  elabrex  5887  elabrexg  5888  abrexco  5889  f1oiso  5956  f1oiso2  5957  acexmidlemab  6001  acexmidlemcase  6002  abrexex2g  6271  abrexex2  6275  recseq  6458  tfr0dm  6474  tfr1onlemaccex  6500  tfrcllemsucaccv  6506  tfrcllembxssdm  6508  tfrcllemaccex  6513  tfrcllemres  6514  freceq1  6544  frec0g  6549  freccllem  6554  frecfcllem  6556  frecsuclem  6558  frecsuc  6559  nnaordex  6682  qseq2  6739  elqsg  6740  elixpsn  6890  ixpsnf1o  6891  isfi  6920  enfi  7043  fimax2gtri  7072  elfi  7149  supeq3  7168  supmoti  7171  suplubti  7178  supisolem  7186  cnvinfex  7196  eqinfti  7198  infvalti  7200  infglbti  7203  enomnilem  7316  finomni  7318  exmidomni  7320  fodjum  7324  fodju0  7325  fodjuomnilemres  7326  fodjuomni  7327  ismkvnex  7333  fodjumkvlemres  7337  fodjumkv  7338  enmkvlem  7339  ltexnqq  7606  elinp  7672  prnmaxl  7686  prnminu  7687  prarloclem3  7695  ltdfpr  7704  genpdflem  7705  genipv  7707  genpassl  7722  genpassu  7723  ltexprlemm  7798  ltexprlemloc  7805  cauappcvgprlemm  7843  cauappcvgprlemopl  7844  cauappcvgprlemlol  7845  cauappcvgprlemopu  7846  cauappcvgprlemupu  7847  cauappcvgprlemdisj  7849  cauappcvgprlemloc  7850  cauappcvgprlemladdfu  7852  cauappcvgprlemladdfl  7853  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  cauappcvgprlem1  7857  cauappcvgprlem2  7858  caucvgprlemm  7866  caucvgprlemopl  7867  caucvgprlemlol  7868  caucvgprlemopu  7869  caucvgprlemupu  7870  caucvgprlemdisj  7872  caucvgprlemloc  7873  caucvgprlemladdfu  7875  caucvgprlemladdrl  7876  caucvgprlem1  7877  caucvgprlem2  7878  caucvgprprlemell  7883  caucvgprprlemelu  7884  caucvgprprlemml  7892  caucvgprprlemmu  7893  caucvgprprlemexbt  7904  caucvgprprlem2  7908  suplocexprlemmu  7916  suplocexprlemru  7917  suplocexprlemdisj  7918  suplocexprlemloc  7919  suplocexprlemub  7921  recexgt0sr  7971  archsr  7980  map2psrprg  8003  suplocsrlemb  8004  axprecex  8078  nntopi  8092  axpre-suploclemres  8099  axpre-suploc  8100  cnegex  8335  apreap  8745  recexap  8811  sup3exmid  9115  creur  9117  creui  9118  cju  9119  supinfneg  9802  infsupneg  9803  infssuzex  10465  nninfdcex  10469  exbtwnzlemshrink  10480  rebtwn2zlemshrink  10485  modqmuladd  10600  hashunlem  11038  iswrd  11086  csbwrdg  11114  shftfvalg  11345  shftfval  11348  rexfiuz  11516  recvguniq  11522  fimaxre2  11754  clim  11808  sumeq1  11882  summodc  11910  fsum3  11914  mertenslemub  12061  mertenslemi1  12062  mertenslem2  12063  mertensabs  12064  prodeq1f  12079  prodeq2w  12083  prodmodc  12105  fprodseq  12110  divides  12316  odd2np1lem  12399  opeo  12424  omeo  12425  divalglemeunn  12448  divalglemeuneg  12450  zeqzmulgcd  12507  bezoutlemnewy  12533  bezoutlemmain  12535  bezoutlemex  12538  bezoutlemaz  12540  exprmfct  12676  nnnn0modprm0  12794  pceu  12834  pcprmpw2  12872  4sqlemafi  12934  4sqexercise1  12937  4sqlem12  12941  ennnfoneleminc  12998  ennnfonelemex  13001  ennnfonelemhom  13002  ennnfonelemnn0  13009  ennnfonelemr  13010  ctinfomlemom  13014  ctinfom  13015  nninfdclemcl  13035  nninfdclemp1  13037  nninfdc  13040  ptex  13313  grpinvalem  13434  igsumvalx  13438  gsumpropd  13441  gsumress  13444  gsum0g  13445  isnsgrp  13455  grpinvex  13559  dfgrp2  13576  grpidinv2  13607  grpidinv  13608  dfgrp3mlem  13647  grp1  13655  imasgrp2  13663  dvdsrd  14074  opprunitd  14090  subrgdvds  14215  lss1d  14363  lspsn  14396  ellspsn  14397  rspsn  14514  znf1o  14631  basis2  14738  eltg2  14743  tg2  14750  neival  14833  isnei  14834  isneip  14836  restbasg  14858  cnpval  14888  iscnp  14889  icnpimaex  14901  lmbr  14903  lmbr2  14904  cnptoprest2  14930  lmff  14939  txbas  14948  txcnp  14961  txrest  14966  blssps  15117  blss  15118  mopni  15172  metss  15184  metrest  15196  metcnp3  15201  divcnap  15255  cncfval  15262  elcncf2  15264  cncfmet  15282  dedekindeulemuub  15307  dedekindeulemloc  15309  dedekindeulemlu  15311  suplociccreex  15314  dedekindicclemuub  15316  dedekindicclemloc  15318  dedekindicclemlu  15320  ivthreinc  15335  limccl  15349  ellimc3apf  15350  limcdifap  15352  limcmpted  15353  plyval  15422  elply2  15425  2lgslem1b  15784  upgredg2vtx  15962  usgredg4  16029  ushgredgedg  16040  ushgredgedgloop  16042  vtxd0nedgbfi  16059  bj-inf2vnlem1  16416  bj-inf2vnlem2  16417  bj-nn0sucALT  16424  sscoll2  16434  3dom  16439  subctctexmid  16453  pw1nct  16456  isomninnlem  16486  trilpolemlt1  16497  trirec0  16500  ismkvnnlem  16508