Theorem ralxp 5844

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1533  ∀wral 3050  {csn 4630  ⟨cop 4636  ∪ ciun 4997   × cxp 5676

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pr 5429

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-iun 4999  df-opab 5212  df-xp 5684  df-rel 5685

This theorem is referenced by:  ralxpf  5849  reu3op  6298  f1opr  7476  ffnov  7547  eqfnov  7550  funimassov  7598  f1stres  8018  f2ndres  8019  naddf  8702  ecopover  8840  xpf1o  9164  xpwdomg  9610  rankxplim  9904  imasaddfnlem  17513  imasvscafn  17522  comfeq  17689  isssc  17806  isfuncd  17854  cofucl  17877  funcres2b  17886  evlfcl  18217  uncfcurf  18234  yonedalem3  18275  yonedainv  18276  efgval2  19691  srgfcl  20148  txbas  23515  hausdiag  23593  tx1stc  23598  txkgen  23600  xkococn  23608  cnmpt21  23619  xkoinjcn  23635  tmdcn2  24037  clssubg  24057  qustgplem  24069  txmetcnp  24500  txmetcn  24501  qtopbaslem  24719  bndth  24928  cxpcn3  26728  mpodvdsmulf1o  27171  fsumdvdsmul  27172  dvdsmulf1o  27173  fsumdvdsmulOLD  27174  addsf  27945  xrofsup  32619  txpconn  34973  cvmlift2lem1  35043  cvmlift2lem12  35055  mclsax  35310  ismtyhmeolem  37408  dih1dimatlem  40932  ffnaov  46717  ovn0ssdmfun  47407  plusfreseq  47412  funcf2lem  48210