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

Theorem r2al 2679
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 2516 . 2  |-  F/_ y A
21r2alf 2677 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 177    /\ wa 359   A.wal 1546    e. wcel 1717   A.wral 2642
This theorem is referenced by:  r3al  2699  soss  4455  raliunxp  4947  codir  5187  qfto  5188  fununi  5450  dff13  5936  mpt22eqb  6111  tz7.48lem  6627  qliftfun  6918  zorn2lem4  8305  isirred2  15726  cnmpt12  17613  cnmpt22  17620  dchrelbas3  20882  cvmlift2lem12  24773  dfso2  25128  dfpo2  25129  isdomn3  27185
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-cleq 2373  df-clel 2376  df-nfc 2505  df-ral 2647
  Copyright terms: Public domain W3C validator