Theorem ralrimi 2535

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

Step	Hyp	Ref	Expression
1		ralrimi.1	. . 3 ⊢ Ⅎ𝑥𝜑
2		ralrimi.2	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))
3	1, 2	alrimi 1509	. 2 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))
4		df-ral 2447	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))
5	3, 4	sylibr 133	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4  ∀wal 1340  Ⅎwnf 1447   ∈ wcel 2135  ∀wral 2442

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 1434  ax-gen 1436  ax-4 1497

This theorem depends on definitions:  df-bi 116  df-nf 1448  df-ral 2447

This theorem is referenced by:  ralrimiv  2536  reximdai  2562  r19.12  2570  rexlimd  2578  rexlimd2  2579  r19.29af2  2604  r19.37  2616  ralidm  3504  iineq2d  3880  mpteq2da  4065  onintonm  4488  mpteqb  5570  fmptdf  5636  eusvobj2  5822  tfri3  6326  mapxpen  6805  fodjuomnilemdc  7099  cc3  7200  fimaxre2  11154  fprodcllemf  11540  fprodap0f  11563  fprodle  11567  zsupcllemstep  11863  bezoutlemmain  11916  bezoutlemzz  11920  exmidunben  12296  mulcncf  13132  limccnp2lem  13186