Theorem ralxp 5825

Description: Universal quantification restricted to a Cartesian product is equivalent to a double restricted quantification. The hypothesis specifies an implicit substitution. (Contributed by NM, 7-Feb-2004.) (Revised by Mario Carneiro, 29-Dec-2014.)

Hypothesis

Ref	Expression
ralxp.1	⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
ralxp	⊢ (∀𝑥 ∈ (𝐴 × 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜓)

Distinct variable groups:   𝑥,𝑦,𝑧,𝐴   𝑥,𝐵,𝑧   𝜑,𝑦,𝑧   𝜓,𝑥   𝑦,𝐵

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦, 𝑧)

Proof of Theorem ralxp

Step	Hyp	Ref	Expression
1		iunxpconst 5732	. . 3 ⊢ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵) = (𝐴 × 𝐵)
2	1	raleqi 3319	. 2 ⊢ (∀𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵)𝜑 ↔ ∀𝑥 ∈ (𝐴 × 𝐵)𝜑)
3		ralxp.1	. . 3 ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝜑 ↔ 𝜓))
4	3	raliunxp 5823	. 2 ⊢ (∀𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜓)
5	2, 4	bitr3i 280	1 ⊢ (∀𝑥 ∈ (𝐴 × 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ∀wral 3078  {csn 4587  ⟨cop 4593  ∪ ciun 4954   × cxp 5657

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-pr 5402

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-iun 4956  df-opab 5172  df-xp 5665  df-rel 5666

This theorem is used by:  ralxpf  5830  reu3op  6294  f1opr  7473  ffnov  7543  eqfnov  7546  ovn0ssdmfun  7586  funimassov  7595  f1stres  8014  f2ndres  8015  naddf  8674  ecopover  8825  xpf1o  9141  xpwdomg  9561  rankxplim  9865  imasaddfnlem  17620  imasvscafn  17629  comfeq  17800  isssc  17915  isfuncd  17960  cofucl  17983  funcres2b  17992  evlfcl  18316  uncfcurf  18333  yonedalem3  18374  yonedainv  18375  efgval2  19857  srgfcl  20341  txbas  23799  hausdiag  23877  tx1stc  23882  txkgen  23884  xkococn  23892  cnmpt21  23903  xkoinjcn  23919  tmdcn2  24321  clssubg  24341  qustgplem  24353  txmetcnp  24779  txmetcn  24780  qtopbaslem  24990  bndth  25192  cxpcn3  26993  mpodvdsmulf1o  27438  fsumdvdsmul  27439  dvdsmulf1o  27440  addsf  28255  xrofsup  33246  txpconn  35819  cvmlift2lem1  35889  cvmlift2lem12  35901  mclsax  36156  ismtyhmeolem  38562  dih1dimatlem  42210  ffnaov  48095  plusfreseq  49087  funcf2lem  50015  imaidfu  50044  imasubc  50085  imassc  50087  fucofulem2  50245