![]() |
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 3258 | . 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
5 | 2 | biimprd 247 | . . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜒 → 𝜓)) |
6 | 1, 5 | ralimdaa 3258 | . 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 3062 |
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 3063 |
This theorem is referenced by: ralbid 3271 2ralbida 3281 ac6num 10474 neiptopreu 22637 istrkg2ld 27711 funcnv5mpt 31893 nadd1suc 42142 naddsuc2 42143 xrralrecnnge 44100 climf2 44382 clim2f2 44386 limsupub 44420 climinfmpt 44431 limsupubuzmpt 44435 limsupre2mpt 44446 limsupre3mpt 44450 limsupreuzmpt 44455 xlimmnfmpt 44559 xlimpnfmpt 44560 smfsupmpt 45531 smfinfmpt 45535 |
Copyright terms: Public domain | W3C validator |