|   | 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 229 | . . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) | 
| 4 | 1, 3 | ralimdaa 3259 | . 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) | 
| 5 | 2 | biimprd 248 | . . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜒 → 𝜓)) | 
| 6 | 1, 5 | ralimdaa 3259 | . 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜒 → ∀𝑥 ∈ 𝐴 𝜓)) | 
| 7 | 4, 6 | impbid 212 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 Ⅎwnf 1782 ∈ wcel 2107 ∀wral 3060 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-12 2176 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 df-nf 1783 df-ral 3061 | 
| This theorem is referenced by: ralbid 3272 2ralbida 3282 naddsuc2 8740 ac6num 10520 neiptopreu 23142 istrkg2ld 28469 funcnv5mpt 32679 nadd1suc 43410 xrralrecnnge 45406 climf2 45686 clim2f2 45690 limsupub 45724 climinfmpt 45735 limsupubuzmpt 45739 limsupre2mpt 45750 limsupre3mpt 45754 limsupreuzmpt 45759 xlimmnfmpt 45863 xlimpnfmpt 45864 smfsupmpt 46835 smfinfmpt 46839 | 
| Copyright terms: Public domain | W3C validator |