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

Theorem ralpr 4547
Description: Convert a restricted universal 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 4543 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓𝜒)))
61, 2, 5mp2an 688 1 (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1522  wcel 2081  wral 3105  Vcvv 3437  {cpr 4478
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ral 3110  df-v 3439  df-sbc 3710  df-un 3868  df-sn 4477  df-pr 4479
This theorem is referenced by:  fprb  6828  fzprval  12823  fvinim0ffz  13011  wwlktovf1  14160  xpsfrnel  16669  xpsle  16686  isdrs2  17383  pmtrsn  18383  iblcnlem1  24076  lfuhgr1v0e  26724  nbgr2vtx1edg  26820  nbuhgr2vtx1edgb  26822  umgr2v2evd2  26997  2wlklem  27136  2wlkdlem5  27400  2wlkdlem10  27406  clwwlknonex2lem2  27579  3pthdlem1  27635  upgr4cycl4dv4e  27656  subfacp1lem3  32043  poimirlem1  34449  paireqne  43181  requad2  43296  ldepsnlinc  44069  rrx2pnecoorneor  44209  rrx2line  44234  rrx2linest  44236
  Copyright terms: Public domain W3C validator