Theorem ensym 8558

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

Syntax hints:   → wi 4   class class class wbr 5066   ≈ cen 8506

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-er 8289  df-en 8510

This theorem is referenced by:  ensymi  8559  ensymd  8560  sbthb  8638  domnsym  8643  sdomdomtr  8650  domsdomtr  8652  enen1  8657  enen2  8658  domen1  8659  domen2  8660  sdomen1  8661  sdomen2  8662  domtriord  8663  xpen  8680  pwen  8690  nneneq  8700  php2  8702  php3  8703  phpeqd  8706  ominf  8730  fineqvlem  8732  en1eqsn  8748  dif1en  8751  enp1i  8753  findcard3  8761  isfinite2  8776  nnsdomg  8777  domunfican  8791  infcntss  8792  fiint  8795  wdomen1  9040  wdomen2  9041  unxpwdom2  9052  karden  9324  finnum  9377  carden2b  9396  fidomtri2  9423  cardmin2  9427  pr2ne  9431  en2eleq  9434  infxpenlem  9439  acnen  9479  acnen2  9481  infpwfien  9488  alephordi  9500  alephinit  9521  dfac12lem2  9570  dfac12r  9572  undjudom  9593  djucomen  9603  djuinf  9614  pwsdompw  9626  infmap2  9640  ackbij1b  9661  cflim2  9685  fin4en1  9731  domfin4  9733  fin23lem25  9746  fin23lem23  9748  enfin1ai  9806  fin67  9817  isfin7-2  9818  fin1a2lem11  9832  axcc2lem  9858  axcclem  9879  numthcor  9916  carden  9973  sdomsdomcard  9982  canthnum  10071  canthwe  10073  canthp1lem2  10075  canthp1  10076  pwxpndom2  10087  gchdjuidm  10090  gchxpidm  10091  gchpwdom  10092  inawinalem  10111  grudomon  10239  isfinite4  13724  hashfn  13737  ramub2  16350  dfod2  18691  sylow2blem1  18745  znhash  20705  hauspwdom  22109  rectbntr0  23440  ovolctb  24091  dyadmbl  24201  eupthfi  27984  derangen  32419  finminlem  33666  domalom  34688  phpreu  34891  pellexlem4  39449  pellexlem5  39450  pellex  39452