Theorem ralxp 5790

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547  ∀wral 3054  {csn 4562  ⟨cop 4568  ∪ ciun 4928   × cxp 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-iun 4930  df-opab 5142  df-xp 5631  df-rel 5632

This theorem is referenced by:  ralxpf  5795  reu3op  6250  f1opr  7419  ffnov  7489  eqfnov  7492  funimassov  7540  f1stres  7962  f2ndres  7963  naddf  8614  ecopover  8765  xpf1o  9074  xpwdomg  9497  rankxplim  9801  imasaddfnlem  17490  imasvscafn  17499  comfeq  17670  isssc  17785  isfuncd  17830  cofucl  17853  funcres2b  17862  evlfcl  18186  uncfcurf  18203  yonedalem3  18244  yonedainv  18245  efgval2  19697  srgfcl  20175  txbas  23557  hausdiag  23635  tx1stc  23640  txkgen  23642  xkococn  23650  cnmpt21  23661  xkoinjcn  23677  tmdcn2  24079  clssubg  24099  qustgplem  24111  txmetcnp  24537  txmetcn  24538  qtopbaslem  24748  bndth  24950  cxpcn3  26737  mpodvdsmulf1o  27182  fsumdvdsmul  27183  dvdsmulf1o  27184  addsf  27999  xrofsup  32866  txpconn  35467  cvmlift2lem1  35537  cvmlift2lem12  35549  mclsax  35804  ismtyhmeolem  38178  dih1dimatlem  41828  ffnaov  47669  ovn0ssdmfun  48657  plusfreseq  48662  funcf2lem  49578  imaidfu  49607  imasubc  49648  imassc  49650  fucofulem2  49808