MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  r2al Unicode version

Theorem r2al 2593
Description: Double restricted universal quantification. (Contributed by NM, 19-Nov-1995.)
Assertion
Ref Expression
r2al  |-  ( A. x  e.  A  A. y  e.  B  ph  <->  A. x A. y ( ( x  e.  A  /\  y  e.  B )  ->  ph )
)
Distinct variable groups:    x, y    y, A
Allowed substitution hints:    ph( x, y)    A( x)    B( x, y)

Proof of Theorem r2al
StepHypRef Expression
1 nfcv 2432 . 2  |-  F/_ y A
21r2alf 2591 1  |-  ( A. x  e.  A  A. y  e.  B  ph  <->  A. x A. y ( ( x  e.  A  /\  y  e.  B )  ->  ph )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358   A.wal 1530    e. wcel 1696   A.wral 2556
This theorem is referenced by:  r3al  2613  soss  4348  raliunxp  4841  codir  5079  qfto  5080  fununi  5332  dff13  5799  mpt22eqb  5969  tz7.48lem  6469  qliftfun  6759  zorn2lem4  8142  isirred2  15499  cnmpt12  17377  cnmpt22  17384  dchrelbas3  20493  cvmlift2lem12  23860  dfso2  24182  dfpo2  24183  imonclem  25916  ismonc  25917  iepiclem  25926  isepic  25927  isdomn3  27626
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561
  Copyright terms: Public domain W3C validator