|   | 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 2140, ax-12 2176. (Revised by GG, 30-Sep-2024.) | 
| Ref | Expression | 
|---|---|
| ralprg.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | 
| ralprg.2 | ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) | 
| Ref | Expression | 
|---|---|
| ralprg | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒))) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | df-pr 4628 | . . . 4 ⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵}) | |
| 2 | 1 | raleqi 3323 | . . 3 ⊢ (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ ∀𝑥 ∈ ({𝐴} ∪ {𝐵})𝜑) | 
| 3 | ralunb 4196 | . . 3 ⊢ (∀𝑥 ∈ ({𝐴} ∪ {𝐵})𝜑 ↔ (∀𝑥 ∈ {𝐴}𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑)) | |
| 4 | 2, 3 | bitri 275 | . 2 ⊢ (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (∀𝑥 ∈ {𝐴}𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑)) | 
| 5 | ralprg.1 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
| 6 | 5 | ralsng 4674 | . . 3 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) | 
| 7 | ralprg.2 | . . . 4 ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) | |
| 8 | 7 | ralsng 4674 | . . 3 ⊢ (𝐵 ∈ 𝑊 → (∀𝑥 ∈ {𝐵}𝜑 ↔ 𝜒)) | 
| 9 | 6, 8 | bi2anan9 638 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((∀𝑥 ∈ {𝐴}𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑) ↔ (𝜓 ∧ 𝜒))) | 
| 10 | 4, 9 | bitrid 283 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒))) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1539 ∈ wcel 2107 ∀wral 3060 ∪ cun 3948 {csn 4625 {cpr 4627 | 
| 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-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1542 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-ral 3061 df-rex 3070 df-v 3481 df-un 3955 df-sn 4626 df-pr 4628 | 
| This theorem is referenced by: rexprg 4696 raltpg 4697 ralpr 4699 reuprg0 4701 iinxprg 5088 disjprg 5138 fpropnf1 7288 f12dfv 7294 f13dfv 7295 suppr 9512 infpr 9544 pfx2 14987 sumpr 15785 gcdcllem2 16538 lcmfpr 16665 joinval2lem 18426 meetval2lem 18440 sgrp2rid2 18940 sgrp2nmndlem4 18942 sgrp2nmndlem5 18943 iccntr 24844 limcun 25931 cplgr3v 29453 3wlkdlem4 30182 frgr3v 30295 3vfriswmgr 30298 prsiga 34133 paireqne 47503 | 
| Copyright terms: Public domain | W3C validator |