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

Theorem ralrimi 2548
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 1522 . 2 (𝜑 → ∀𝑥(𝑥𝐴𝜓))
4 df-ral 2460 . 2 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
53, 4sylibr 134 1 (𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1351  wnf 1460  wcel 2148  wral 2455
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-4 1510
This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460
This theorem is referenced by:  ralrimiv  2549  reximdai  2575  r19.12  2583  rexlimd  2591  rexlimd2  2592  r19.29af2  2617  r19.37  2629  ralidm  3524  iineq2d  3907  mpteq2da  4093  onintonm  4517  mpteqb  5607  fmptdf  5674  eusvobj2  5861  tfri3  6368  mapxpen  6848  fodjuomnilemdc  7142  cc3  7267  fimaxre2  11235  fprodcllemf  11621  fprodap0f  11644  fprodle  11648  zsupcllemstep  11946  bezoutlemmain  11999  bezoutlemzz  12003  exmidunben  12427  mulcncf  14094  limccnp2lem  14148
  Copyright terms: Public domain W3C validator