**Description:** Inference from Theorem 19.21 of Margaris p. 90. (Restricted
quantifier version with double quantification.) (Contributed by Jeff
Madsen, 19-Jun-2011)

Ref | Expression | ||
---|---|---|---|

Hypothesis | ralrimivva.1 | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → 𝜓 ) | |

Assertion | ralrimivva | ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜓 ) |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | ralrimivva.1 | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → 𝜓 ) | |

2 | 1 | ex | ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝜓 ) ) |

3 | 2 | ralrimivv | ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜓 ) |