Theorem ralxp 5805

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ∀wral 3044  {csn 4589  ⟨cop 4595  ∪ ciun 4955   × cxp 5636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-iun 4957  df-opab 5170  df-xp 5644  df-rel 5645

This theorem is referenced by:  ralxpf  5810  reu3op  6265  f1opr  7445  ffnov  7515  eqfnov  7518  funimassov  7566  f1stres  7992  f2ndres  7993  naddf  8645  ecopover  8794  xpf1o  9103  xpwdomg  9538  rankxplim  9832  imasaddfnlem  17491  imasvscafn  17500  comfeq  17667  isssc  17782  isfuncd  17827  cofucl  17850  funcres2b  17859  evlfcl  18183  uncfcurf  18200  yonedalem3  18241  yonedainv  18242  efgval2  19654  srgfcl  20105  txbas  23454  hausdiag  23532  tx1stc  23537  txkgen  23539  xkococn  23547  cnmpt21  23558  xkoinjcn  23574  tmdcn2  23976  clssubg  23996  qustgplem  24008  txmetcnp  24435  txmetcn  24436  qtopbaslem  24646  bndth  24857  cxpcn3  26658  mpodvdsmulf1o  27104  fsumdvdsmul  27105  dvdsmulf1o  27106  fsumdvdsmulOLD  27107  addsf  27889  xrofsup  32690  txpconn  35219  cvmlift2lem1  35289  cvmlift2lem12  35301  mclsax  35556  ismtyhmeolem  37798  dih1dimatlem  41323  ffnaov  47200  ovn0ssdmfun  48147  plusfreseq  48152  funcf2lem  49070  imaidfu  49099  imasubc  49140  imassc  49142  fucofulem2  49300