Theorem ralpr 4661

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 4657	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒)))
6	1, 2, 5	mp2an 705	1 ⊢ (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2147  ∀wral 3080  Vcvv 3454  {cpr 4590

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-v 3456  df-un 4154  df-sn 4589  df-pr 4591

This theorem is used by:  fprb  7219  fzprval  13743  fvinim0ffz  13948  wwlktovf1  15136  xpsfrnel  17760  xpsle  17777  isdrs2  18506  degenmgm  19163  degenmgm2  19166  pmtrsn  19760  iblcnlem1  26135  lfuhgr1v0e  29862  nbgr2vtx1edg  29958  nbuhgr2vtx1edgb  29960  umgr2v2evd2  30135  2wlklem  30273  dfpth2  30341  2wlkdlem5  30545  2wlkdlem10  30551  clwwlknonex2lem2  30726  3pthdlem1  30792  upgr4cycl4dv4e  30813  subfacp1lem3  36113  mh-infprim2bi  37512  poimirlem1  38730  paireqne  48796  requad2  48924  ldepsnlinc  49823  rrx2pnecoorneor  50031  rrx2line  50055  rrx2linest  50057