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

Theorem r2al 2580
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 2419 . 2  |-  F/_ y A
21r2alf 2578 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 1527    e. wcel 1684   A.wral 2543
This theorem is referenced by:  r3al  2600  soss  4332  raliunxp  4825  codir  5063  qfto  5064  fununi  5316  dff13  5783  mpt22eqb  5953  tz7.48lem  6453  qliftfun  6743  zorn2lem4  8126  isirred2  15483  cnmpt12  17361  cnmpt22  17368  dchrelbas3  20477  cvmlift2lem12  23845  dfso2  24111  dfpo2  24112  imonclem  25813  ismonc  25814  iepiclem  25823  isepic  25824  isdomn3  27523
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548
  Copyright terms: Public domain W3C validator