Theorem ralprg 4626

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1533   ∈ wcel 2110  ∀wral 3138  {cpr 4563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-v 3497  df-sbc 3773  df-un 3941  df-sn 4562  df-pr 4564

This theorem is referenced by:  raltpg  4628  ralpr  4630  reuprg0  4632  iinxprg  5004  disjprgw  5054  disjprg  5055  fpropnf1  7019  f12dfv  7024  f13dfv  7025  suppr  8929  infpr  8961  pfx2  14303  sumpr  15097  gcdcllem2  15843  lcmfpr  15965  joinval2lem  17612  meetval2lem  17626  sgrp2rid2  18085  sgrp2nmndlem4  18087  sgrp2nmndlem5  18088  iccntr  23423  limcun  24487  cplgr3v  27211  3wlkdlem4  27935  frgr3v  28048  3vfriswmgr  28051  prsiga  31385  paireqne  43666