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

Theorem alcom 1712
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 1709 . 2  |-  ( A. x A. y ph  ->  A. y A. x ph )
2 ax-7 1709 . 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 1528
This theorem is referenced by:  alrot3  1713  sbcom  2028  sbnf2  2047  sbcom2  2056  sbal2  2076  2mo  2222  2eu4  2227  ralcomf  2699  unissb  3858  dfiin2g  3937  dftr5  4117  cotr  5054  cnvsym  5056  dffun2  5231  fun11  5280  aceq1  7739  isch2  21795  dfon2lem8  23547  dford4  26521  hbexg  27593  hbexgVD  27950
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-7 1709
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator