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 3239 | . 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
5 | 2 | biimprd 247 | . . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜒 → 𝜓)) |
6 | 1, 5 | ralimdaa 3239 | . 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜒 → ∀𝑥 ∈ 𝐴 𝜓)) |
7 | 4, 6 | impbid 211 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 Ⅎwnf 1784 ∈ wcel 2105 ∀wral 3061 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-12 2170 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1781 df-nf 1785 df-ral 3062 |
This theorem is referenced by: ralbid 3252 2ralbida 3262 ac6num 10336 neiptopreu 22390 istrkg2ld 27110 funcnv5mpt 31292 xrralrecnnge 43265 climf2 43543 clim2f2 43547 limsupub 43581 climinfmpt 43592 limsupubuzmpt 43596 limsupre2mpt 43607 limsupre3mpt 43611 limsupreuzmpt 43616 xlimmnfmpt 43720 xlimpnfmpt 43721 smfsupmpt 44690 smfinfmpt 44694 |
Copyright terms: Public domain | W3C validator |