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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569  ∀wral 3076  {csn 4584  ⟨cop 4834  ∪ ciun 4950   × cxp 5648

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-iun 4952  df-opab 5167  df-xp 5656  df-rel 5657

This theorem is used by:  ralxpf  5823  reu3op  6295  f1opr  7477  ffnov  7547  eqfnov  7550  ovn0ssdmfun  7590  funimassov  7599  f1stres  8026  f2ndres  8027  naddf  8695  ecopover  8846  xpf1o  9162  xpwdomg  9583  rankxplim  9900  imasaddfnlem  17706  imasvscafn  17715  comfeq  17886  isssc  18001  isfuncd  18046  cofucl  18069  funcres2b  18078  evlfcl  18402  uncfcurf  18419  yonedalem3  18460  yonedainv  18461  efgval2  19944  srgfcl  20428  txbas  23892  hausdiag  23970  tx1stc  23975  txkgen  23977  xkococn  23985  cnmpt21  23996  xkoinjcn  24012  tmdcn2  24414  clssubg  24434  qustgplem  24446  txmetcnp  24872  txmetcn  24873  qtopbaslem  25083  bndth  25285  cxpcn3  27082  mpodvdsmulf1o  27527  fsumdvdsmul  27528  dvdsmulf1o  27529  addsf  28374  xrofsup  33406  txpconn  36084  cvmlift2lem1  36154  cvmlift2lem12  36166  mclsax  36421  ismtyhmeolem  38832  dih1dimatlem  42480  ffnaov  48363  plusfreseq  49355  funcf2lem  50289  imaidfu  50320  imasubc  50361  imassc  50363  fucofulem2  50527