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

Theorem ralprg 4624
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 2142, ax-12 2176. (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 4558 . . . 4 {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
21raleqi 3335 . . 3 (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ ∀𝑥 ∈ ({𝐴} ∪ {𝐵})𝜑)
3 ralunb 4119 . . 3 (∀𝑥 ∈ ({𝐴} ∪ {𝐵})𝜑 ↔ (∀𝑥 ∈ {𝐴}𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑))
42, 3bitri 278 . 2 (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (∀𝑥 ∈ {𝐴}𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑))
5 ralprg.1 . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
65ralsng 4603 . . 3 (𝐴𝑉 → (∀𝑥 ∈ {𝐴}𝜑𝜓))
7 ralprg.2 . . . 4 (𝑥 = 𝐵 → (𝜑𝜒))
87ralsng 4603 . . 3 (𝐵𝑊 → (∀𝑥 ∈ {𝐵}𝜑𝜒))
96, 8bi2anan9 639 . 2 ((𝐴𝑉𝐵𝑊) → ((∀𝑥 ∈ {𝐴}𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑) ↔ (𝜓𝜒)))
104, 9syl5bb 286 1 ((𝐴𝑉𝐵𝑊) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1543  wcel 2111  wral 3062  cun 3878  {csn 4555  {cpr 4557
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-ext 2709
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-sb 2072  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3067  df-v 3422  df-un 3885  df-sn 4556  df-pr 4558
This theorem is referenced by:  rexprg  4626  raltpg  4628  ralpr  4630  reuprg0  4632  iinxprg  5011  disjprgw  5062  disjprg  5063  fpropnf1  7097  f12dfv  7102  f13dfv  7103  suppr  9111  infpr  9143  pfx2  14536  sumpr  15336  gcdcllem2  16083  lcmfpr  16208  joinval2lem  17910  meetval2lem  17924  sgrp2rid2  18377  sgrp2nmndlem4  18379  sgrp2nmndlem5  18380  iccntr  23742  limcun  24816  cplgr3v  27547  3wlkdlem4  28269  frgr3v  28382  3vfriswmgr  28385  prsiga  31835  paireqne  44664
  Copyright terms: Public domain W3C validator