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

Theorem r2al 2750
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 2577 . 2  |-  F/_ y A
21r2alf 2748 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 setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369   A.wal 1362    e. wcel 1761   A.wral 2713
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1592  df-nf 1595  df-sb 1706  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ral 2718
This theorem is referenced by:  r3al  2771  soss  4655  raliunxp  4975  codir  5215  qfto  5216  fununi  5481  dff13  5968  mpt22eqb  6198  tz7.48lem  6892  qliftfun  7181  zorn2lem4  8664  isirred2  16783  cnmpt12  19199  cnmpt22  19206  dchrelbas3  22536  cvmlift2lem12  27133  dfso2  27493  dfpo2  27494  isdomn3  29497
  Copyright terms: Public domain W3C validator