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

Theorem r2al 2845
Description: Double restricted universal quantification. (Contributed by NM, 19-Nov-1995.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 9-Jan-2020.)
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 19.21v 1930 . 2  |-  ( A. y ( x  e.  A  ->  ( y  e.  B  ->  ph )
)  <->  ( x  e.  A  ->  A. y
( y  e.  B  ->  ph ) ) )
21r2allem 2842 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 1377    e. wcel 1767   A.wral 2817
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-ral 2822
This theorem is referenced by:  r3al  2847  r3alOLD  2905  r2ex  2990  soss  4824  raliunxp  5148  codir  5393  qfto  5394  fununi  5660  dff13  6165  mpt22eqb  6406  tz7.48lem  7118  qliftfun  7408  zorn2lem4  8891  isirred2  17222  cnmpt12  20036  cnmpt22  20043  dchrelbas3  23379  cvmlift2lem12  28584  dfso2  29110  dfpo2  29111  isdomn3  31093
  Copyright terms: Public domain W3C validator