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

Theorem ralrimi 2480
Description: Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 10-Oct-1999.)
Hypotheses
Ref Expression
ralrimi.1 𝑥𝜑
ralrimi.2 (𝜑 → (𝑥𝐴𝜓))
Assertion
Ref Expression
ralrimi (𝜑 → ∀𝑥𝐴 𝜓)

Proof of Theorem ralrimi
StepHypRef Expression
1 ralrimi.1 . . 3 𝑥𝜑
2 ralrimi.2 . . 3 (𝜑 → (𝑥𝐴𝜓))
31, 2alrimi 1487 . 2 (𝜑 → ∀𝑥(𝑥𝐴𝜓))
4 df-ral 2398 . 2 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
53, 4sylibr 133 1 (𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1314  wnf 1421  wcel 1465  wral 2393
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 1408  ax-gen 1410  ax-4 1472
This theorem depends on definitions:  df-bi 116  df-nf 1422  df-ral 2398
This theorem is referenced by:  ralrimiv  2481  reximdai  2507  r19.12  2515  rexlimd  2523  rexlimd2  2524  r19.29af2  2549  r19.37  2560  ralidm  3433  iineq2d  3803  mpteq2da  3987  onintonm  4403  mpteqb  5479  fmptdf  5545  eusvobj2  5728  tfri3  6232  mapxpen  6710  fodjuomnilemdc  6984  fimaxre2  10966  zsupcllemstep  11565  bezoutlemmain  11613  bezoutlemzz  11617  exmidunben  11866  mulcncf  12687  limccnp2lem  12741
  Copyright terms: Public domain W3C validator