Theorem rexbidv 2478

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

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

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-rex 2461

This theorem is referenced by:  rexbii  2484  2rexbidv  2502  rexralbidv  2503  rexeqbi1dv  2682  rexeqbidv  2686  cbvrex2vw  2716  cbvrex2v  2718  rspc2ev  2857  rspc3ev  2859  ceqsrex2v  2870  sbcrext  3041  uniiunlem  3245  eliun  3891  dfiin2g  3920  dfiunv2  3923  nn0suc  4604  rexxpf  4775  elrnmpt  4877  elrnmptg  4880  elimag  4975  funcnvuni  5286  fun11iun  5483  fvelrnb  5564  fvelimab  5573  foco2  5755  elabrex  5759  abrexco  5760  f1oiso  5827  f1oiso2  5828  acexmidlemab  5869  acexmidlemcase  5870  abrexex2g  6121  abrexex2  6125  recseq  6307  tfr0dm  6323  tfr1onlemaccex  6349  tfrcllemsucaccv  6355  tfrcllembxssdm  6357  tfrcllemaccex  6362  tfrcllemres  6363  freceq1  6393  frec0g  6398  freccllem  6403  frecfcllem  6405  frecsuclem  6407  frecsuc  6408  nnaordex  6529  qseq2  6584  elqsg  6585  elixpsn  6735  ixpsnf1o  6736  isfi  6761  enfi  6873  fimax2gtri  6901  elfi  6970  supeq3  6989  supmoti  6992  suplubti  6999  supisolem  7007  cnvinfex  7017  eqinfti  7019  infvalti  7021  infglbti  7024  enomnilem  7136  finomni  7138  exmidomni  7140  fodjum  7144  fodju0  7145  fodjuomnilemres  7146  fodjuomni  7147  ismkvnex  7153  fodjumkvlemres  7157  fodjumkv  7158  enmkvlem  7159  ltexnqq  7407  elinp  7473  prnmaxl  7487  prnminu  7488  prarloclem3  7496  ltdfpr  7505  genpdflem  7506  genipv  7508  genpassl  7523  genpassu  7524  ltexprlemm  7599  ltexprlemloc  7606  cauappcvgprlemm  7644  cauappcvgprlemopl  7645  cauappcvgprlemlol  7646  cauappcvgprlemopu  7647  cauappcvgprlemupu  7648  cauappcvgprlemdisj  7650  cauappcvgprlemloc  7651  cauappcvgprlemladdfu  7653  cauappcvgprlemladdfl  7654  cauappcvgprlemladdru  7655  cauappcvgprlemladdrl  7656  cauappcvgprlem1  7658  cauappcvgprlem2  7659  caucvgprlemm  7667  caucvgprlemopl  7668  caucvgprlemlol  7669  caucvgprlemopu  7670  caucvgprlemupu  7671  caucvgprlemdisj  7673  caucvgprlemloc  7674  caucvgprlemladdfu  7676  caucvgprlemladdrl  7677  caucvgprlem1  7678  caucvgprlem2  7679  caucvgprprlemell  7684  caucvgprprlemelu  7685  caucvgprprlemml  7693  caucvgprprlemmu  7694  caucvgprprlemexbt  7705  caucvgprprlem2  7709  suplocexprlemmu  7717  suplocexprlemru  7718  suplocexprlemdisj  7719  suplocexprlemloc  7720  suplocexprlemub  7722  recexgt0sr  7772  archsr  7781  map2psrprg  7804  suplocsrlemb  7805  axprecex  7879  nntopi  7893  axpre-suploclemres  7900  axpre-suploc  7901  cnegex  8135  apreap  8544  recexap  8610  sup3exmid  8914  creur  8916  creui  8917  cju  8918  supinfneg  9595  infsupneg  9596  exbtwnzlemshrink  10249  rebtwn2zlemshrink  10254  modqmuladd  10366  hashunlem  10784  shftfvalg  10827  shftfval  10830  rexfiuz  10998  recvguniq  11004  fimaxre2  11235  clim  11289  sumeq1  11363  summodc  11391  fsum3  11395  mertenslemub  11542  mertenslemi1  11543  mertenslem2  11544  mertensabs  11545  prodeq1f  11560  prodeq2w  11564  prodmodc  11586  fprodseq  11591  divides  11796  odd2np1lem  11877  opeo  11902  omeo  11903  divalglemeunn  11926  divalglemeuneg  11928  infssuzex  11950  nninfdcex  11954  zeqzmulgcd  11971  bezoutlemnewy  11997  bezoutlemmain  11999  bezoutlemex  12002  bezoutlemaz  12004  exprmfct  12138  nnnn0modprm0  12255  pceu  12295  pcprmpw2  12332  ennnfoneleminc  12412  ennnfonelemex  12415  ennnfonelemhom  12416  ennnfonelemnn0  12423  ennnfonelemr  12424  ctinfomlemom  12428  ctinfom  12429  nninfdclemcl  12449  nninfdclemp1  12451  nninfdc  12454  ptex  12713  grprinvlem  12804  isnsgrp  12812  grpinvex  12887  dfgrp2  12902  grpidinv2  12928  grpidinv  12929  dfgrp3mlem  12968  grp1  12976  dvdsrd  13263  opprunitd  13279  subrgdvds  13356  basis2  13551  eltg2  13556  tg2  13563  neival  13646  isnei  13647  isneip  13649  restbasg  13671  cnpval  13701  iscnp  13702  icnpimaex  13714  lmbr  13716  lmbr2  13717  cnptoprest2  13743  lmff  13752  txbas  13761  txcnp  13774  txrest  13779  blssps  13930  blss  13931  mopni  13985  metss  13997  metrest  14009  metcnp3  14014  divcnap  14058  cncfval  14062  elcncf2  14064  cncfmet  14082  dedekindeulemuub  14098  dedekindeulemloc  14100  dedekindeulemlu  14102  suplociccreex  14105  dedekindicclemuub  14107  dedekindicclemloc  14109  dedekindicclemlu  14111  limccl  14131  ellimc3apf  14132  limcdifap  14134  limcmpted  14135  bj-inf2vnlem1  14725  bj-inf2vnlem2  14726  bj-nn0sucALT  14733  sscoll2  14743  subctctexmid  14753  pw1nct  14755  isomninnlem  14781  trilpolemlt1  14792  trirec0  14795  ismkvnnlem  14803