Theorem ensym 9017

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

Syntax hints:   → wi 4   class class class wbr 5119   ≈ cen 8956

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 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7729

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-er 8719  df-en 8960

This theorem is referenced by:  ensymi  9018  ensymd  9019  sbthb  9108  domnsym  9113  sdomdomtr  9124  domsdomtr  9126  enen1  9131  enen2  9132  domen1  9133  domen2  9134  sdomen1  9135  sdomen2  9136  domtriord  9137  xpen  9154  pwen  9164  php2OLD  9232  php3OLD  9233  phpeqdOLD  9234  ominfOLD  9267  fineqvlem  9270  en1eqsnOLD  9281  dif1ennnALT  9283  enp1iOLD  9286  findcard3OLD  9291  isfinite2  9306  nnsdomgOLD  9308  domunfican  9333  infcntss  9334  fiintOLD  9339  wdomen1  9590  wdomen2  9591  unxpwdom2  9602  karden  9909  finnum  9962  carden2b  9981  fidomtri2  10008  cardmin2  10013  pr2neOLD  10019  en2eleq  10022  infxpenlem  10027  acnen  10067  acnen2  10069  infpwfien  10076  alephordi  10088  alephinit  10109  dfac12lem2  10159  dfac12r  10161  undjudom  10182  djucomen  10192  djuinf  10203  pwsdompw  10217  infmap2  10231  ackbij1b  10252  cflim2  10277  fin4en1  10323  domfin4  10325  fin23lem25  10338  fin23lem23  10340  enfin1ai  10398  fin67  10409  isfin7-2  10410  fin1a2lem11  10424  axcc2lem  10450  axcclem  10471  numthcor  10508  carden  10565  sdomsdomcard  10574  canthnum  10663  canthwe  10665  canthp1lem2  10667  canthp1  10668  pwxpndom2  10679  gchdjuidm  10682  gchxpidm  10683  gchpwdom  10684  inawinalem  10703  grudomon  10831  isfinite4  14380  hashfn  14393  ramub2  17034  dfod2  19545  sylow2blem1  19601  znhash  21519  hauspwdom  23439  rectbntr0  24772  ovolctb  25443  dyadmbl  25553  eupthfi  30186  derangen  35194  finminlem  36336  domalom  37422  phpreu  37628  pellexlem4  42855  pellexlem5  42856  pellex  42858