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

Theorem rexbidv 2413
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 1491 . 2 𝑥𝜑
2 ralbidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2rexbid 2411 1 (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐴 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104  wrex 2392
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 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-17 1489  ax-ial 1497
This theorem depends on definitions:  df-bi 116  df-nf 1420  df-rex 2397
This theorem is referenced by:  rexbii  2417  2rexbidv  2435  rexralbidv  2436  rexeqbi1dv  2610  rexeqbidv  2614  cbvrex2v  2638  rspc2ev  2776  rspc3ev  2778  ceqsrex2v  2789  sbcrext  2956  uniiunlem  3153  eliun  3785  dfiin2g  3814  dfiunv2  3817  nn0suc  4486  rexxpf  4654  elrnmpt  4756  elrnmptg  4759  elimag  4853  funcnvuni  5160  fun11iun  5354  fvelrnb  5435  fvelimab  5443  foco2  5621  elabrex  5625  abrexco  5626  f1oiso  5693  f1oiso2  5694  acexmidlemab  5734  acexmidlemcase  5735  grprinvlem  5931  abrexex2g  5984  abrexex2  5988  recseq  6169  tfr0dm  6185  tfr1onlemaccex  6211  tfrcllemsucaccv  6217  tfrcllembxssdm  6219  tfrcllemaccex  6224  tfrcllemres  6225  freceq1  6255  frec0g  6260  freccllem  6265  frecfcllem  6267  frecsuclem  6269  frecsuc  6270  nnaordex  6389  qseq2  6444  elqsg  6445  elixpsn  6595  ixpsnf1o  6596  isfi  6621  enfi  6733  fimax2gtri  6761  elfi  6825  supeq3  6843  supmoti  6846  suplubti  6853  supisolem  6861  cnvinfex  6871  eqinfti  6873  infvalti  6875  infglbti  6878  enomnilem  6976  finomni  6978  exmidomni  6980  fodjum  6984  fodju0  6985  fodjuomnilemres  6986  fodjuomni  6987  ismkvnex  6995  fodjumkvlemres  6999  fodjumkv  7000  ltexnqq  7180  elinp  7246  prnmaxl  7260  prnminu  7261  prarloclem3  7269  ltdfpr  7278  genpdflem  7279  genipv  7281  genpassl  7296  genpassu  7297  ltexprlemm  7372  ltexprlemloc  7379  cauappcvgprlemm  7417  cauappcvgprlemopl  7418  cauappcvgprlemlol  7419  cauappcvgprlemopu  7420  cauappcvgprlemupu  7421  cauappcvgprlemdisj  7423  cauappcvgprlemloc  7424  cauappcvgprlemladdfu  7426  cauappcvgprlemladdfl  7427  cauappcvgprlemladdru  7428  cauappcvgprlemladdrl  7429  cauappcvgprlem1  7431  cauappcvgprlem2  7432  caucvgprlemm  7440  caucvgprlemopl  7441  caucvgprlemlol  7442  caucvgprlemopu  7443  caucvgprlemupu  7444  caucvgprlemdisj  7446  caucvgprlemloc  7447  caucvgprlemladdfu  7449  caucvgprlemladdrl  7450  caucvgprlem1  7451  caucvgprlem2  7452  caucvgprprlemell  7457  caucvgprprlemelu  7458  caucvgprprlemml  7466  caucvgprprlemmu  7467  caucvgprprlemexbt  7478  caucvgprprlem2  7482  suplocexprlemmu  7490  suplocexprlemru  7491  suplocexprlemdisj  7492  suplocexprlemloc  7493  suplocexprlemub  7495  recexgt0sr  7545  archsr  7554  map2psrprg  7577  suplocsrlemb  7578  axprecex  7652  nntopi  7666  axpre-suploclemres  7673  axpre-suploc  7674  cnegex  7904  apreap  8312  recexap  8374  sup3exmid  8672  creur  8674  creui  8675  cju  8676  supinfneg  9339  infsupneg  9340  exbtwnzlemshrink  9966  rebtwn2zlemshrink  9971  modqmuladd  10079  hashunlem  10490  shftfvalg  10530  shftfval  10533  rexfiuz  10701  recvguniq  10707  fimaxre2  10938  clim  10990  sumeq1  11064  summodc  11092  fsum3  11096  mertenslemub  11243  mertenslemi1  11244  mertenslem2  11245  mertensabs  11246  divides  11391  odd2np1lem  11465  opeo  11490  omeo  11491  divalglemeunn  11514  divalglemeuneg  11516  infssuzex  11538  zeqzmulgcd  11555  bezoutlemnewy  11580  bezoutlemmain  11582  bezoutlemex  11585  bezoutlemaz  11587  exprmfct  11714  ennnfoneleminc  11819  ennnfonelemex  11822  ennnfonelemhom  11823  ennnfonelemnn0  11830  ennnfonelemr  11831  ctinfomlemom  11835  ctinfom  11836  basis2  12110  eltg2  12117  tg2  12124  neival  12207  isnei  12208  isneip  12210  restbasg  12232  cnpval  12262  iscnp  12263  icnpimaex  12275  lmbr  12277  lmbr2  12278  cnptoprest2  12304  lmff  12313  txbas  12322  txcnp  12335  txrest  12340  blssps  12491  blss  12492  mopni  12546  metss  12558  metrest  12570  metcnp3  12575  divcnap  12619  cncfval  12623  elcncf2  12625  cncfmet  12643  dedekindeulemuub  12659  dedekindeulemloc  12661  dedekindeulemlu  12663  limccl  12671  ellimc3apf  12672  limcdifap  12674  limcmpted  12675  bj-inf2vnlem1  12970  bj-inf2vnlem2  12971  bj-nn0sucALT  12978  subctctexmid  12998  isomninnlem  13027  trilpolemlt1  13036
  Copyright terms: Public domain W3C validator