Theorem ralxp 5796

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ∀wral 3051  {csn 4567  ⟨cop 4573  ∪ ciun 4933   × cxp 5629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-iun 4935  df-opab 5148  df-xp 5637  df-rel 5638

This theorem is referenced by:  ralxpf  5801  reu3op  6256  f1opr  7423  ffnov  7493  eqfnov  7496  funimassov  7544  f1stres  7966  f2ndres  7967  naddf  8617  ecopover  8768  xpf1o  9077  xpwdomg  9500  rankxplim  9803  imasaddfnlem  17492  imasvscafn  17501  comfeq  17672  isssc  17787  isfuncd  17832  cofucl  17855  funcres2b  17864  evlfcl  18188  uncfcurf  18205  yonedalem3  18246  yonedainv  18247  efgval2  19699  srgfcl  20177  txbas  23532  hausdiag  23610  tx1stc  23615  txkgen  23617  xkococn  23625  cnmpt21  23636  xkoinjcn  23652  tmdcn2  24054  clssubg  24074  qustgplem  24086  txmetcnp  24512  txmetcn  24513  qtopbaslem  24723  bndth  24925  cxpcn3  26712  mpodvdsmulf1o  27157  fsumdvdsmul  27158  dvdsmulf1o  27159  addsf  27974  xrofsup  32840  txpconn  35414  cvmlift2lem1  35484  cvmlift2lem12  35496  mclsax  35751  ismtyhmeolem  38125  dih1dimatlem  41775  ffnaov  47647  ovn0ssdmfun  48635  plusfreseq  48640  funcf2lem  49556  imaidfu  49585  imasubc  49626  imassc  49628  fucofulem2  49786