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

Theorem ralxp 5296
 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 5209 . . 3 𝑦𝐴 ({𝑦} × 𝐵) = (𝐴 × 𝐵)
21raleqi 3172 . 2 (∀𝑥 𝑦𝐴 ({𝑦} × 𝐵)𝜑 ↔ ∀𝑥 ∈ (𝐴 × 𝐵)𝜑)
3 ralxp.1 . . 3 (𝑥 = ⟨𝑦, 𝑧⟩ → (𝜑𝜓))
43raliunxp 5294 . 2 (∀𝑥 𝑦𝐴 ({𝑦} × 𝐵)𝜑 ↔ ∀𝑦𝐴𝑧𝐵 𝜓)
52, 4bitr3i 266 1 (∀𝑥 ∈ (𝐴 × 𝐵)𝜑 ↔ ∀𝑦𝐴𝑧𝐵 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   = wceq 1523  ∀wral 2941  {csn 4210  ⟨cop 4216  ∪ ciun 4552   × cxp 5141 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-iun 4554  df-opab 4746  df-xp 5149  df-rel 5150 This theorem is referenced by:  ralxpf  5301  issref  5544  ffnov  6806  eqfnov  6808  funimassov  6853  f1stres  7234  f2ndres  7235  ecopover  7894  xpf1o  8163  xpwdomg  8531  rankxplim  8780  imasaddfnlem  16235  imasvscafn  16244  comfeq  16413  isssc  16527  isfuncd  16572  cofucl  16595  funcres2b  16604  evlfcl  16909  uncfcurf  16926  yonedalem3  16967  yonedainv  16968  efgval2  18183  srgfcl  18561  txbas  21418  hausdiag  21496  tx1stc  21501  txkgen  21503  xkococn  21511  cnmpt21  21522  xkoinjcn  21538  tmdcn2  21940  clssubg  21959  qustgplem  21971  txmetcnp  22399  txmetcn  22400  qtopbaslem  22609  bndth  22804  cxpcn3  24534  dvdsmulf1o  24965  fsumdvdsmul  24966  xrofsup  29661  txpconn  31340  cvmlift2lem1  31410  cvmlift2lem12  31422  mclsax  31592  f1opr  33649  ismtyhmeolem  33733  dih1dimatlem  36935  ffnaov  41600  ovn0ssdmfun  42092  plusfreseq  42097
 Copyright terms: Public domain W3C validator