Theorem ralxp 5818

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ∀wral 3077  {csn 4584  ⟨cop 4590  ∪ ciun 4951   × cxp 5649

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-iun 4953  df-opab 5168  df-xp 5657  df-rel 5658

This theorem is used by:  ralxpf  5824  reu3op  6288  f1opr  7468  ffnov  7538  eqfnov  7541  ovn0ssdmfun  7581  funimassov  7590  f1stres  8014  f2ndres  8015  naddf  8675  ecopover  8826  xpf1o  9142  xpwdomg  9563  rankxplim  9877  imasaddfnlem  17680  imasvscafn  17689  comfeq  17860  isssc  17975  isfuncd  18020  cofucl  18043  funcres2b  18052  evlfcl  18376  uncfcurf  18393  yonedalem3  18434  yonedainv  18435  efgval2  19918  srgfcl  20402  txbas  23866  hausdiag  23944  tx1stc  23949  txkgen  23951  xkococn  23959  cnmpt21  23970  xkoinjcn  23986  tmdcn2  24388  clssubg  24408  qustgplem  24420  txmetcnp  24846  txmetcn  24847  qtopbaslem  25057  bndth  25259  cxpcn3  27058  mpodvdsmulf1o  27503  fsumdvdsmul  27504  dvdsmulf1o  27505  addsf  28350  xrofsup  33341  txpconn  35966  cvmlift2lem1  36036  cvmlift2lem12  36048  mclsax  36303  ismtyhmeolem  38706  dih1dimatlem  42354  ffnaov  48213  plusfreseq  49205  funcf2lem  50133  imaidfu  50162  imasubc  50203  imassc  50205  fucofulem2  50363