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 1542  ∀wral 3052  {csn 4568  ⟨cop 4574  ∪ ciun 4934   × cxp 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-iun 4936  df-opab 5149  df-xp 5630  df-rel 5631

This theorem is referenced by:  ralxpf  5795  reu3op  6250  f1opr  7416  ffnov  7486  eqfnov  7489  funimassov  7537  f1stres  7959  f2ndres  7960  naddf  8610  ecopover  8761  xpf1o  9070  xpwdomg  9493  rankxplim  9794  imasaddfnlem  17483  imasvscafn  17492  comfeq  17663  isssc  17778  isfuncd  17823  cofucl  17846  funcres2b  17855  evlfcl  18179  uncfcurf  18196  yonedalem3  18237  yonedainv  18238  efgval2  19690  srgfcl  20168  txbas  23542  hausdiag  23620  tx1stc  23625  txkgen  23627  xkococn  23635  cnmpt21  23646  xkoinjcn  23662  tmdcn2  24064  clssubg  24084  qustgplem  24096  txmetcnp  24522  txmetcn  24523  qtopbaslem  24733  bndth  24935  cxpcn3  26725  mpodvdsmulf1o  27171  fsumdvdsmul  27172  dvdsmulf1o  27173  addsf  27988  xrofsup  32855  txpconn  35430  cvmlift2lem1  35500  cvmlift2lem12  35512  mclsax  35767  ismtyhmeolem  38139  dih1dimatlem  41789  ffnaov  47659  ovn0ssdmfun  48647  plusfreseq  48652  funcf2lem  49568  imaidfu  49597  imasubc  49638  imassc  49640  fucofulem2  49798