Theorem ensym 9043

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 9042	. 2 ⊢ (𝐴 ≈ 𝐵 ↔ 𝐵 ≈ 𝐴)
2	1	biimpi 216	1 ⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴)

Syntax hints:   → wi 4   class class class wbr 5143   ≈ cen 8982

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-er 8745  df-en 8986

This theorem is referenced by:  ensymi  9044  ensymd  9045  sbthb  9134  domnsym  9139  sdomdomtr  9150  domsdomtr  9152  enen1  9157  enen2  9158  domen1  9159  domen2  9160  sdomen1  9161  sdomen2  9162  domtriord  9163  xpen  9180  pwen  9190  nneneqOLD  9258  php2OLD  9260  php3OLD  9261  phpeqdOLD  9262  ominfOLD  9295  fineqvlem  9298  en1eqsnOLD  9309  dif1ennnALT  9311  enp1iOLD  9314  findcard3OLD  9319  isfinite2  9334  nnsdomgOLD  9336  domunfican  9361  infcntss  9362  fiintOLD  9367  wdomen1  9616  wdomen2  9617  unxpwdom2  9628  karden  9935  finnum  9988  carden2b  10007  fidomtri2  10034  cardmin2  10039  pr2neOLD  10045  en2eleq  10048  infxpenlem  10053  acnen  10093  acnen2  10095  infpwfien  10102  alephordi  10114  alephinit  10135  dfac12lem2  10185  dfac12r  10187  undjudom  10208  djucomen  10218  djuinf  10229  pwsdompw  10243  infmap2  10257  ackbij1b  10278  cflim2  10303  fin4en1  10349  domfin4  10351  fin23lem25  10364  fin23lem23  10366  enfin1ai  10424  fin67  10435  isfin7-2  10436  fin1a2lem11  10450  axcc2lem  10476  axcclem  10497  numthcor  10534  carden  10591  sdomsdomcard  10600  canthnum  10689  canthwe  10691  canthp1lem2  10693  canthp1  10694  pwxpndom2  10705  gchdjuidm  10708  gchxpidm  10709  gchpwdom  10710  inawinalem  10729  grudomon  10857  isfinite4  14401  hashfn  14414  ramub2  17052  dfod2  19582  sylow2blem1  19638  znhash  21577  hauspwdom  23509  rectbntr0  24854  ovolctb  25525  dyadmbl  25635  eupthfi  30224  derangen  35177  finminlem  36319  domalom  37405  phpreu  37611  pellexlem4  42843  pellexlem5  42844  pellex  42846