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 2957 and ralrimiv 2965. 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 1751 | . 2 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) |
4 | df-ral 2917 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) | |
5 | 3, 4 | sylibr 224 | 1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1481 ∈ wcel 1990 ∀wral 2912 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 |
This theorem depends on definitions: df-bi 197 df-ral 2917 |
This theorem is referenced by: ralrimi 2957 ralrimiv 2965 bnj1145 31061 |
Copyright terms: Public domain | W3C validator |