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.) (Proof shortened by AV, 8-Apr-2023.) |
Ref | Expression |
---|---|
ralprg.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
ralprg.2 | ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) |
Ref | Expression |
---|---|
ralprg | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1911 | . 2 ⊢ Ⅎ𝑥𝜓 | |
2 | nfv 1911 | . 2 ⊢ Ⅎ𝑥𝜒 | |
3 | ralprg.1 | . 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
4 | ralprg.2 | . 2 ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) | |
5 | 1, 2, 3, 4 | ralprgf 4623 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 = wceq 1533 ∈ wcel 2110 ∀wral 3138 {cpr 4562 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-v 3496 df-sbc 3772 df-un 3940 df-sn 4561 df-pr 4563 |
This theorem is referenced by: raltpg 4627 ralpr 4629 reuprg0 4631 iinxprg 5003 disjprgw 5053 disjprg 5054 fpropnf1 7019 f12dfv 7024 f13dfv 7025 suppr 8929 infpr 8961 pfx2 14303 sumpr 15097 gcdcllem2 15843 lcmfpr 15965 joinval2lem 17612 meetval2lem 17626 sgrp2rid2 18085 sgrp2nmndlem4 18087 sgrp2nmndlem5 18088 iccntr 23423 limcun 24487 cplgr3v 27211 3wlkdlem4 27935 frgr3v 28048 3vfriswmgr 28051 prsiga 31385 paireqne 43667 |
Copyright terms: Public domain | W3C validator |