Theorem ralxp 5832

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1539  ∀wral 3050  {csn 4606  ⟨cop 4612  ∪ ciun 4971   × cxp 5663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pr 5412

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ral 3051  df-rex 3060  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-iun 4973  df-opab 5186  df-xp 5671  df-rel 5672

This theorem is referenced by:  ralxpf  5837  reu3op  6292  f1opr  7471  ffnov  7541  eqfnov  7544  funimassov  7592  f1stres  8020  f2ndres  8021  naddf  8701  ecopover  8843  xpf1o  9161  xpwdomg  9607  rankxplim  9901  imasaddfnlem  17544  imasvscafn  17553  comfeq  17720  isssc  17835  isfuncd  17881  cofucl  17904  funcres2b  17913  evlfcl  18237  uncfcurf  18254  yonedalem3  18295  yonedainv  18296  efgval2  19710  srgfcl  20161  txbas  23521  hausdiag  23599  tx1stc  23604  txkgen  23606  xkococn  23614  cnmpt21  23625  xkoinjcn  23641  tmdcn2  24043  clssubg  24063  qustgplem  24075  txmetcnp  24504  txmetcn  24505  qtopbaslem  24715  bndth  24926  cxpcn3  26727  mpodvdsmulf1o  27173  fsumdvdsmul  27174  dvdsmulf1o  27175  fsumdvdsmulOLD  27176  addsf  27951  xrofsup  32708  txpconn  35196  cvmlift2lem1  35266  cvmlift2lem12  35278  mclsax  35533  ismtyhmeolem  37770  dih1dimatlem  41290  ffnaov  47169  ovn0ssdmfun  48033  plusfreseq  48038  funcf2lem  48883  fucofulem2  48982