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

Theorem ralrimiv 2385
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Nov-1994.)
Hypothesis
Ref Expression
ralrimiv.1
Assertion
Ref Expression
ralrimiv
Distinct variable group:   ,
Allowed substitution hints:   ()   ()

Proof of Theorem ralrimiv
StepHypRef Expression
1 nfv 1418 . 2  F/
2 ralrimiv.1 . 2
31, 2ralrimi 2384 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:  ralrimiva  2386  ralrimivw  2387  ralrimivv  2394  r19.27av  2442  rr19.3v  2676  rabssdv  3014  rzal  3312  trin  3855  class2seteq  3907  ralxfrALT  4165  ssorduni  4179  ordsucim  4192  issref  4650  funimaexglem  4925  poxp  5794  rdgss  5910  dom2lem  6188  uzind  8105  zindd  8112  lbzbi  8307  icoshftf1o  8609  bj-nntrans2  9386  bj-inf2vnlem1  9400
  Copyright terms: Public domain W3C validator