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  1984  sbnf2  2071  sbcom2  2077  sbal2  2104  2mo  2196  2eu4  2201  ralcomf  2673  unissb  3831  dfiin2g  3910  dftr5  4090  cotr  5043  cnvsym  5045  dffun2  5204  fun11  5253  aceq1  7712  isch2  21763  dfon2lem8  23515  dford4  26489  hbexg  27375  hbexgVD  27732
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