![]() |
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 2138, ax-12 2172. (Revised by Gino Giotto, 30-Sep-2024.) |
Ref | Expression |
---|---|
ralprg.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
ralprg.2 | ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) |
Ref | Expression |
---|---|
ralprg | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-pr 4594 | . . . 4 ⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵}) | |
2 | 1 | raleqi 3314 | . . 3 ⊢ (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ ∀𝑥 ∈ ({𝐴} ∪ {𝐵})𝜑) |
3 | ralunb 4156 | . . 3 ⊢ (∀𝑥 ∈ ({𝐴} ∪ {𝐵})𝜑 ↔ (∀𝑥 ∈ {𝐴}𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑)) | |
4 | 2, 3 | bitri 275 | . 2 ⊢ (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (∀𝑥 ∈ {𝐴}𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑)) |
5 | ralprg.1 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
6 | 5 | ralsng 4639 | . . 3 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) |
7 | ralprg.2 | . . . 4 ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) | |
8 | 7 | ralsng 4639 | . . 3 ⊢ (𝐵 ∈ 𝑊 → (∀𝑥 ∈ {𝐵}𝜑 ↔ 𝜒)) |
9 | 6, 8 | bi2anan9 638 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((∀𝑥 ∈ {𝐴}𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑) ↔ (𝜓 ∧ 𝜒))) |
10 | 4, 9 | bitrid 283 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 = wceq 1542 ∈ wcel 2107 ∀wral 3065 ∪ cun 3913 {csn 4591 {cpr 4593 |
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-8 2109 ax-9 2117 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-ral 3066 df-v 3450 df-un 3920 df-sn 4592 df-pr 4594 |
This theorem is referenced by: rexprg 4662 raltpg 4664 ralpr 4666 reuprg0 4668 iinxprg 5054 disjprgw 5105 disjprg 5106 fpropnf1 7219 f12dfv 7224 f13dfv 7225 suppr 9414 infpr 9446 pfx2 14843 sumpr 15640 gcdcllem2 16387 lcmfpr 16510 joinval2lem 18276 meetval2lem 18290 sgrp2rid2 18743 sgrp2nmndlem4 18745 sgrp2nmndlem5 18746 iccntr 24200 limcun 25275 cplgr3v 28425 3wlkdlem4 29148 frgr3v 29261 3vfriswmgr 29264 prsiga 32770 paireqne 45777 |
Copyright terms: Public domain | W3C validator |