Theorem ralxp 5852

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ∀wral 3061  {csn 4626  ⟨cop 4632  ∪ ciun 4991   × cxp 5683

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-iun 4993  df-opab 5206  df-xp 5691  df-rel 5692

This theorem is referenced by:  ralxpf  5857  reu3op  6312  f1opr  7489  ffnov  7559  eqfnov  7562  funimassov  7610  f1stres  8038  f2ndres  8039  naddf  8719  ecopover  8861  xpf1o  9179  xpwdomg  9625  rankxplim  9919  imasaddfnlem  17573  imasvscafn  17582  comfeq  17749  isssc  17864  isfuncd  17910  cofucl  17933  funcres2b  17942  evlfcl  18267  uncfcurf  18284  yonedalem3  18325  yonedainv  18326  efgval2  19742  srgfcl  20193  txbas  23575  hausdiag  23653  tx1stc  23658  txkgen  23660  xkococn  23668  cnmpt21  23679  xkoinjcn  23695  tmdcn2  24097  clssubg  24117  qustgplem  24129  txmetcnp  24560  txmetcn  24561  qtopbaslem  24779  bndth  24990  cxpcn3  26791  mpodvdsmulf1o  27237  fsumdvdsmul  27238  dvdsmulf1o  27239  fsumdvdsmulOLD  27240  addsf  28015  xrofsup  32771  txpconn  35237  cvmlift2lem1  35307  cvmlift2lem12  35319  mclsax  35574  ismtyhmeolem  37811  dih1dimatlem  41331  ffnaov  47211  ovn0ssdmfun  48075  plusfreseq  48080  funcf2lem  48914  fucofulem2  49006