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

Theorem ralrimivw 2387
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.)
Hypothesis
Ref Expression
ralrimivw.1
Assertion
Ref Expression
ralrimivw
Distinct variable group:   ,
Allowed substitution hints:   ()   ()

Proof of Theorem ralrimivw
StepHypRef Expression
1 ralrimivw.1 . . 3
21a1d 22 . 2
32ralrimiv 2385 1
Colors of variables: wff set class
Syntax hints:   wi 4   wcel 1390  wral 2300
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 1333  ax-gen 1335  ax-4 1397  ax-17 1416
This theorem depends on definitions:  df-bi 110  df-nf 1347  df-ral 2305
This theorem is referenced by:  exse  4058  sosng  4356  dmxpm  4498  exse2  4642  funco  4883  acexmidlemph  5448  mpt2eq12  5507  xpexgALT  5702  mpt2exg  5776  rdgtfr  5901  rdgruledefgg  5902  rdgivallem  5908  frecabex  5923  frectfr  5924  omfnex  5968  oeiv  5975  oeicl  5981  uniqs  6100  genpdisj  6506  ltexprlemloc  6581  recexprlemloc  6603  cauappcvgprlemrnd  6622  cauappcvgprlemdisj  6623  caucvgprlemrnd  6644  caucvgprlemdisj  6645
  Copyright terms: Public domain W3C validator