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 2142, ax-12 2176. (Revised by Gino Giotto, 30-Sep-2024.) |
Ref | Expression |
---|---|
ralprg.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
ralprg.2 | ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) |
Ref | Expression |
---|---|
ralprg | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-pr 4558 | . . . 4 ⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵}) | |
2 | 1 | raleqi 3335 | . . 3 ⊢ (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ ∀𝑥 ∈ ({𝐴} ∪ {𝐵})𝜑) |
3 | ralunb 4119 | . . 3 ⊢ (∀𝑥 ∈ ({𝐴} ∪ {𝐵})𝜑 ↔ (∀𝑥 ∈ {𝐴}𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑)) | |
4 | 2, 3 | bitri 278 | . 2 ⊢ (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (∀𝑥 ∈ {𝐴}𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑)) |
5 | ralprg.1 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
6 | 5 | ralsng 4603 | . . 3 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) |
7 | ralprg.2 | . . . 4 ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) | |
8 | 7 | ralsng 4603 | . . 3 ⊢ (𝐵 ∈ 𝑊 → (∀𝑥 ∈ {𝐵}𝜑 ↔ 𝜒)) |
9 | 6, 8 | bi2anan9 639 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((∀𝑥 ∈ {𝐴}𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑) ↔ (𝜓 ∧ 𝜒))) |
10 | 4, 9 | syl5bb 286 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 = wceq 1543 ∈ wcel 2111 ∀wral 3062 ∪ cun 3878 {csn 4555 {cpr 4557 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2113 ax-9 2121 ax-ext 2709 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-tru 1546 df-ex 1788 df-sb 2072 df-clab 2716 df-cleq 2730 df-clel 2817 df-ral 3067 df-v 3422 df-un 3885 df-sn 4556 df-pr 4558 |
This theorem is referenced by: rexprg 4626 raltpg 4628 ralpr 4630 reuprg0 4632 iinxprg 5011 disjprgw 5062 disjprg 5063 fpropnf1 7097 f12dfv 7102 f13dfv 7103 suppr 9111 infpr 9143 pfx2 14536 sumpr 15336 gcdcllem2 16083 lcmfpr 16208 joinval2lem 17910 meetval2lem 17924 sgrp2rid2 18377 sgrp2nmndlem4 18379 sgrp2nmndlem5 18380 iccntr 23742 limcun 24816 cplgr3v 27547 3wlkdlem4 28269 frgr3v 28382 3vfriswmgr 28385 prsiga 31835 paireqne 44664 |
Copyright terms: Public domain | W3C validator |