Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ralprg Structured version   Visualization version   GIF version

Theorem ralprg 4341
 Description: Convert a quantification over a pair to a conjunction. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
Hypotheses
Ref Expression
ralprg.1 (𝑥 = 𝐴 → (𝜑𝜓))
ralprg.2 (𝑥 = 𝐵 → (𝜑𝜒))
Assertion
Ref Expression
ralprg ((𝐴𝑉𝐵𝑊) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓𝜒)))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜓,𝑥   𝜒,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝑉(𝑥)   𝑊(𝑥)

Proof of Theorem ralprg
StepHypRef Expression
1 df-pr 4288 . . . 4 {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
21raleqi 3245 . . 3 (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ ∀𝑥 ∈ ({𝐴} ∪ {𝐵})𝜑)
3 ralunb 3902 . . 3 (∀𝑥 ∈ ({𝐴} ∪ {𝐵})𝜑 ↔ (∀𝑥 ∈ {𝐴}𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑))
42, 3bitri 264 . 2 (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (∀𝑥 ∈ {𝐴}𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑))
5 ralprg.1 . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
65ralsng 4325 . . 3 (𝐴𝑉 → (∀𝑥 ∈ {𝐴}𝜑𝜓))
7 ralprg.2 . . . 4 (𝑥 = 𝐵 → (𝜑𝜒))
87ralsng 4325 . . 3 (𝐵𝑊 → (∀𝑥 ∈ {𝐵}𝜑𝜒))
96, 8bi2anan9 953 . 2 ((𝐴𝑉𝐵𝑊) → ((∀𝑥 ∈ {𝐴}𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑) ↔ (𝜓𝜒)))
104, 9syl5bb 272 1 ((𝐴𝑉𝐵𝑊) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓𝜒)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1596   ∈ wcel 2103  ∀wral 3014   ∪ cun 3678  {csn 4285  {cpr 4287 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ral 3019  df-v 3306  df-sbc 3542  df-un 3685  df-sn 4286  df-pr 4288 This theorem is referenced by:  raltpg  4343  ralpr  4345  iinxprg  4709  disjprg  4756  fpropnf1  6639  f12dfv  6644  f13dfv  6645  suppr  8493  infpr  8525  sumpr  14597  gcdcllem2  15345  lcmfpr  15463  joinval2lem  17130  meetval2lem  17144  sgrp2rid2  17535  sgrp2nmndlem4  17537  sgrp2nmndlem5  17538  iccntr  22746  limcun  23779  cplgr3v  26462  3wlkdlem4  27235  frgr3v  27350  3vfriswmgr  27353  prsiga  30424  pfx2  41839
 Copyright terms: Public domain W3C validator