Theorem ralxp 5781

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  ∀wral 3047  {csn 4576  ⟨cop 4582  ∪ ciun 4941   × cxp 5614

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-iun 4943  df-opab 5154  df-xp 5622  df-rel 5623

This theorem is referenced by:  ralxpf  5786  reu3op  6239  f1opr  7402  ffnov  7472  eqfnov  7475  funimassov  7523  f1stres  7945  f2ndres  7946  naddf  8596  ecopover  8745  xpf1o  9052  xpwdomg  9471  rankxplim  9772  imasaddfnlem  17432  imasvscafn  17441  comfeq  17612  isssc  17727  isfuncd  17772  cofucl  17795  funcres2b  17804  evlfcl  18128  uncfcurf  18145  yonedalem3  18186  yonedainv  18187  efgval2  19637  srgfcl  20115  txbas  23483  hausdiag  23561  tx1stc  23566  txkgen  23568  xkococn  23576  cnmpt21  23587  xkoinjcn  23603  tmdcn2  24005  clssubg  24025  qustgplem  24037  txmetcnp  24463  txmetcn  24464  qtopbaslem  24674  bndth  24885  cxpcn3  26686  mpodvdsmulf1o  27132  fsumdvdsmul  27133  dvdsmulf1o  27134  fsumdvdsmulOLD  27135  addsf  27926  xrofsup  32748  txpconn  35274  cvmlift2lem1  35344  cvmlift2lem12  35356  mclsax  35611  ismtyhmeolem  37850  dih1dimatlem  41374  ffnaov  47236  ovn0ssdmfun  48196  plusfreseq  48201  funcf2lem  49119  imaidfu  49148  imasubc  49189  imassc  49191  fucofulem2  49349