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  3523  iineq2d  3906  mpteq2da  4092  onintonm  4516  mpteqb  5606  fmptdf  5673  eusvobj2  5860  tfri3  6367  mapxpen  6847  fodjuomnilemdc  7141  cc3  7266  fimaxre2  11230  fprodcllemf  11616  fprodap0f  11639  fprodle  11643  zsupcllemstep  11940  bezoutlemmain  11993  bezoutlemzz  11997  exmidunben  12421  mulcncf  13984  limccnp2lem  14038
  Copyright terms: Public domain W3C validator