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

Theorem ralpr 4426
Description: Convert a quantification over a pair to a conjunction. (Contributed by NM, 3-Jun-2007.) (Revised by Mario Carneiro, 23-Apr-2015.)
Hypotheses
Ref Expression
ralpr.1 𝐴 ∈ V
ralpr.2 𝐵 ∈ V
ralpr.3 (𝑥 = 𝐴 → (𝜑𝜓))
ralpr.4 (𝑥 = 𝐵 → (𝜑𝜒))
Assertion
Ref Expression
ralpr (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓𝜒))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜓,𝑥   𝜒,𝑥
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem ralpr
StepHypRef Expression
1 ralpr.1 . 2 𝐴 ∈ V
2 ralpr.2 . 2 𝐵 ∈ V
3 ralpr.3 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
4 ralpr.4 . . 3 (𝑥 = 𝐵 → (𝜑𝜒))
53, 4ralprg 4422 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓𝜒)))
61, 2, 5mp2an 684 1 (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 385   = wceq 1653  wcel 2157  wral 3087  Vcvv 3383  {cpr 4368
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2775
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2784  df-cleq 2790  df-clel 2793  df-nfc 2928  df-ral 3092  df-v 3385  df-sbc 3632  df-un 3772  df-sn 4367  df-pr 4369
This theorem is referenced by:  fzprval  12651  fvinim0ffz  12838  wwlktovf1  14040  xpsfrnel  16535  xpsle  16553  isdrs2  17251  pmtrsn  18249  iblcnlem1  23892  lfuhgr1v0e  26480  nbgr2vtx1edg  26580  nbuhgr2vtx1edgb  26582  umgr2v2evd2  26769  2wlklem  26908  2wlkdlem5  27210  2wlkdlem10  27216  clwwlknonex2lem2  27440  3pthdlem1  27500  upgr4cycl4dv4e  27521  subfacp1lem3  31673  fprb  32175  poimirlem1  33891  ldepsnlinc  43084
  Copyright terms: Public domain W3C validator