Theorem ensym 8943

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

Syntax hints:   → wi 4   class class class wbr 5086   ≈ cen 8883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-pow 5302  ax-pr 5370  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-er 8636  df-en 8887

This theorem is referenced by:  ensymi  8944  ensymd  8945  sbthb  9029  domnsym  9034  sdomdomtr  9041  domsdomtr  9043  enen1  9048  enen2  9049  domen1  9050  domen2  9051  sdomen1  9052  sdomen2  9053  domtriord  9054  xpen  9071  pwen  9081  fineqvlem  9169  dif1ennnALT  9180  isfinite2  9201  domunfican  9225  infcntss  9226  wdomen1  9484  wdomen2  9485  unxpwdom2  9496  karden  9810  finnum  9863  carden2b  9882  fidomtri2  9909  cardmin2  9914  en2eleq  9921  infxpenlem  9926  acnen  9966  acnen2  9968  infpwfien  9975  alephordi  9987  alephinit  10008  dfac12lem2  10058  dfac12r  10060  undjudom  10081  djucomen  10091  djuinf  10102  pwsdompw  10116  infmap2  10130  ackbij1b  10151  cflim2  10176  fin4en1  10222  domfin4  10224  fin23lem25  10237  fin23lem23  10239  enfin1ai  10297  fin67  10308  isfin7-2  10309  fin1a2lem11  10323  axcc2lem  10349  axcclem  10370  numthcor  10407  carden  10464  sdomsdomcard  10473  canthnum  10563  canthwe  10565  canthp1lem2  10567  canthp1  10568  pwxpndom2  10579  gchdjuidm  10582  gchxpidm  10583  gchpwdom  10584  inawinalem  10603  grudomon  10731  isfinite4  14315  hashfn  14328  ramub2  16976  dfod2  19530  sylow2blem1  19586  znhash  21548  hauspwdom  23476  rectbntr0  24808  ovolctb  25467  dyadmbl  25577  eupthfi  30290  padct  32806  derangen  35370  finminlem  36516  domalom  37734  phpreu  37939  pellexlem4  43278  pellexlem5  43279  pellex  43281