![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ralbida | Structured version Visualization version GIF version |
Description: Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 6-Oct-2003.) (Proof shortened by Wolf Lammen, 31-Oct-2024.) |
Ref | Expression |
---|---|
ralbida.1 | ⊢ Ⅎ𝑥𝜑 |
ralbida.2 | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
ralbida | ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralbida.1 | . . 3 ⊢ Ⅎ𝑥𝜑 | |
2 | ralbida.2 | . . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) | |
3 | 2 | biimpd 228 | . . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) |
4 | 1, 3 | ralimdaa 3242 | . 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
5 | 2 | biimprd 248 | . . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜒 → 𝜓)) |
6 | 1, 5 | ralimdaa 3242 | . 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜒 → ∀𝑥 ∈ 𝐴 𝜓)) |
7 | 4, 6 | impbid 211 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 Ⅎwnf 1786 ∈ wcel 2107 ∀wral 3063 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-12 2172 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-nf 1787 df-ral 3064 |
This theorem is referenced by: ralbid 3255 2ralbida 3265 ac6num 10349 neiptopreu 22412 istrkg2ld 27207 funcnv5mpt 31388 xrralrecnnge 43420 climf2 43698 clim2f2 43702 limsupub 43736 climinfmpt 43747 limsupubuzmpt 43751 limsupre2mpt 43762 limsupre3mpt 43766 limsupreuzmpt 43771 xlimmnfmpt 43875 xlimpnfmpt 43876 smfsupmpt 44847 smfinfmpt 44851 |
Copyright terms: Public domain | W3C validator |