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

Theorem r2al 2757
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 2584 . 2  |-  F/_ y A
21r2alf 2755 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 1367    e. wcel 1756   A.wral 2720
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ral 2725
This theorem is referenced by:  r3al  2778  soss  4664  raliunxp  4984  codir  5223  qfto  5224  fununi  5489  dff13  5976  mpt22eqb  6204  tz7.48lem  6901  qliftfun  7190  zorn2lem4  8673  isirred2  16798  cnmpt12  19245  cnmpt22  19252  dchrelbas3  22582  cvmlift2lem12  27208  dfso2  27569  dfpo2  27570  isdomn3  29577
  Copyright terms: Public domain W3C validator