Theorem ralxp 5712

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537  ∀wral 3138  {csn 4567  ⟨cop 4573  ∪ ciun 4919   × cxp 5553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-iun 4921  df-opab 5129  df-xp 5561  df-rel 5562

This theorem is referenced by:  ralxpf  5717  reu3op  6143  f1opr  7210  ffnov  7278  eqfnov  7280  funimassov  7325  f1stres  7713  f2ndres  7714  ecopover  8401  xpf1o  8679  xpwdomg  9049  rankxplim  9308  imasaddfnlem  16801  imasvscafn  16810  comfeq  16976  isssc  17090  isfuncd  17135  cofucl  17158  funcres2b  17167  evlfcl  17472  uncfcurf  17489  yonedalem3  17530  yonedainv  17531  efgval2  18850  srgfcl  19265  txbas  22175  hausdiag  22253  tx1stc  22258  txkgen  22260  xkococn  22268  cnmpt21  22279  xkoinjcn  22295  tmdcn2  22697  clssubg  22717  qustgplem  22729  txmetcnp  23157  txmetcn  23158  qtopbaslem  23367  bndth  23562  cxpcn3  25329  dvdsmulf1o  25771  fsumdvdsmul  25772  xrofsup  30492  txpconn  32479  cvmlift2lem1  32549  cvmlift2lem12  32561  mclsax  32816  ismtyhmeolem  35097  dih1dimatlem  38480  ffnaov  43418  ovn0ssdmfun  44054  plusfreseq  44059