| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ralprg | Structured version Visualization version GIF version | ||
| Description: Convert a restricted universal quantification over a pair to a conjunction. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.) Avoid ax-10 2178, ax-12 2215. (Revised by GG, 30-Sep-2024.) |
| Ref | Expression |
|---|---|
| ralprg.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
| ralprg.2 | ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) |
| Ref | Expression |
|---|---|
| ralprg | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-pr 4588 | . . . 4 ⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵}) | |
| 2 | 1 | raleqi 3321 | . . 3 ⊢ (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ ∀𝑥 ∈ ({𝐴} ∪ {𝐵})𝜑) |
| 3 | ralunb 4152 | . . 3 ⊢ (∀𝑥 ∈ ({𝐴} ∪ {𝐵})𝜑 ↔ (∀𝑥 ∈ {𝐴}𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑)) | |
| 4 | 2, 3 | bitri 278 | . 2 ⊢ (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (∀𝑥 ∈ {𝐴}𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑)) |
| 5 | ralprg.1 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
| 6 | 5 | ralsng 4637 | . . 3 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) |
| 7 | ralprg.2 | . . . 4 ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) | |
| 8 | 7 | ralsng 4637 | . . 3 ⊢ (𝐵 ∈ 𝑊 → (∀𝑥 ∈ {𝐵}𝜑 ↔ 𝜒)) |
| 9 | 6, 8 | bi2anan9 649 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((∀𝑥 ∈ {𝐴}𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑) ↔ (𝜓 ∧ 𝜒))) |
| 10 | 4, 9 | bitrid 286 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒))) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 = wceq 1563 ∈ wcel 2145 ∀wral 3079 ∪ cun 3905 {csn 4585 {cpr 4587 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-ext 2737 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-tru 1566 df-ex 1803 df-sb 2094 df-clab 2744 df-cleq 2757 df-clel 2840 df-ral 3080 df-rex 3090 df-v 3459 df-un 3912 df-sn 4586 df-pr 4588 |
| This theorem is referenced by: rexprg 4659 raltpg 4660 ralpr 4662 reuprg0 4664 iinxprg 5051 disjprg 5101 fpropnf1 7255 f12dfv 7261 f13dfv 7262 suppr 9420 infpr 9453 pfx2 14974 sumpr 15789 gcdcllem2 16548 lcmfpr 16675 joinval2lem 18424 meetval2lem 18438 sgrp2rid2 18978 sgrp2nmndlem4 18980 sgrp2nmndlem5 18981 iccntr 24940 limcun 26015 cplgr3v 29694 3wlkdlem4 30422 frgr3v 30535 3vfriswmgr 30538 prsiga 34438 paireqne 48115 |
| Copyright terms: Public domain | W3C validator |