Theorem ralxp 5854

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1536  ∀wral 3058  {csn 4630  ⟨cop 4636  ∪ ciun 4995   × cxp 5686

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-iun 4997  df-opab 5210  df-xp 5694  df-rel 5695

This theorem is referenced by:  ralxpf  5859  reu3op  6313  f1opr  7488  ffnov  7558  eqfnov  7561  funimassov  7609  f1stres  8036  f2ndres  8037  naddf  8717  ecopover  8859  xpf1o  9177  xpwdomg  9622  rankxplim  9916  imasaddfnlem  17574  imasvscafn  17583  comfeq  17750  isssc  17867  isfuncd  17915  cofucl  17938  funcres2b  17947  evlfcl  18278  uncfcurf  18295  yonedalem3  18336  yonedainv  18337  efgval2  19756  srgfcl  20213  txbas  23590  hausdiag  23668  tx1stc  23673  txkgen  23675  xkococn  23683  cnmpt21  23694  xkoinjcn  23710  tmdcn2  24112  clssubg  24132  qustgplem  24144  txmetcnp  24575  txmetcn  24576  qtopbaslem  24794  bndth  25003  cxpcn3  26805  mpodvdsmulf1o  27251  fsumdvdsmul  27252  dvdsmulf1o  27253  fsumdvdsmulOLD  27254  addsf  28029  xrofsup  32777  txpconn  35216  cvmlift2lem1  35286  cvmlift2lem12  35298  mclsax  35553  ismtyhmeolem  37790  dih1dimatlem  41311  ffnaov  47148  ovn0ssdmfun  48002  plusfreseq  48007  funcf2lem  48810