MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ralxp Structured version   Visualization version   GIF version

Theorem ralxp 5802
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
StepHypRef Expression
1 iunxpconst 5709 . . 3 𝑦𝐴 ({𝑦} × 𝐵) = (𝐴 × 𝐵)
21raleqi 3314 . 2 (∀𝑥 𝑦𝐴 ({𝑦} × 𝐵)𝜑 ↔ ∀𝑥 ∈ (𝐴 × 𝐵)𝜑)
3 ralxp.1 . . 3 (𝑥 = ⟨𝑦, 𝑧⟩ → (𝜑𝜓))
43raliunxp 5800 . 2 (∀𝑥 𝑦𝐴 ({𝑦} × 𝐵)𝜑 ↔ ∀𝑦𝐴𝑧𝐵 𝜓)
52, 4bitr3i 277 1 (∀𝑥 ∈ (𝐴 × 𝐵)𝜑 ↔ ∀𝑦𝐴𝑧𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1542  wral 3065  {csn 4591  cop 4597   ciun 4959   × cxp 5636
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 2708  ax-sep 5261  ax-nul 5268  ax-pr 5389
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ral 3066  df-rex 3075  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-iun 4961  df-opab 5173  df-xp 5644  df-rel 5645
This theorem is referenced by:  ralxpf  5807  reu3op  6249  f1opr  7418  ffnov  7488  eqfnov  7490  funimassov  7536  f1stres  7950  f2ndres  7951  naddf  8632  ecopover  8767  xpf1o  9090  xpwdomg  9528  rankxplim  9822  imasaddfnlem  17417  imasvscafn  17426  comfeq  17593  isssc  17710  isfuncd  17758  cofucl  17781  funcres2b  17790  evlfcl  18118  uncfcurf  18135  yonedalem3  18176  yonedainv  18177  efgval2  19513  srgfcl  19934  txbas  22934  hausdiag  23012  tx1stc  23017  txkgen  23019  xkococn  23027  cnmpt21  23038  xkoinjcn  23054  tmdcn2  23456  clssubg  23476  qustgplem  23488  txmetcnp  23919  txmetcn  23920  qtopbaslem  24138  bndth  24337  cxpcn3  26117  dvdsmulf1o  26559  fsumdvdsmul  26560  addsf  27314  xrofsup  31714  txpconn  33866  cvmlift2lem1  33936  cvmlift2lem12  33948  mclsax  34203  ismtyhmeolem  36292  dih1dimatlem  39821  ffnaov  45505  ovn0ssdmfun  46135  plusfreseq  46140  funcf2lem  47112
  Copyright terms: Public domain W3C validator