Theorem ralxp 5603

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1522  ∀wral 3105  {csn 4476  ⟨cop 4482  ∪ ciun 4829   × cxp 5446

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5099  ax-nul 5106  ax-pr 5226

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3710  df-csb 3816  df-dif 3866  df-un 3868  df-in 3870  df-ss 3878  df-nul 4216  df-if 4386  df-sn 4477  df-pr 4479  df-op 4483  df-iun 4831  df-opab 5029  df-xp 5454  df-rel 5455

This theorem is referenced by:  ralxpf  5608  reu3op  6023  f1opr  7074  ffnov  7139  eqfnov  7141  funimassov  7186  f1stres  7574  f2ndres  7575  ecopover  8256  xpf1o  8531  xpwdomg  8900  rankxplim  9159  imasaddfnlem  16635  imasvscafn  16644  comfeq  16810  isssc  16924  isfuncd  16969  cofucl  16992  funcres2b  17001  evlfcl  17306  uncfcurf  17323  yonedalem3  17364  yonedainv  17365  efgval2  18582  srgfcl  18960  txbas  21864  hausdiag  21942  tx1stc  21947  txkgen  21949  xkococn  21957  cnmpt21  21968  xkoinjcn  21984  tmdcn2  22386  clssubg  22405  qustgplem  22417  txmetcnp  22845  txmetcn  22846  qtopbaslem  23055  bndth  23250  cxpcn3  25015  dvdsmulf1o  25458  fsumdvdsmul  25459  xrofsup  30185  txpconn  32094  cvmlift2lem1  32164  cvmlift2lem12  32176  mclsax  32431  ismtyhmeolem  34640  dih1dimatlem  38022  ffnaov  42941  ovn0ssdmfun  43543  plusfreseq  43548