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

Theorem ralprg 4371
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 4319 . . . 4 {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
21raleqi 3291 . . 3 (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ ∀𝑥 ∈ ({𝐴} ∪ {𝐵})𝜑)
3 ralunb 3945 . . 3 (∀𝑥 ∈ ({𝐴} ∪ {𝐵})𝜑 ↔ (∀𝑥 ∈ {𝐴}𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑))
42, 3bitri 264 . 2 (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (∀𝑥 ∈ {𝐴}𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑))
5 ralprg.1 . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
65ralsng 4356 . . 3 (𝐴𝑉 → (∀𝑥 ∈ {𝐴}𝜑𝜓))
7 ralprg.2 . . . 4 (𝑥 = 𝐵 → (𝜑𝜒))
87ralsng 4356 . . 3 (𝐵𝑊 → (∀𝑥 ∈ {𝐵}𝜑𝜒))
96, 8bi2anan9 620 . 2 ((𝐴𝑉𝐵𝑊) → ((∀𝑥 ∈ {𝐴}𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑) ↔ (𝜓𝜒)))
104, 9syl5bb 272 1 ((𝐴𝑉𝐵𝑊) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382   = wceq 1631  wcel 2145  wral 3061  cun 3721  {csn 4316  {cpr 4318
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-v 3353  df-sbc 3588  df-un 3728  df-sn 4317  df-pr 4319
This theorem is referenced by:  raltpg  4373  ralpr  4375  iinxprg  4735  disjprg  4782  fpropnf1  6667  f12dfv  6672  f13dfv  6673  suppr  8533  infpr  8565  sumpr  14685  gcdcllem2  15430  lcmfpr  15548  joinval2lem  17216  meetval2lem  17230  sgrp2rid2  17621  sgrp2nmndlem4  17623  sgrp2nmndlem5  17624  iccntr  22844  limcun  23879  cplgr3v  26566  3wlkdlem4  27342  frgr3v  27457  3vfriswmgr  27460  prsiga  30534  pfx2  41940
  Copyright terms: Public domain W3C validator