Theorem ralxp 5808

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ∀wral 3045  {csn 4592  ⟨cop 4598  ∪ ciun 4958   × cxp 5639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-iun 4960  df-opab 5173  df-xp 5647  df-rel 5648

This theorem is referenced by:  ralxpf  5813  reu3op  6268  f1opr  7448  ffnov  7518  eqfnov  7521  funimassov  7569  f1stres  7995  f2ndres  7996  naddf  8648  ecopover  8797  xpf1o  9109  xpwdomg  9545  rankxplim  9839  imasaddfnlem  17498  imasvscafn  17507  comfeq  17674  isssc  17789  isfuncd  17834  cofucl  17857  funcres2b  17866  evlfcl  18190  uncfcurf  18207  yonedalem3  18248  yonedainv  18249  efgval2  19661  srgfcl  20112  txbas  23461  hausdiag  23539  tx1stc  23544  txkgen  23546  xkococn  23554  cnmpt21  23565  xkoinjcn  23581  tmdcn2  23983  clssubg  24003  qustgplem  24015  txmetcnp  24442  txmetcn  24443  qtopbaslem  24653  bndth  24864  cxpcn3  26665  mpodvdsmulf1o  27111  fsumdvdsmul  27112  dvdsmulf1o  27113  fsumdvdsmulOLD  27114  addsf  27896  xrofsup  32697  txpconn  35226  cvmlift2lem1  35296  cvmlift2lem12  35308  mclsax  35563  ismtyhmeolem  37805  dih1dimatlem  41330  ffnaov  47204  ovn0ssdmfun  48151  plusfreseq  48156  funcf2lem  49074  imaidfu  49103  imasubc  49144  imassc  49146  fucofulem2  49304