Theorem ralxp 5817

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1563  ∀wral 3079  {csn 4585  ⟨cop 4591  ∪ ciun 4951   × cxp 5649

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5250  ax-pr 5394

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-iun 4953  df-opab 5167  df-xp 5657  df-rel 5658

This theorem is referenced by:  ralxpf  5822  reu3op  6282  f1opr  7456  ffnov  7526  eqfnov  7529  funimassov  7577  f1stres  7998  f2ndres  7999  naddf  8656  ecopover  8807  xpf1o  9115  xpwdomg  9535  rankxplim  9839  imasaddfnlem  17570  imasvscafn  17579  comfeq  17750  isssc  17865  isfuncd  17910  cofucl  17933  funcres2b  17942  evlfcl  18266  uncfcurf  18283  yonedalem3  18324  yonedainv  18325  efgval2  19782  srgfcl  20266  txbas  23681  hausdiag  23759  tx1stc  23764  txkgen  23766  xkococn  23774  cnmpt21  23785  xkoinjcn  23801  tmdcn2  24203  clssubg  24223  qustgplem  24235  txmetcnp  24661  txmetcn  24662  qtopbaslem  24872  bndth  25074  cxpcn3  26867  mpodvdsmulf1o  27312  fsumdvdsmul  27313  dvdsmulf1o  27314  addsf  28129  xrofsup  33020  txpconn  35590  cvmlift2lem1  35660  cvmlift2lem12  35672  mclsax  35927  ismtyhmeolem  38310  dih1dimatlem  41960  ffnaov  47792  ovn0ssdmfun  48780  plusfreseq  48785  funcf2lem  49711  imaidfu  49740  imasubc  49781  imassc  49783  fucofulem2  49941