Theorem ralprg 4592

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.) (Proof shortened by AV, 8-Apr-2023.)

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		nfv 1915	. 2 ⊢ Ⅎ𝑥𝜓
2		nfv 1915	. 2 ⊢ Ⅎ𝑥𝜒
3		ralprg.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4		ralprg.2	. 2 ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))
5	1, 2, 3, 4	ralprgf 4590	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ {𝐴, 𝐵}𝜑 ↔ (𝜓 ∧ 𝜒)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∀wral 3106  {cpr 4527

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-v 3443  df-sbc 3721  df-un 3886  df-sn 4526  df-pr 4528

This theorem is referenced by:  raltpg  4594  ralpr  4596  reuprg0  4598  iinxprg  4974  disjprgw  5025  disjprg  5026  fpropnf1  7003  f12dfv  7008  f13dfv  7009  suppr  8919  infpr  8951  pfx2  14300  sumpr  15095  gcdcllem2  15839  lcmfpr  15961  joinval2lem  17610  meetval2lem  17624  sgrp2rid2  18083  sgrp2nmndlem4  18085  sgrp2nmndlem5  18086  iccntr  23426  limcun  24498  cplgr3v  27225  3wlkdlem4  27947  frgr3v  28060  3vfriswmgr  28063  prsiga  31500  paireqne  44028