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

Theorem ralprg 4608
 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.) (Proof shortened by AV, 8-Apr-2023.)
Hypotheses
Ref Expression
ralprg.1 (𝑥 = 𝐴 → (𝜑𝜓))
ralprg.2 (𝑥 = 𝐵 → (𝜑𝜒))
Assertion
Ref Expression
ralprg ((𝐴𝑉𝐵𝑊) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓𝜒)))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜓,𝑥   𝜒,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝑉(𝑥)   𝑊(𝑥)

Proof of Theorem ralprg
StepHypRef Expression
1 nfv 1915 . 2 𝑥𝜓
2 nfv 1915 . 2 𝑥𝜒
3 ralprg.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
4 ralprg.2 . 2 (𝑥 = 𝐵 → (𝜑𝜒))
51, 2, 3, 4ralprgf 4606 1 ((𝐴𝑉𝐵𝑊) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓𝜒)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537   ∈ wcel 2114  ∀wral 3125  {cpr 4545 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-12 2177  ax-ext 2792 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-ral 3130  df-v 3475  df-sbc 3753  df-un 3918  df-sn 4544  df-pr 4546 This theorem is referenced by:  raltpg  4610  ralpr  4612  reuprg0  4614  iinxprg  4987  disjprgw  5037  disjprg  5038  fpropnf1  7002  f12dfv  7007  f13dfv  7008  suppr  8913  infpr  8945  pfx2  14289  sumpr  15083  gcdcllem2  15827  lcmfpr  15949  joinval2lem  17597  meetval2lem  17611  sgrp2rid2  18070  sgrp2nmndlem4  18072  sgrp2nmndlem5  18073  iccntr  23405  limcun  24477  cplgr3v  27204  3wlkdlem4  27926  frgr3v  28039  3vfriswmgr  28042  prsiga  31398  paireqne  43819
 Copyright terms: Public domain W3C validator