Theorem ralxp 5185

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

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475  ∀wral 2896  {csn 4125  ⟨cop 4131  ∪ ciun 4455   × cxp 5036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-iun 4457  df-opab 4644  df-xp 5044  df-rel 5045

This theorem is referenced by:  ralxpf  5190  issref  5428  ffnov  6662  eqfnov  6664  funimassov  6709  f1stres  7081  f2ndres  7082  ecopover  7738  ecopoverOLD  7739  xpf1o  8007  xpwdomg  8373  rankxplim  8625  imasaddfnlem  16011  imasvscafn  16020  comfeq  16189  isssc  16303  isfuncd  16348  cofucl  16371  funcres2b  16380  evlfcl  16685  uncfcurf  16702  yonedalem3  16743  yonedainv  16744  efgval2  17960  srgfcl  18338  txbas  21180  hausdiag  21258  tx1stc  21263  txkgen  21265  xkococn  21273  cnmpt21  21284  xkoinjcn  21300  tmdcn2  21703  clssubg  21722  qustgplem  21734  txmetcnp  22162  txmetcn  22163  qtopbaslem  22372  bndth  22565  cxpcn3  24289  dvdsmulf1o  24720  fsumdvdsmul  24721  xrofsup  28923  txpcon  30468  cvmlift2lem1  30538  cvmlift2lem12  30550  mclsax  30720  f1opr  32689  ismtyhmeolem  32773  dih1dimatlem  35636  ffnaov  39928  ovn0ssdmfun  41557  plusfreseq  41562