Theorem ensym 9042

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	⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴)

Proof of Theorem ensym

Step	Hyp	Ref	Expression
1		ensymb 9041	. 2 ⊢ (𝐴 ≈ 𝐵 ↔ 𝐵 ≈ 𝐴)
2	1	biimpi 216	1 ⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴)

Syntax hints:   → wi 4   class class class wbr 5148   ≈ cen 8981

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-er 8744  df-en 8985

This theorem is referenced by:  ensymi  9043  ensymd  9044  sbthb  9133  domnsym  9138  sdomdomtr  9149  domsdomtr  9151  enen1  9156  enen2  9157  domen1  9158  domen2  9159  sdomen1  9160  sdomen2  9161  domtriord  9162  xpen  9179  pwen  9189  nneneqOLD  9256  php2OLD  9258  php3OLD  9259  phpeqdOLD  9260  ominfOLD  9293  fineqvlem  9296  en1eqsnOLD  9307  dif1ennnALT  9309  enp1iOLD  9312  findcard3OLD  9317  isfinite2  9332  nnsdomgOLD  9334  domunfican  9359  infcntss  9360  fiintOLD  9365  wdomen1  9614  wdomen2  9615  unxpwdom2  9626  karden  9933  finnum  9986  carden2b  10005  fidomtri2  10032  cardmin2  10037  pr2neOLD  10043  en2eleq  10046  infxpenlem  10051  acnen  10091  acnen2  10093  infpwfien  10100  alephordi  10112  alephinit  10133  dfac12lem2  10183  dfac12r  10185  undjudom  10206  djucomen  10216  djuinf  10227  pwsdompw  10241  infmap2  10255  ackbij1b  10276  cflim2  10301  fin4en1  10347  domfin4  10349  fin23lem25  10362  fin23lem23  10364  enfin1ai  10422  fin67  10433  isfin7-2  10434  fin1a2lem11  10448  axcc2lem  10474  axcclem  10495  numthcor  10532  carden  10589  sdomsdomcard  10598  canthnum  10687  canthwe  10689  canthp1lem2  10691  canthp1  10692  pwxpndom2  10703  gchdjuidm  10706  gchxpidm  10707  gchpwdom  10708  inawinalem  10727  grudomon  10855  isfinite4  14398  hashfn  14411  ramub2  17048  dfod2  19597  sylow2blem1  19653  znhash  21595  hauspwdom  23525  rectbntr0  24868  ovolctb  25539  dyadmbl  25649  eupthfi  30234  derangen  35157  finminlem  36301  domalom  37387  phpreu  37591  pellexlem4  42820  pellexlem5  42821  pellex  42823