Theorem ralxp 5798

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ∀wral 3052  {csn 4582  ⟨cop 4588  ∪ ciun 4948   × cxp 5630

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 2709  ax-sep 5243  ax-pr 5379

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 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-iun 4950  df-opab 5163  df-xp 5638  df-rel 5639

This theorem is referenced by:  ralxpf  5803  reu3op  6258  f1opr  7424  ffnov  7494  eqfnov  7497  funimassov  7545  f1stres  7967  f2ndres  7968  naddf  8619  ecopover  8770  xpf1o  9079  xpwdomg  9502  rankxplim  9803  imasaddfnlem  17461  imasvscafn  17470  comfeq  17641  isssc  17756  isfuncd  17801  cofucl  17824  funcres2b  17833  evlfcl  18157  uncfcurf  18174  yonedalem3  18215  yonedainv  18216  efgval2  19665  srgfcl  20143  txbas  23523  hausdiag  23601  tx1stc  23606  txkgen  23608  xkococn  23616  cnmpt21  23627  xkoinjcn  23643  tmdcn2  24045  clssubg  24065  qustgplem  24077  txmetcnp  24503  txmetcn  24504  qtopbaslem  24714  bndth  24925  cxpcn3  26726  mpodvdsmulf1o  27172  fsumdvdsmul  27173  dvdsmulf1o  27174  fsumdvdsmulOLD  27175  addsf  27990  xrofsup  32857  txpconn  35445  cvmlift2lem1  35515  cvmlift2lem12  35527  mclsax  35782  ismtyhmeolem  38052  dih1dimatlem  41702  ffnaov  47556  ovn0ssdmfun  48516  plusfreseq  48521  funcf2lem  49437  imaidfu  49466  imasubc  49507  imassc  49509  fucofulem2  49667