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

Theorem rexbidv 2377
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 1464 . 2 𝑥𝜑
2 ralbidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2rexbid 2375 1 (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐴 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103  wrex 2356
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 1379  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-4 1443  ax-17 1462  ax-ial 1470
This theorem depends on definitions:  df-bi 115  df-nf 1393  df-rex 2361
This theorem is referenced by:  rexbii  2381  2rexbidv  2399  rexralbidv  2400  rexeqbi1dv  2567  rexeqbidv  2571  cbvrex2v  2595  rspc2ev  2728  rspc3ev  2730  ceqsrex2v  2740  sbcrext  2905  uniiunlem  3098  eliun  3719  dfiin2g  3748  dfiunv2  3751  nn0suc  4394  rexxpf  4553  elrnmpt  4654  elrnmptg  4657  elimag  4747  funcnvuni  5050  fun11iun  5239  fvelrnb  5317  fvelimab  5325  foelrnOLD  5495  foco2  5496  elabrex  5500  abrexco  5501  f1oiso  5568  f1oiso2  5569  acexmidlemab  5609  acexmidlemcase  5610  grprinvlem  5798  abrexex2g  5850  abrexex2  5854  recseq  6027  tfr0dm  6043  tfr1onlemaccex  6069  tfrcllemsucaccv  6075  tfrcllembxssdm  6077  tfrcllemaccex  6082  tfrcllemres  6083  freceq1  6113  frec0g  6118  freccllem  6123  frecfcllem  6125  frecsuclem  6127  frecsuc  6128  nnaordex  6240  qseq2  6295  elqsg  6296  isfi  6432  enfi  6543  fimax2gtri  6571  supeq3  6632  supmoti  6635  suplubti  6642  supisolem  6650  cnvinfex  6660  eqinfti  6662  infvalti  6664  infglbti  6667  enomnilem  6741  finomni  6743  exmidomni  6745  fodjuomnilemm  6748  fodjuomnilem0  6749  fodjuomnilemres  6750  fodjuomni  6751  ltexnqq  6914  elinp  6980  prnmaxl  6994  prnminu  6995  prarloclem3  7003  ltdfpr  7012  genpdflem  7013  genipv  7015  genpassl  7030  genpassu  7031  ltexprlemm  7106  ltexprlemloc  7113  cauappcvgprlemm  7151  cauappcvgprlemopl  7152  cauappcvgprlemlol  7153  cauappcvgprlemopu  7154  cauappcvgprlemupu  7155  cauappcvgprlemdisj  7157  cauappcvgprlemloc  7158  cauappcvgprlemladdfu  7160  cauappcvgprlemladdfl  7161  cauappcvgprlemladdru  7162  cauappcvgprlemladdrl  7163  cauappcvgprlem1  7165  cauappcvgprlem2  7166  caucvgprlemm  7174  caucvgprlemopl  7175  caucvgprlemlol  7176  caucvgprlemopu  7177  caucvgprlemupu  7178  caucvgprlemdisj  7180  caucvgprlemloc  7181  caucvgprlemladdfu  7183  caucvgprlemladdrl  7184  caucvgprlem1  7185  caucvgprlem2  7186  caucvgprprlemell  7191  caucvgprprlemelu  7192  caucvgprprlemml  7200  caucvgprprlemmu  7201  caucvgprprlemexbt  7212  caucvgprprlem2  7216  recexgt0sr  7266  archsr  7274  axprecex  7362  nntopi  7376  cnegex  7607  apreap  8008  recexap  8064  creur  8357  creui  8358  cju  8359  supinfneg  9018  infsupneg  9019  exbtwnzlemshrink  9591  rebtwn2zlemshrink  9596  modqmuladd  9704  hashunlem  10112  shftfvalg  10152  shftfval  10155  rexfiuz  10321  recvguniq  10327  fimaxre2  10556  clim  10567  sumeq1  10639  isummo  10667  fisum  10670  divides  10704  odd2np1lem  10778  opeo  10803  omeo  10804  divalglemeunn  10827  divalglemeuneg  10829  infssuzex  10851  zeqzmulgcd  10868  bezoutlemnewy  10891  bezoutlemmain  10893  bezoutlemex  10896  bezoutlemaz  10898  exprmfct  11025  bj-inf2vnlem1  11334  bj-inf2vnlem2  11335  bj-nn0sucALT  11342
  Copyright terms: Public domain W3C validator