Theorem ralprg 4653

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 2177, ax-12 2212. (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 4587	. . . 4 ⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
2	1	raleqi 3317	. . 3 ⊢ (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ ∀𝑥 ∈ ({𝐴} ∪ {𝐵})𝜑)
3		ralunb 4195	. . 3 ⊢ (∀𝑥 ∈ ({𝐴} ∪ {𝐵})𝜑 ↔ (∀𝑥 ∈ {𝐴}𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑))
4	2, 3	bitri 278	. 2 ⊢ (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (∀𝑥 ∈ {𝐴}𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑))
5		ralprg.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
6	5	ralsng 4632	. . 3 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ {𝐴}𝜑 ↔ 𝜓))
7		ralprg.2	. . . 4 ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))
8	7	ralsng 4632	. . 3 ⊢ (𝐵 ∈ 𝑊 → (∀𝑥 ∈ {𝐵}𝜑 ↔ 𝜒))
9	6, 8	bi2anan9 650	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((∀𝑥 ∈ {𝐴}𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑) ↔ (𝜓 ∧ 𝜒)))
10	4, 9	bitrid 286	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ∈ wcel 2144  ∀wral 3076   ∪ cun 4149  {csn 4584  {cpr 4586

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-v 3452  df-un 4151  df-sn 4585  df-pr 4587

This theorem is used by:  rexprg  4654  raltpg  4655  ralpr  4657  reuprg0  4659  iinxprg  5048  disjprg  5098  fpropnf1  7272  f12dfv  7282  f13dfv  7283  suppr  9468  infpr  9501  pfx2  15104  sumpr  15920  gcdcllem2  16676  lcmfpr  16808  joinval2lem  18558  meetval2lem  18572  sgrp2rid2  19131  sgrp2nmndlem4  19133  sgrp2nmndlem5  19134  iccntr  25147  limcun  26221  cplgr3v  30022  3wlkdlem4  30769  frgr3v  30882  3vfriswmgr  30885  prsiga  34810  paireqne  48687