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

Theorem rexbidva 2323
 Description: Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 9-Mar-1997.)
Hypothesis
Ref Expression
ralbidva.1
Assertion
Ref Expression
rexbidva
Distinct variable group:   ,
Allowed substitution hints:   ()   ()   ()

Proof of Theorem rexbidva
StepHypRef Expression
1 nfv 1421 . 2
2 ralbidva.1 . 2
31, 2rexbida 2321 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 97   wb 98   wcel 1393  wrex 2307 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427 This theorem depends on definitions:  df-bi 110  df-nf 1350  df-rex 2312 This theorem is referenced by:  2rexbiia  2340  2rexbidva  2347  rexeqbidva  2520  dfimafn  5222  funimass4  5224  fconstfvm  5379  fliftel  5433  fliftf  5439  f1oiso  5465  releldm2  5811  qsinxp  6182  qliftel  6186  genpassl  6622  genpassu  6623  addcomprg  6676  mulcomprg  6678  1idprl  6688  1idpru  6689  archrecnq  6761  archrecpr  6762  caucvgprprlemexbt  6804  caucvgprprlemexb  6805  archsr  6866  cnegexlem3  7188  cnegex2  7190  recexre  7569  rerecclap  7706  creur  7911  creui  7912  nndiv  7954  arch  8178  nnrecl  8179  expnlbnd  9373  clim2  9804  clim2c  9805  clim0c  9807  climabs0  9828  climrecvg1n  9867
 Copyright terms: Public domain W3C validator