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

Theorem ralpr 4185
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 4181 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓𝜒)))
61, 2, 5mp2an 704 1 (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383   = wceq 1475  wcel 1977  wral 2896  Vcvv 3173  {cpr 4127
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-v 3175  df-sbc 3403  df-un 3545  df-sn 4126  df-pr 4128
This theorem is referenced by:  fzprval  12271  fvinim0ffz  12449  wwlktovf1  13548  xpsfrnel  16046  xpsle  16064  isdrs2  16762  pmtrsn  17762  iblcnlem1  23360  wlkntrllem2  26090  wlkntrllem3  26091  2wlklem  26094  numclwwlkovf2ex  26613  subfacp1lem3  30418  fprb  30916  poimirlem1  32580  lfuhgr1v0e  40480  nbgr2vtx1edg  40572  nbuhgr2vtx1edgb  40574  umgr2v2evd2  40743  2Wlklem  40875  usgr2wlkneq  40962  usgr2trlncl  40966  21wlkdlem5  41136  21wlkdlem10  41142  3pthdlem1  41331  upgr4cycl4dv4e  41352  av-numclwwlkovf2ex  41517  ldepsnlinc  42091
  Copyright terms: Public domain W3C validator