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

Theorem ralrimi 2506
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 1503 . 2 (𝜑 → ∀𝑥(𝑥𝐴𝜓))
4 df-ral 2422 . 2 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
53, 4sylibr 133 1 (𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1330  wnf 1437  wcel 1481  wral 2417
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 1424  ax-gen 1426  ax-4 1488
This theorem depends on definitions:  df-bi 116  df-nf 1438  df-ral 2422
This theorem is referenced by:  ralrimiv  2507  reximdai  2533  r19.12  2541  rexlimd  2549  rexlimd2  2550  r19.29af2  2575  r19.37  2586  ralidm  3466  iineq2d  3839  mpteq2da  4023  onintonm  4439  mpteqb  5517  fmptdf  5583  eusvobj2  5766  tfri3  6270  mapxpen  6748  fodjuomnilemdc  7022  cc3  7098  fimaxre2  11028  zsupcllemstep  11667  bezoutlemmain  11715  bezoutlemzz  11719  exmidunben  11968  mulcncf  12792  limccnp2lem  12846
  Copyright terms: Public domain W3C validator