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

Theorem alcom 1568
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 1535 . 2  |-  ( A. x A. y ph  ->  A. y A. x ph )
2 ax-7 1535 . 2  |-  ( A. y A. x ph  ->  A. x A. y ph )
31, 2impbii 182 1  |-  ( A. x A. y ph  <->  A. y A. x ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 178   A.wal 1532
This theorem is referenced by:  alrot3  1610  sbcom  1983  sbnf2  2068  sbcom2  2074  sbal2  2100  2mo  2191  2eu4  2196  ralcomf  2660  unissb  3755  dfiin2g  3834  dftr5  4013  cotr  4962  cnvsym  4964  dffun2  5123  fun11  5172  aceq1  7628  isch2  21633  dfon2lem8  23314  dford4  26288  hbexg  27112  hbexgVD  27469
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-7 1535
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator