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

Theorem ensym 7554
Description: Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
Assertion
Ref Expression
ensym  |-  ( A 
~~  B  ->  B  ~~  A )

Proof of Theorem ensym
StepHypRef Expression
1 ensymb 7553 . 2  |-  ( A 
~~  B  <->  B  ~~  A )
21biimpi 194 1  |-  ( A 
~~  B  ->  B  ~~  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   class class class wbr 4440    ~~ cen 7503
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pow 4618  ax-pr 4679  ax-un 6567
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-pw 4005  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-opab 4499  df-id 4788  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-rn 5003  df-res 5004  df-ima 5005  df-fun 5581  df-fn 5582  df-f 5583  df-f1 5584  df-fo 5585  df-f1o 5586  df-er 7301  df-en 7507
This theorem is referenced by:  ensymi  7555  ensymd  7556  sbthb  7628  domnsym  7633  sdomdomtr  7640  domsdomtr  7642  enen1  7647  enen2  7648  domen1  7649  domen2  7650  sdomen1  7651  sdomen2  7652  domtriord  7653  xpen  7670  pwen  7680  nneneq  7690  php2  7692  php3  7693  ominf  7722  fineqvlem  7724  en1eqsn  7739  dif1enOLD  7741  dif1en  7742  enp1i  7744  findcard3  7752  isfinite2  7767  nnsdomg  7768  domunfican  7782  infcntss  7783  fiint  7786  wdomen1  7991  wdomen2  7992  unxpwdom2  8003  karden  8302  finnum  8318  carden2b  8337  fidomtri2  8364  cardmin2  8368  pr2ne  8372  en2eleq  8375  infxpenlem  8380  acnen  8423  acnen2  8425  infpwfien  8432  alephordi  8444  alephinit  8465  dfac12lem2  8513  dfac12r  8515  uncdadom  8540  cdacomen  8550  cdainf  8561  pwsdompw  8573  infmap2  8587  ackbij1b  8608  cflim2  8632  fin4en1  8678  domfin4  8680  fin23lem25  8693  fin23lem23  8695  enfin1ai  8753  fin67  8764  isfin7-2  8765  fin1a2lem11  8779  axcc2lem  8805  axcclem  8826  numthcor  8863  carden  8915  sdomsdomcard  8924  canthnum  9016  canthwe  9018  canthp1lem2  9020  canthp1  9021  pwxpndom2  9032  gchcdaidm  9035  gchxpidm  9036  gchpwdom  9037  inawinalem  9056  grudomon  9184  hashfn  12398  isprm2lem  14072  ramub2  14380  dfod2  16375  sylow2blem1  16429  znhash  18357  hauspwdom  19761  rectbntr0  21065  ovolctb  21629  dyadmbl  21737  eupafi  24633  derangen  28242  finminlem  29700  pellexlem4  30359  pellexlem5  30360  pellex  30362
  Copyright terms: Public domain W3C validator