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

Theorem ralxp 5417
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 5330 . . 3 𝑦𝐴 ({𝑦} × 𝐵) = (𝐴 × 𝐵)
21raleqi 3279 . 2 (∀𝑥 𝑦𝐴 ({𝑦} × 𝐵)𝜑 ↔ ∀𝑥 ∈ (𝐴 × 𝐵)𝜑)
3 ralxp.1 . . 3 (𝑥 = ⟨𝑦, 𝑧⟩ → (𝜑𝜓))
43raliunxp 5415 . 2 (∀𝑥 𝑦𝐴 ({𝑦} × 𝐵)𝜑 ↔ ∀𝑦𝐴𝑧𝐵 𝜓)
52, 4bitr3i 266 1 (∀𝑥 ∈ (𝐴 × 𝐵)𝜑 ↔ ∀𝑦𝐴𝑧𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1630  wral 3048  {csn 4319  cop 4325   ciun 4670   × cxp 5262
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-sep 4931  ax-nul 4939  ax-pr 5053
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ral 3053  df-rex 3054  df-rab 3057  df-v 3340  df-sbc 3575  df-csb 3673  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-nul 4057  df-if 4229  df-sn 4320  df-pr 4322  df-op 4326  df-iun 4672  df-opab 4863  df-xp 5270  df-rel 5271
This theorem is referenced by:  ralxpf  5422  issref  5665  ffnov  6927  eqfnov  6929  funimassov  6974  f1stres  7355  f2ndres  7356  ecopover  8016  xpf1o  8285  xpwdomg  8653  rankxplim  8913  imasaddfnlem  16388  imasvscafn  16397  comfeq  16565  isssc  16679  isfuncd  16724  cofucl  16747  funcres2b  16756  evlfcl  17061  uncfcurf  17078  yonedalem3  17119  yonedainv  17120  efgval2  18335  srgfcl  18713  txbas  21570  hausdiag  21648  tx1stc  21653  txkgen  21655  xkococn  21663  cnmpt21  21674  xkoinjcn  21690  tmdcn2  22092  clssubg  22111  qustgplem  22123  txmetcnp  22551  txmetcn  22552  qtopbaslem  22761  bndth  22956  cxpcn3  24686  dvdsmulf1o  25117  fsumdvdsmul  25118  xrofsup  29840  txpconn  31519  cvmlift2lem1  31589  cvmlift2lem12  31601  mclsax  31771  f1opr  33830  ismtyhmeolem  33914  dih1dimatlem  37118  ffnaov  41783  ovn0ssdmfun  42275  plusfreseq  42280
  Copyright terms: Public domain W3C validator