ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  rexbidv GIF version

Theorem rexbidv 2465
Description: Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 20-Nov-1994.)
Hypothesis
Ref Expression
ralbidv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
rexbidv (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐴 𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem rexbidv
StepHypRef Expression
1 nfv 1515 . 2 𝑥𝜑
2 ralbidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2rexbid 2463 1 (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐴 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104  wrex 2443
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1434  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-4 1497  ax-17 1513  ax-ial 1521
This theorem depends on definitions:  df-bi 116  df-nf 1448  df-rex 2448
This theorem is referenced by:  rexbii  2471  2rexbidv  2489  rexralbidv  2490  rexeqbi1dv  2668  rexeqbidv  2672  cbvrex2vw  2702  cbvrex2v  2704  rspc2ev  2843  rspc3ev  2845  ceqsrex2v  2856  sbcrext  3026  uniiunlem  3229  eliun  3867  dfiin2g  3896  dfiunv2  3899  nn0suc  4578  rexxpf  4748  elrnmpt  4850  elrnmptg  4853  elimag  4947  funcnvuni  5254  fun11iun  5450  fvelrnb  5531  fvelimab  5539  foco2  5719  elabrex  5723  abrexco  5724  f1oiso  5791  f1oiso2  5792  acexmidlemab  5833  acexmidlemcase  5834  grprinvlem  6030  abrexex2g  6083  abrexex2  6087  recseq  6268  tfr0dm  6284  tfr1onlemaccex  6310  tfrcllemsucaccv  6316  tfrcllembxssdm  6318  tfrcllemaccex  6323  tfrcllemres  6324  freceq1  6354  frec0g  6359  freccllem  6364  frecfcllem  6366  frecsuclem  6368  frecsuc  6369  nnaordex  6489  qseq2  6544  elqsg  6545  elixpsn  6695  ixpsnf1o  6696  isfi  6721  enfi  6833  fimax2gtri  6861  elfi  6930  supeq3  6949  supmoti  6952  suplubti  6959  supisolem  6967  cnvinfex  6977  eqinfti  6979  infvalti  6981  infglbti  6984  enomnilem  7096  finomni  7098  exmidomni  7100  fodjum  7104  fodju0  7105  fodjuomnilemres  7106  fodjuomni  7107  ismkvnex  7113  fodjumkvlemres  7117  fodjumkv  7118  enmkvlem  7119  ltexnqq  7343  elinp  7409  prnmaxl  7423  prnminu  7424  prarloclem3  7432  ltdfpr  7441  genpdflem  7442  genipv  7444  genpassl  7459  genpassu  7460  ltexprlemm  7535  ltexprlemloc  7542  cauappcvgprlemm  7580  cauappcvgprlemopl  7581  cauappcvgprlemlol  7582  cauappcvgprlemopu  7583  cauappcvgprlemupu  7584  cauappcvgprlemdisj  7586  cauappcvgprlemloc  7587  cauappcvgprlemladdfu  7589  cauappcvgprlemladdfl  7590  cauappcvgprlemladdru  7591  cauappcvgprlemladdrl  7592  cauappcvgprlem1  7594  cauappcvgprlem2  7595  caucvgprlemm  7603  caucvgprlemopl  7604  caucvgprlemlol  7605  caucvgprlemopu  7606  caucvgprlemupu  7607  caucvgprlemdisj  7609  caucvgprlemloc  7610  caucvgprlemladdfu  7612  caucvgprlemladdrl  7613  caucvgprlem1  7614  caucvgprlem2  7615  caucvgprprlemell  7620  caucvgprprlemelu  7621  caucvgprprlemml  7629  caucvgprprlemmu  7630  caucvgprprlemexbt  7641  caucvgprprlem2  7645  suplocexprlemmu  7653  suplocexprlemru  7654  suplocexprlemdisj  7655  suplocexprlemloc  7656  suplocexprlemub  7658  recexgt0sr  7708  archsr  7717  map2psrprg  7740  suplocsrlemb  7741  axprecex  7815  nntopi  7829  axpre-suploclemres  7836  axpre-suploc  7837  cnegex  8070  apreap  8479  recexap  8544  sup3exmid  8846  creur  8848  creui  8849  cju  8850  supinfneg  9527  infsupneg  9528  exbtwnzlemshrink  10178  rebtwn2zlemshrink  10183  modqmuladd  10295  hashunlem  10711  shftfvalg  10754  shftfval  10757  rexfiuz  10925  recvguniq  10931  fimaxre2  11162  clim  11216  sumeq1  11290  summodc  11318  fsum3  11322  mertenslemub  11469  mertenslemi1  11470  mertenslem2  11471  mertensabs  11472  prodeq1f  11487  prodeq2w  11491  prodmodc  11513  fprodseq  11518  divides  11723  odd2np1lem  11803  opeo  11828  omeo  11829  divalglemeunn  11852  divalglemeuneg  11854  infssuzex  11876  nninfdcex  11880  zeqzmulgcd  11897  bezoutlemnewy  11923  bezoutlemmain  11925  bezoutlemex  11928  bezoutlemaz  11930  exprmfct  12064  nnnn0modprm0  12181  pceu  12221  pcprmpw2  12258  ennnfoneleminc  12338  ennnfonelemex  12341  ennnfonelemhom  12342  ennnfonelemnn0  12349  ennnfonelemr  12350  ctinfomlemom  12354  ctinfom  12355  nninfdclemcl  12375  nninfdclemp1  12377  nninfdc  12380  basis2  12644  eltg2  12651  tg2  12658  neival  12741  isnei  12742  isneip  12744  restbasg  12766  cnpval  12796  iscnp  12797  icnpimaex  12809  lmbr  12811  lmbr2  12812  cnptoprest2  12838  lmff  12847  txbas  12856  txcnp  12869  txrest  12874  blssps  13025  blss  13026  mopni  13080  metss  13092  metrest  13104  metcnp3  13109  divcnap  13153  cncfval  13157  elcncf2  13159  cncfmet  13177  dedekindeulemuub  13193  dedekindeulemloc  13195  dedekindeulemlu  13197  suplociccreex  13200  dedekindicclemuub  13202  dedekindicclemloc  13204  dedekindicclemlu  13206  limccl  13226  ellimc3apf  13227  limcdifap  13229  limcmpted  13230  bj-inf2vnlem1  13745  bj-inf2vnlem2  13746  bj-nn0sucALT  13753  sscoll2  13763  subctctexmid  13774  pw1nct  13776  isomninnlem  13802  trilpolemlt1  13813  trirec0  13816  ismkvnnlem  13824
  Copyright terms: Public domain W3C validator