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

Theorem alcom 1748
Description: Theorem 19.5 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
alcom  |-  ( A. x A. y ph  <->  A. y A. x ph )

Proof of Theorem alcom
StepHypRef Expression
1 ax-7 1745 . 2  |-  ( A. x A. y ph  ->  A. y A. x ph )
2 ax-7 1745 . 2  |-  ( A. y A. x ph  ->  A. x A. y ph )
31, 2impbii 181 1  |-  ( A. x A. y ph  <->  A. y A. x ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 177   A.wal 1546
This theorem is referenced by:  alrot3  1749  excom  1752  sbcom  2138  sbnf2  2157  sbcom2  2163  sbal2  2184  2mo  2332  2eu4  2337  ralcomf  2826  unissb  4005  dfiin2g  4084  dftr5  4265  cotr  5205  cnvsym  5207  dffun2  5423  fun11  5475  aceq1  7954  isch2  22679  dfon2lem8  25360  dford4  26990  hbexg  28354  hbexgVD  28727
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-7 1745
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator