Theorem ralxp 5695

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1543  ∀wral 3051  {csn 4527  ⟨cop 4533  ∪ ciun 4890   × cxp 5534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-sbc 3684  df-csb 3799  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-iun 4892  df-opab 5102  df-xp 5542  df-rel 5543

This theorem is referenced by:  ralxpf  5700  reu3op  6135  f1opr  7245  ffnov  7315  eqfnov  7317  funimassov  7363  f1stres  7763  f2ndres  7764  ecopover  8481  xpf1o  8786  xpwdomg  9179  rankxplim  9460  imasaddfnlem  16987  imasvscafn  16996  comfeq  17163  isssc  17279  isfuncd  17325  cofucl  17348  funcres2b  17357  evlfcl  17684  uncfcurf  17701  yonedalem3  17742  yonedainv  17743  efgval2  19068  srgfcl  19484  txbas  22418  hausdiag  22496  tx1stc  22501  txkgen  22503  xkococn  22511  cnmpt21  22522  xkoinjcn  22538  tmdcn2  22940  clssubg  22960  qustgplem  22972  txmetcnp  23399  txmetcn  23400  qtopbaslem  23610  bndth  23809  cxpcn3  25588  dvdsmulf1o  26030  fsumdvdsmul  26031  xrofsup  30764  txpconn  32861  cvmlift2lem1  32931  cvmlift2lem12  32943  mclsax  33198  ismtyhmeolem  35648  dih1dimatlem  39029  ffnaov  44306  ovn0ssdmfun  44937  plusfreseq  44942  funcf2lem  45915