Theorem rexbidv 2498

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

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

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-rex 2481

This theorem is referenced by:  rexbii  2504  2rexbidv  2522  rexralbidv  2523  rexeqbi1dv  2706  rexeqbidv  2710  cbvrex2vw  2741  cbvrex2v  2743  rspc2ev  2883  rspc3ev  2885  ceqsrex2v  2896  sbcrext  3067  uniiunlem  3272  eliun  3920  dfiin2g  3949  dfiunv2  3952  nn0suc  4640  rexxpf  4813  elrnmpt  4915  elrnmptg  4918  elimag  5013  funcnvuni  5327  fun11iun  5525  fvelrnb  5608  fvelimab  5617  foco2  5800  elabrex  5804  elabrexg  5805  abrexco  5806  f1oiso  5873  f1oiso2  5874  acexmidlemab  5916  acexmidlemcase  5917  abrexex2g  6177  abrexex2  6181  recseq  6364  tfr0dm  6380  tfr1onlemaccex  6406  tfrcllemsucaccv  6412  tfrcllembxssdm  6414  tfrcllemaccex  6419  tfrcllemres  6420  freceq1  6450  frec0g  6455  freccllem  6460  frecfcllem  6462  frecsuclem  6464  frecsuc  6465  nnaordex  6586  qseq2  6643  elqsg  6644  elixpsn  6794  ixpsnf1o  6795  isfi  6820  enfi  6934  fimax2gtri  6962  elfi  7037  supeq3  7056  supmoti  7059  suplubti  7066  supisolem  7074  cnvinfex  7084  eqinfti  7086  infvalti  7088  infglbti  7091  enomnilem  7204  finomni  7206  exmidomni  7208  fodjum  7212  fodju0  7213  fodjuomnilemres  7214  fodjuomni  7215  ismkvnex  7221  fodjumkvlemres  7225  fodjumkv  7226  enmkvlem  7227  ltexnqq  7475  elinp  7541  prnmaxl  7555  prnminu  7556  prarloclem3  7564  ltdfpr  7573  genpdflem  7574  genipv  7576  genpassl  7591  genpassu  7592  ltexprlemm  7667  ltexprlemloc  7674  cauappcvgprlemm  7712  cauappcvgprlemopl  7713  cauappcvgprlemlol  7714  cauappcvgprlemopu  7715  cauappcvgprlemupu  7716  cauappcvgprlemdisj  7718  cauappcvgprlemloc  7719  cauappcvgprlemladdfu  7721  cauappcvgprlemladdfl  7722  cauappcvgprlemladdru  7723  cauappcvgprlemladdrl  7724  cauappcvgprlem1  7726  cauappcvgprlem2  7727  caucvgprlemm  7735  caucvgprlemopl  7736  caucvgprlemlol  7737  caucvgprlemopu  7738  caucvgprlemupu  7739  caucvgprlemdisj  7741  caucvgprlemloc  7742  caucvgprlemladdfu  7744  caucvgprlemladdrl  7745  caucvgprlem1  7746  caucvgprlem2  7747  caucvgprprlemell  7752  caucvgprprlemelu  7753  caucvgprprlemml  7761  caucvgprprlemmu  7762  caucvgprprlemexbt  7773  caucvgprprlem2  7777  suplocexprlemmu  7785  suplocexprlemru  7786  suplocexprlemdisj  7787  suplocexprlemloc  7788  suplocexprlemub  7790  recexgt0sr  7840  archsr  7849  map2psrprg  7872  suplocsrlemb  7873  axprecex  7947  nntopi  7961  axpre-suploclemres  7968  axpre-suploc  7969  cnegex  8204  apreap  8614  recexap  8680  sup3exmid  8984  creur  8986  creui  8987  cju  8988  supinfneg  9669  infsupneg  9670  infssuzex  10323  nninfdcex  10327  exbtwnzlemshrink  10338  rebtwn2zlemshrink  10343  modqmuladd  10458  hashunlem  10896  iswrd  10937  csbwrdg  10964  shftfvalg  10983  shftfval  10986  rexfiuz  11154  recvguniq  11160  fimaxre2  11392  clim  11446  sumeq1  11520  summodc  11548  fsum3  11552  mertenslemub  11699  mertenslemi1  11700  mertenslem2  11701  mertensabs  11702  prodeq1f  11717  prodeq2w  11721  prodmodc  11743  fprodseq  11748  divides  11954  odd2np1lem  12037  opeo  12062  omeo  12063  divalglemeunn  12086  divalglemeuneg  12088  zeqzmulgcd  12137  bezoutlemnewy  12163  bezoutlemmain  12165  bezoutlemex  12168  bezoutlemaz  12170  exprmfct  12306  nnnn0modprm0  12424  pceu  12464  pcprmpw2  12502  4sqlemafi  12564  4sqexercise1  12567  4sqlem12  12571  ennnfoneleminc  12628  ennnfonelemex  12631  ennnfonelemhom  12632  ennnfonelemnn0  12639  ennnfonelemr  12640  ctinfomlemom  12644  ctinfom  12645  nninfdclemcl  12665  nninfdclemp1  12667  nninfdc  12670  ptex  12935  grpinvalem  13028  igsumvalx  13032  gsumpropd  13035  gsumress  13038  gsum0g  13039  isnsgrp  13049  grpinvex  13142  dfgrp2  13159  grpidinv2  13190  grpidinv  13191  dfgrp3mlem  13230  grp1  13238  imasgrp2  13240  dvdsrd  13650  opprunitd  13666  subrgdvds  13791  lss1d  13939  lspsn  13972  ellspsn  13973  rspsn  14090  znf1o  14207  basis2  14284  eltg2  14289  tg2  14296  neival  14379  isnei  14380  isneip  14382  restbasg  14404  cnpval  14434  iscnp  14435  icnpimaex  14447  lmbr  14449  lmbr2  14450  cnptoprest2  14476  lmff  14485  txbas  14494  txcnp  14507  txrest  14512  blssps  14663  blss  14664  mopni  14718  metss  14730  metrest  14742  metcnp3  14747  divcnap  14801  cncfval  14808  elcncf2  14810  cncfmet  14828  dedekindeulemuub  14853  dedekindeulemloc  14855  dedekindeulemlu  14857  suplociccreex  14860  dedekindicclemuub  14862  dedekindicclemloc  14864  dedekindicclemlu  14866  ivthreinc  14881  limccl  14895  ellimc3apf  14896  limcdifap  14898  limcmpted  14899  plyval  14968  elply2  14971  2lgslem1b  15330  bj-inf2vnlem1  15616  bj-inf2vnlem2  15617  bj-nn0sucALT  15624  sscoll2  15634  subctctexmid  15645  pw1nct  15647  isomninnlem  15674  trilpolemlt1  15685  trirec0  15688  ismkvnnlem  15696