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

Theorem ralprg 4699
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 2138, ax-12 2172. (Revised by Gino Giotto, 30-Sep-2024.)
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 4632 . . . 4 {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
21raleqi 3324 . . 3 (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ ∀𝑥 ∈ ({𝐴} ∪ {𝐵})𝜑)
3 ralunb 4192 . . 3 (∀𝑥 ∈ ({𝐴} ∪ {𝐵})𝜑 ↔ (∀𝑥 ∈ {𝐴}𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑))
42, 3bitri 275 . 2 (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (∀𝑥 ∈ {𝐴}𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑))
5 ralprg.1 . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
65ralsng 4678 . . 3 (𝐴𝑉 → (∀𝑥 ∈ {𝐴}𝜑𝜓))
7 ralprg.2 . . . 4 (𝑥 = 𝐵 → (𝜑𝜒))
87ralsng 4678 . . 3 (𝐵𝑊 → (∀𝑥 ∈ {𝐵}𝜑𝜒))
96, 8bi2anan9 638 . 2 ((𝐴𝑉𝐵𝑊) → ((∀𝑥 ∈ {𝐴}𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑) ↔ (𝜓𝜒)))
104, 9bitrid 283 1 ((𝐴𝑉𝐵𝑊) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  wcel 2107  wral 3062  cun 3947  {csn 4629  {cpr 4631
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-v 3477  df-un 3954  df-sn 4630  df-pr 4632
This theorem is referenced by:  rexprg  4701  raltpg  4703  ralpr  4705  reuprg0  4707  iinxprg  5093  disjprgw  5144  disjprg  5145  fpropnf1  7266  f12dfv  7271  f13dfv  7272  suppr  9466  infpr  9498  pfx2  14898  sumpr  15694  gcdcllem2  16441  lcmfpr  16564  joinval2lem  18333  meetval2lem  18347  sgrp2rid2  18807  sgrp2nmndlem4  18809  sgrp2nmndlem5  18810  iccntr  24337  limcun  25412  cplgr3v  28692  3wlkdlem4  29415  frgr3v  29528  3vfriswmgr  29531  prsiga  33129  paireqne  46179
  Copyright terms: Public domain W3C validator