Theorem ralpr 4636

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

Step	Hyp	Ref	Expression
1		ralpr.1	. 2 ⊢ 𝐴 ∈ V
2		ralpr.2	. 2 ⊢ 𝐵 ∈ V
3		ralpr.3	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4		ralpr.4	. . 3 ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))
5	3, 4	ralprg 4630	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒)))
6	1, 2, 5	mp2an 689	1 ⊢ (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   ∈ wcel 2106  ∀wral 3064  Vcvv 3432  {cpr 4563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-v 3434  df-un 3892  df-sn 4562  df-pr 4564

This theorem is referenced by:  fprb  7069  fzprval  13317  fvinim0ffz  13506  wwlktovf1  14672  xpsfrnel  17273  xpsle  17290  isdrs2  18024  pmtrsn  19127  iblcnlem1  24952  lfuhgr1v0e  27621  nbgr2vtx1edg  27717  nbuhgr2vtx1edgb  27719  umgr2v2evd2  27894  2wlklem  28035  2wlkdlem5  28294  2wlkdlem10  28300  clwwlknonex2lem2  28472  3pthdlem1  28528  upgr4cycl4dv4e  28549  subfacp1lem3  33144  poimirlem1  35778  paireqne  44963  requad2  45075  ldepsnlinc  45849  rrx2pnecoorneor  46061  rrx2line  46086  rrx2linest  46088