Theorem ralprg 4648

Description: Convert a restricted universal quantification over a pair to a conjunction. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.) Avoid ax-10 2146, ax-12 2182. (Revised by GG, 30-Sep-2024.)

Hypotheses

Ref	Expression
ralprg.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
ralprg.2	⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))

Assertion

Ref	Expression
ralprg	⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒)))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜓,𝑥   𝜒,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝑉(𝑥)   𝑊(𝑥)

Proof of Theorem ralprg

Step	Hyp	Ref	Expression
1		df-pr 4578	. . . 4 ⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
2	1	raleqi 3291	. . 3 ⊢ (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ ∀𝑥 ∈ ({𝐴} ∪ {𝐵})𝜑)
3		ralunb 4146	. . 3 ⊢ (∀𝑥 ∈ ({𝐴} ∪ {𝐵})𝜑 ↔ (∀𝑥 ∈ {𝐴}𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑))
4	2, 3	bitri 275	. 2 ⊢ (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (∀𝑥 ∈ {𝐴}𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑))
5		ralprg.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
6	5	ralsng 4627	. . 3 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓))
7		ralprg.2	. . . 4 ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))
8	7	ralsng 4627	. . 3 ⊢ (𝐵 ∈ 𝑊 → (∀𝑥 ∈ {𝐵}𝜑 ↔ 𝜒))
9	6, 8	bi2anan9 638	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((∀𝑥 ∈ {𝐴}𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑) ↔ (𝜓 ∧ 𝜒)))
10	4, 9	bitrid 283	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ∀wral 3048   ∪ cun 3896  {csn 4575  {cpr 4577

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-v 3439  df-un 3903  df-sn 4576  df-pr 4578

This theorem is referenced by:  rexprg  4649  raltpg  4650  ralpr  4652  reuprg0  4654  iinxprg  5039  disjprg  5089  fpropnf1  7207  f12dfv  7213  f13dfv  7214  suppr  9363  infpr  9396  pfx2  14856  sumpr  15657  gcdcllem2  16413  lcmfpr  16540  joinval2lem  18286  meetval2lem  18300  sgrp2rid2  18836  sgrp2nmndlem4  18838  sgrp2nmndlem5  18839  iccntr  24738  limcun  25824  cplgr3v  29415  3wlkdlem4  30144  frgr3v  30257  3vfriswmgr  30260  prsiga  34165  paireqne  47635