![]() |
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 3255 | . 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
5 | 2 | biimprd 247 | . . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜒 → 𝜓)) |
6 | 1, 5 | ralimdaa 3255 | . 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜒 → ∀𝑥 ∈ 𝐴 𝜓)) |
7 | 4, 6 | impbid 211 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 Ⅎwnf 1783 ∈ wcel 2104 ∀wral 3059 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-12 2169 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1780 df-nf 1784 df-ral 3060 |
This theorem is referenced by: ralbid 3268 2ralbida 3278 ac6num 10476 neiptopreu 22857 istrkg2ld 27978 funcnv5mpt 32160 nadd1suc 42444 naddsuc2 42445 xrralrecnnge 44398 climf2 44680 clim2f2 44684 limsupub 44718 climinfmpt 44729 limsupubuzmpt 44733 limsupre2mpt 44744 limsupre3mpt 44748 limsupreuzmpt 44753 xlimmnfmpt 44857 xlimpnfmpt 44858 smfsupmpt 45829 smfinfmpt 45833 |
Copyright terms: Public domain | W3C validator |