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

Theorem alcom 2148
Description: Theorem 19.5 of [Margaris] p. 89. Use its weak version alcomw 2039 when it allows to avoid dependence on ax-11 2146. (Contributed by NM, 30-Jun-1993.)
Assertion
Ref Expression
alcom (∀𝑥𝑦𝜑 ↔ ∀𝑦𝑥𝜑)

Proof of Theorem alcom
StepHypRef Expression
1 ax-11 2146 . 2 (∀𝑥𝑦𝜑 → ∀𝑦𝑥𝜑)
2 ax-11 2146 . 2 (∀𝑦𝑥𝜑 → ∀𝑥𝑦𝜑)
31, 2impbii 208 1 (∀𝑥𝑦𝜑 ↔ ∀𝑦𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wal 1531
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-11 2146
This theorem depends on definitions:  df-bi 206
This theorem is referenced by:  alrot3  2149  excom  2151  sbal  2158  sbcom2  2162  nfa2  2165  aaan  2321  sb8v  2342  sb8f  2343  sbnf2  2348  sbal1  2521  sbal2  2522  2mo2  2635  ralcom4  3273  ralcom4OLD  3274  ralcom  3276  nfra2wOLD  3287  ralcomf  3289  moelOLD  3388  unissbOLD  4944  dfiin2g  5036  dftr5OLD  5271  cotrgOLD  6115  cotrgOLDOLD  6116  cnvsymOLD  6120  cnvsymOLDOLD  6121  dffun2OLD  6560  dffun2OLDOLD  6561  fun11  6628  aceq1  10142  isch2  31105  dfon2lem8  35517  bj-hbaeb  36427  wl-sb9v  37147  wl-sbcom2d  37159  wl-sbalnae  37160  wl-2spsbbi  37163  cocossss  38038  cossssid3  38071  trcoss2  38086  dford4  42592  unielss  42788  elmapintrab  43148  undmrnresiss  43176  cnvssco  43178  elintima  43225  relexp0eq  43273  dfhe3  43347  dffrege115  43550  hbexg  44137  hbexgVD  44487  dfich2  46935  ichcom  46936
  Copyright terms: Public domain W3C validator