Theorem ralxp 5788

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ∀wral 3044  {csn 4579  ⟨cop 4585  ∪ ciun 4944   × cxp 5621

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-iun 4946  df-opab 5158  df-xp 5629  df-rel 5630

This theorem is referenced by:  ralxpf  5793  reu3op  6244  f1opr  7409  ffnov  7479  eqfnov  7482  funimassov  7530  f1stres  7955  f2ndres  7956  naddf  8606  ecopover  8755  xpf1o  9063  xpwdomg  9496  rankxplim  9794  imasaddfnlem  17450  imasvscafn  17459  comfeq  17630  isssc  17745  isfuncd  17790  cofucl  17813  funcres2b  17822  evlfcl  18146  uncfcurf  18163  yonedalem3  18204  yonedainv  18205  efgval2  19621  srgfcl  20099  txbas  23470  hausdiag  23548  tx1stc  23553  txkgen  23555  xkococn  23563  cnmpt21  23574  xkoinjcn  23590  tmdcn2  23992  clssubg  24012  qustgplem  24024  txmetcnp  24451  txmetcn  24452  qtopbaslem  24662  bndth  24873  cxpcn3  26674  mpodvdsmulf1o  27120  fsumdvdsmul  27121  dvdsmulf1o  27122  fsumdvdsmulOLD  27123  addsf  27912  xrofsup  32723  txpconn  35207  cvmlift2lem1  35277  cvmlift2lem12  35289  mclsax  35544  ismtyhmeolem  37786  dih1dimatlem  41311  ffnaov  47187  ovn0ssdmfun  48147  plusfreseq  48152  funcf2lem  49070  imaidfu  49099  imasubc  49140  imassc  49142  fucofulem2  49300