Theorem ralxp 5821

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 5727	. . 3 ⊢ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵) = (𝐴 × 𝐵)
2	1	raleqi 3303	. 2 ⊢ (∀𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵)𝜑 ↔ ∀𝑥 ∈ (𝐴 × 𝐵)𝜑)
3		ralxp.1	. . 3 ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝜑 ↔ 𝜓))
4	3	raliunxp 5819	. 2 ⊢ (∀𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜓)
5	2, 4	bitr3i 277	1 ⊢ (∀𝑥 ∈ (𝐴 × 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ∀wral 3051  {csn 4601  ⟨cop 4607  ∪ ciun 4967   × cxp 5652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-iun 4969  df-opab 5182  df-xp 5660  df-rel 5661

This theorem is referenced by:  ralxpf  5826  reu3op  6281  f1opr  7463  ffnov  7533  eqfnov  7536  funimassov  7584  f1stres  8012  f2ndres  8013  naddf  8693  ecopover  8835  xpf1o  9153  xpwdomg  9599  rankxplim  9893  imasaddfnlem  17542  imasvscafn  17551  comfeq  17718  isssc  17833  isfuncd  17878  cofucl  17901  funcres2b  17910  evlfcl  18234  uncfcurf  18251  yonedalem3  18292  yonedainv  18293  efgval2  19705  srgfcl  20156  txbas  23505  hausdiag  23583  tx1stc  23588  txkgen  23590  xkococn  23598  cnmpt21  23609  xkoinjcn  23625  tmdcn2  24027  clssubg  24047  qustgplem  24059  txmetcnp  24486  txmetcn  24487  qtopbaslem  24697  bndth  24908  cxpcn3  26710  mpodvdsmulf1o  27156  fsumdvdsmul  27157  dvdsmulf1o  27158  fsumdvdsmulOLD  27159  addsf  27941  xrofsup  32744  txpconn  35254  cvmlift2lem1  35324  cvmlift2lem12  35336  mclsax  35591  ismtyhmeolem  37828  dih1dimatlem  41348  ffnaov  47228  ovn0ssdmfun  48134  plusfreseq  48139  funcf2lem  49046  imaidfu  49069  imasubc  49091  imassc  49093  fucofulem2  49222