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

Theorem rexbidv 2415
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 1493 . 2 𝑥𝜑
2 ralbidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2rexbid 2413 1 (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐴 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104  wrex 2394
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 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-4 1472  ax-17 1491  ax-ial 1499
This theorem depends on definitions:  df-bi 116  df-nf 1422  df-rex 2399
This theorem is referenced by:  rexbii  2419  2rexbidv  2437  rexralbidv  2438  rexeqbi1dv  2612  rexeqbidv  2616  cbvrex2v  2640  rspc2ev  2778  rspc3ev  2780  ceqsrex2v  2791  sbcrext  2958  uniiunlem  3155  eliun  3787  dfiin2g  3816  dfiunv2  3819  nn0suc  4488  rexxpf  4656  elrnmpt  4758  elrnmptg  4761  elimag  4855  funcnvuni  5162  fun11iun  5356  fvelrnb  5437  fvelimab  5445  foco2  5623  elabrex  5627  abrexco  5628  f1oiso  5695  f1oiso2  5696  acexmidlemab  5736  acexmidlemcase  5737  grprinvlem  5933  abrexex2g  5986  abrexex2  5990  recseq  6171  tfr0dm  6187  tfr1onlemaccex  6213  tfrcllemsucaccv  6219  tfrcllembxssdm  6221  tfrcllemaccex  6226  tfrcllemres  6227  freceq1  6257  frec0g  6262  freccllem  6267  frecfcllem  6269  frecsuclem  6271  frecsuc  6272  nnaordex  6391  qseq2  6446  elqsg  6447  elixpsn  6597  ixpsnf1o  6598  isfi  6623  enfi  6735  fimax2gtri  6763  elfi  6827  supeq3  6845  supmoti  6848  suplubti  6855  supisolem  6863  cnvinfex  6873  eqinfti  6875  infvalti  6877  infglbti  6880  enomnilem  6978  finomni  6980  exmidomni  6982  fodjum  6986  fodju0  6987  fodjuomnilemres  6988  fodjuomni  6989  ismkvnex  6997  fodjumkvlemres  7001  fodjumkv  7002  ltexnqq  7184  elinp  7250  prnmaxl  7264  prnminu  7265  prarloclem3  7273  ltdfpr  7282  genpdflem  7283  genipv  7285  genpassl  7300  genpassu  7301  ltexprlemm  7376  ltexprlemloc  7383  cauappcvgprlemm  7421  cauappcvgprlemopl  7422  cauappcvgprlemlol  7423  cauappcvgprlemopu  7424  cauappcvgprlemupu  7425  cauappcvgprlemdisj  7427  cauappcvgprlemloc  7428  cauappcvgprlemladdfu  7430  cauappcvgprlemladdfl  7431  cauappcvgprlemladdru  7432  cauappcvgprlemladdrl  7433  cauappcvgprlem1  7435  cauappcvgprlem2  7436  caucvgprlemm  7444  caucvgprlemopl  7445  caucvgprlemlol  7446  caucvgprlemopu  7447  caucvgprlemupu  7448  caucvgprlemdisj  7450  caucvgprlemloc  7451  caucvgprlemladdfu  7453  caucvgprlemladdrl  7454  caucvgprlem1  7455  caucvgprlem2  7456  caucvgprprlemell  7461  caucvgprprlemelu  7462  caucvgprprlemml  7470  caucvgprprlemmu  7471  caucvgprprlemexbt  7482  caucvgprprlem2  7486  suplocexprlemmu  7494  suplocexprlemru  7495  suplocexprlemdisj  7496  suplocexprlemloc  7497  suplocexprlemub  7499  recexgt0sr  7549  archsr  7558  map2psrprg  7581  suplocsrlemb  7582  axprecex  7656  nntopi  7670  axpre-suploclemres  7677  axpre-suploc  7678  cnegex  7908  apreap  8316  recexap  8381  sup3exmid  8679  creur  8681  creui  8682  cju  8683  supinfneg  9346  infsupneg  9347  exbtwnzlemshrink  9981  rebtwn2zlemshrink  9986  modqmuladd  10094  hashunlem  10505  shftfvalg  10545  shftfval  10548  rexfiuz  10716  recvguniq  10722  fimaxre2  10953  clim  11005  sumeq1  11079  summodc  11107  fsum3  11111  mertenslemub  11258  mertenslemi1  11259  mertenslem2  11260  mertensabs  11261  divides  11407  odd2np1lem  11481  opeo  11506  omeo  11507  divalglemeunn  11530  divalglemeuneg  11532  infssuzex  11554  zeqzmulgcd  11571  bezoutlemnewy  11596  bezoutlemmain  11598  bezoutlemex  11601  bezoutlemaz  11603  exprmfct  11730  ennnfoneleminc  11835  ennnfonelemex  11838  ennnfonelemhom  11839  ennnfonelemnn0  11846  ennnfonelemr  11847  ctinfomlemom  11851  ctinfom  11852  basis2  12126  eltg2  12133  tg2  12140  neival  12223  isnei  12224  isneip  12226  restbasg  12248  cnpval  12278  iscnp  12279  icnpimaex  12291  lmbr  12293  lmbr2  12294  cnptoprest2  12320  lmff  12329  txbas  12338  txcnp  12351  txrest  12356  blssps  12507  blss  12508  mopni  12562  metss  12574  metrest  12586  metcnp3  12591  divcnap  12635  cncfval  12639  elcncf2  12641  cncfmet  12659  dedekindeulemuub  12675  dedekindeulemloc  12677  dedekindeulemlu  12679  suplociccreex  12682  dedekindicclemuub  12684  dedekindicclemloc  12686  dedekindicclemlu  12688  limccl  12708  ellimc3apf  12709  limcdifap  12711  limcmpted  12712  bj-inf2vnlem1  13064  bj-inf2vnlem2  13065  bj-nn0sucALT  13072  subctctexmid  13092  isomninnlem  13121  trilpolemlt1  13130
  Copyright terms: Public domain W3C validator