![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > hbralrimi | Structured version Visualization version GIF version |
Description: Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). This theorem contains the common proof steps for ralrimi 3239 and ralrimiv 3139. Its main advantage over these two is its minimal references to axioms. The proof is extracted from NM's previous work. (Contributed by Wolf Lammen, 4-Dec-2019.) |
Ref | Expression |
---|---|
hbralrimi.1 | ⊢ (𝜑 → ∀𝑥𝜑) |
hbralrimi.2 | ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓)) |
Ref | Expression |
---|---|
hbralrimi | ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hbralrimi.1 | . . 3 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | hbralrimi.2 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓)) | |
3 | 1, 2 | alrimih 1827 | . 2 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) |
4 | df-ral 3062 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) | |
5 | 3, 4 | sylibr 233 | 1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1540 ∈ wcel 2107 ∀wral 3061 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 |
This theorem depends on definitions: df-bi 206 df-ral 3062 |
This theorem is referenced by: ralrimiv 3139 ralrimi 3239 bnj1145 33662 |
Copyright terms: Public domain | W3C validator |