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

Theorem ralprg 4658
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 2178, ax-12 2215. (Revised by GG, 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 4588 . . . 4 {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
21raleqi 3321 . . 3 (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ ∀𝑥 ∈ ({𝐴} ∪ {𝐵})𝜑)
3 ralunb 4152 . . 3 (∀𝑥 ∈ ({𝐴} ∪ {𝐵})𝜑 ↔ (∀𝑥 ∈ {𝐴}𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑))
42, 3bitri 278 . 2 (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (∀𝑥 ∈ {𝐴}𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑))
5 ralprg.1 . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
65ralsng 4637 . . 3 (𝐴𝑉 → (∀𝑥 ∈ {𝐴}𝜑𝜓))
7 ralprg.2 . . . 4 (𝑥 = 𝐵 → (𝜑𝜒))
87ralsng 4637 . . 3 (𝐵𝑊 → (∀𝑥 ∈ {𝐵}𝜑𝜒))
96, 8bi2anan9 649 . 2 ((𝐴𝑉𝐵𝑊) → ((∀𝑥 ∈ {𝐴}𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑) ↔ (𝜓𝜒)))
104, 9bitrid 286 1 ((𝐴𝑉𝐵𝑊) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 400   = wceq 1563  wcel 2145  wral 3079  cun 3905  {csn 4585  {cpr 4587
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737
This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-rex 3090  df-v 3459  df-un 3912  df-sn 4586  df-pr 4588
This theorem is referenced by:  rexprg  4659  raltpg  4660  ralpr  4662  reuprg0  4664  iinxprg  5050  disjprg  5100  fpropnf1  7255  f12dfv  7261  f13dfv  7262  suppr  9420  infpr  9453  pfx2  14972  sumpr  15787  gcdcllem2  16546  lcmfpr  16673  joinval2lem  18422  meetval2lem  18436  sgrp2rid2  18976  sgrp2nmndlem4  18978  sgrp2nmndlem5  18979  iccntr  24936  limcun  26011  cplgr3v  29690  3wlkdlem4  30418  frgr3v  30531  3vfriswmgr  30534  prsiga  34433  paireqne  48116
  Copyright terms: Public domain W3C validator