Theorem ralxp 5790

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  ∀wral 3051  {csn 4580  ⟨cop 4586  ∪ ciun 4946   × cxp 5622

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

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 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-iun 4948  df-opab 5161  df-xp 5630  df-rel 5631

This theorem is referenced by:  ralxpf  5795  reu3op  6250  f1opr  7414  ffnov  7484  eqfnov  7487  funimassov  7535  f1stres  7957  f2ndres  7958  naddf  8609  ecopover  8758  xpf1o  9067  xpwdomg  9490  rankxplim  9791  imasaddfnlem  17449  imasvscafn  17458  comfeq  17629  isssc  17744  isfuncd  17789  cofucl  17812  funcres2b  17821  evlfcl  18145  uncfcurf  18162  yonedalem3  18203  yonedainv  18204  efgval2  19653  srgfcl  20131  txbas  23511  hausdiag  23589  tx1stc  23594  txkgen  23596  xkococn  23604  cnmpt21  23615  xkoinjcn  23631  tmdcn2  24033  clssubg  24053  qustgplem  24065  txmetcnp  24491  txmetcn  24492  qtopbaslem  24702  bndth  24913  cxpcn3  26714  mpodvdsmulf1o  27160  fsumdvdsmul  27161  dvdsmulf1o  27162  fsumdvdsmulOLD  27163  addsf  27978  xrofsup  32847  txpconn  35426  cvmlift2lem1  35496  cvmlift2lem12  35508  mclsax  35763  ismtyhmeolem  38005  dih1dimatlem  41589  ffnaov  47445  ovn0ssdmfun  48405  plusfreseq  48410  funcf2lem  49326  imaidfu  49355  imasubc  49396  imassc  49398  fucofulem2  49556