Theorem ralxp 5832

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ∀wral 3082  {csn 4594  ⟨cop 4600  ∪ ciun 4961   × cxp 5664

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-pr 5409

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-iun 4963  df-opab 5179  df-xp 5672  df-rel 5673

This theorem is used by:  ralxpf  5837  reu3op  6300  f1opr  7479  ffnov  7549  eqfnov  7552  funimassov  7600  f1stres  8019  f2ndres  8020  naddf  8677  ecopover  8828  xpf1o  9137  xpwdomg  9557  rankxplim  9861  imasaddfnlem  17607  imasvscafn  17616  comfeq  17787  isssc  17902  isfuncd  17947  cofucl  17970  funcres2b  17979  evlfcl  18303  uncfcurf  18320  yonedalem3  18361  yonedainv  18362  efgval2  19825  srgfcl  20309  txbas  23761  hausdiag  23839  tx1stc  23844  txkgen  23846  xkococn  23854  cnmpt21  23865  xkoinjcn  23881  tmdcn2  24283  clssubg  24303  qustgplem  24315  txmetcnp  24741  txmetcn  24742  qtopbaslem  24952  bndth  25154  cxpcn3  26950  mpodvdsmulf1o  27395  fsumdvdsmul  27396  dvdsmulf1o  27397  addsf  28212  xrofsup  33149  txpconn  35745  cvmlift2lem1  35815  cvmlift2lem12  35827  mclsax  36082  ismtyhmeolem  38496  dih1dimatlem  42144  ffnaov  47977  ovn0ssdmfun  48965  plusfreseq  48970  funcf2lem  49900  imaidfu  49929  imasubc  49970  imassc  49972  fucofulem2  50130