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

Theorem rexbidv 2375
Description: Formula-building rule for restricted existential quantifier (deduction rule). (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 1462 . 2 𝑥𝜑
2 ralbidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2rexbid 2373 1 (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐴 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103  wrex 2354
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468
This theorem depends on definitions:  df-bi 115  df-nf 1391  df-rex 2359
This theorem is referenced by:  rexbii  2379  2rexbidv  2397  rexralbidv  2398  rexeqbi1dv  2564  rexeqbidv  2568  cbvrex2v  2592  rspc2ev  2724  rspc3ev  2726  ceqsrex2v  2736  sbcrext  2901  uniiunlem  3092  eliun  3703  dfiin2g  3732  dfiunv2  3735  nn0suc  4374  rexxpf  4532  elrnmpt  4632  elrnmptg  4635  elimag  4723  funcnvuni  5020  fun11iun  5200  fvelrnb  5275  fvelimab  5283  foelrn  5371  foco2  5372  elabrex  5451  abrexco  5452  f1oiso  5518  f1oiso2  5519  acexmidlemab  5559  acexmidlemcase  5560  grprinvlem  5748  abrexex2g  5800  abrexex2  5804  recseq  5977  tfr0dm  5993  tfr1onlemaccex  6019  tfrcllemsucaccv  6025  tfrcllembxssdm  6027  tfrcllemaccex  6032  tfrcllemres  6033  freceq1  6063  frec0g  6068  freccllem  6073  frecfcllem  6075  frecsuclem  6077  frecsuc  6078  nnaordex  6189  qseq2  6244  elqsg  6245  isfi  6331  enfi  6431  supeq3  6499  supmoti  6502  suplubti  6509  supisolem  6517  cnvinfex  6527  eqinfti  6529  infvalti  6531  infglbti  6534  finomni  6581  exmidomni  6583  ltexnqq  6737  elinp  6803  prnmaxl  6817  prnminu  6818  prarloclem3  6826  ltdfpr  6835  genpdflem  6836  genipv  6838  genpassl  6853  genpassu  6854  ltexprlemm  6929  ltexprlemloc  6936  cauappcvgprlemm  6974  cauappcvgprlemopl  6975  cauappcvgprlemlol  6976  cauappcvgprlemopu  6977  cauappcvgprlemupu  6978  cauappcvgprlemdisj  6980  cauappcvgprlemloc  6981  cauappcvgprlemladdfu  6983  cauappcvgprlemladdfl  6984  cauappcvgprlemladdru  6985  cauappcvgprlemladdrl  6986  cauappcvgprlem1  6988  cauappcvgprlem2  6989  caucvgprlemm  6997  caucvgprlemopl  6998  caucvgprlemlol  6999  caucvgprlemopu  7000  caucvgprlemupu  7001  caucvgprlemdisj  7003  caucvgprlemloc  7004  caucvgprlemladdfu  7006  caucvgprlemladdrl  7007  caucvgprlem1  7008  caucvgprlem2  7009  caucvgprprlemell  7014  caucvgprprlemelu  7015  caucvgprprlemml  7023  caucvgprprlemmu  7024  caucvgprprlemexbt  7035  caucvgprprlem2  7039  recexgt0sr  7089  archsr  7097  axprecex  7185  nntopi  7199  cnegex  7430  apreap  7831  recexap  7887  creur  8180  creui  8181  cju  8182  supinfneg  8841  infsupneg  8842  exbtwnzlemshrink  9412  rebtwn2zlemshrink  9417  modqmuladd  9525  hashunlem  9905  shftfvalg  9932  shftfval  9935  rexfiuz  10101  recvguniq  10107  fimaxre2  10335  clim  10346  sumeq1  10418  divides  10430  odd2np1lem  10504  opeo  10529  omeo  10530  divalglemeunn  10553  divalglemeuneg  10555  infssuzex  10577  zeqzmulgcd  10594  bezoutlemnewy  10617  bezoutlemmain  10619  bezoutlemex  10622  bezoutlemaz  10624  exprmfct  10751  bj-inf2vnlem1  11057  bj-inf2vnlem2  11058  bj-nn0sucALT  11065
  Copyright terms: Public domain W3C validator