Theorem ralxp 5749

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542  ∀wral 3066  {csn 4567  ⟨cop 4573  ∪ ciun 4930   × cxp 5588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pr 5356

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ral 3071  df-rex 3072  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574  df-iun 4932  df-opab 5142  df-xp 5596  df-rel 5597

This theorem is referenced by:  ralxpf  5754  reu3op  6194  f1opr  7325  ffnov  7395  eqfnov  7397  funimassov  7443  f1stres  7848  f2ndres  7849  ecopover  8593  xpf1o  8908  xpwdomg  9322  rankxplim  9638  imasaddfnlem  17237  imasvscafn  17246  comfeq  17413  isssc  17530  isfuncd  17578  cofucl  17601  funcres2b  17610  evlfcl  17938  uncfcurf  17955  yonedalem3  17996  yonedainv  17997  efgval2  19328  srgfcl  19749  txbas  22716  hausdiag  22794  tx1stc  22799  txkgen  22801  xkococn  22809  cnmpt21  22820  xkoinjcn  22836  tmdcn2  23238  clssubg  23258  qustgplem  23270  txmetcnp  23701  txmetcn  23702  qtopbaslem  23920  bndth  24119  cxpcn3  25899  dvdsmulf1o  26341  fsumdvdsmul  26342  xrofsup  31086  txpconn  33190  cvmlift2lem1  33260  cvmlift2lem12  33272  mclsax  33527  ismtyhmeolem  35958  dih1dimatlem  39339  ffnaov  44659  ovn0ssdmfun  45290  plusfreseq  45295  funcf2lem  46268