Theorem ralxp 5753

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  ∀wral 3065  {csn 4562  ⟨cop 4568  ∪ ciun 4925   × cxp 5588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-iun 4927  df-opab 5138  df-xp 5596  df-rel 5597

This theorem is referenced by:  ralxpf  5758  reu3op  6199  f1opr  7340  ffnov  7410  eqfnov  7412  funimassov  7458  f1stres  7864  f2ndres  7865  ecopover  8619  xpf1o  8935  xpwdomg  9353  rankxplim  9646  imasaddfnlem  17248  imasvscafn  17257  comfeq  17424  isssc  17541  isfuncd  17589  cofucl  17612  funcres2b  17621  evlfcl  17949  uncfcurf  17966  yonedalem3  18007  yonedainv  18008  efgval2  19339  srgfcl  19760  txbas  22727  hausdiag  22805  tx1stc  22810  txkgen  22812  xkococn  22820  cnmpt21  22831  xkoinjcn  22847  tmdcn2  23249  clssubg  23269  qustgplem  23281  txmetcnp  23712  txmetcn  23713  qtopbaslem  23931  bndth  24130  cxpcn3  25910  dvdsmulf1o  26352  fsumdvdsmul  26353  xrofsup  31099  txpconn  33203  cvmlift2lem1  33273  cvmlift2lem12  33285  mclsax  33540  ismtyhmeolem  35971  dih1dimatlem  39350  ffnaov  44702  ovn0ssdmfun  45332  plusfreseq  45337  funcf2lem  46310