Theorem ensym 8977

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

Syntax hints:   → wi 4   class class class wbr 5110   ≈ cen 8918

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-er 8674  df-en 8922

This theorem is referenced by:  ensymi  8978  ensymd  8979  sbthb  9068  domnsym  9073  sdomdomtr  9080  domsdomtr  9082  enen1  9087  enen2  9088  domen1  9089  domen2  9090  sdomen1  9091  sdomen2  9092  domtriord  9093  xpen  9110  pwen  9120  ominfOLD  9213  fineqvlem  9216  en1eqsnOLD  9227  dif1ennnALT  9229  enp1iOLD  9232  findcard3OLD  9237  isfinite2  9252  nnsdomgOLD  9254  domunfican  9279  infcntss  9280  fiintOLD  9285  wdomen1  9536  wdomen2  9537  unxpwdom2  9548  karden  9855  finnum  9908  carden2b  9927  fidomtri2  9954  cardmin2  9959  pr2neOLD  9965  en2eleq  9968  infxpenlem  9973  acnen  10013  acnen2  10015  infpwfien  10022  alephordi  10034  alephinit  10055  dfac12lem2  10105  dfac12r  10107  undjudom  10128  djucomen  10138  djuinf  10149  pwsdompw  10163  infmap2  10177  ackbij1b  10198  cflim2  10223  fin4en1  10269  domfin4  10271  fin23lem25  10284  fin23lem23  10286  enfin1ai  10344  fin67  10355  isfin7-2  10356  fin1a2lem11  10370  axcc2lem  10396  axcclem  10417  numthcor  10454  carden  10511  sdomsdomcard  10520  canthnum  10609  canthwe  10611  canthp1lem2  10613  canthp1  10614  pwxpndom2  10625  gchdjuidm  10628  gchxpidm  10629  gchpwdom  10630  inawinalem  10649  grudomon  10777  isfinite4  14334  hashfn  14347  ramub2  16992  dfod2  19501  sylow2blem1  19557  znhash  21475  hauspwdom  23395  rectbntr0  24728  ovolctb  25398  dyadmbl  25508  eupthfi  30141  derangen  35166  finminlem  36313  domalom  37399  phpreu  37605  pellexlem4  42827  pellexlem5  42828  pellex  42830