Theorem ensym 8744

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

Syntax hints:   → wi 4   class class class wbr 5070   ≈ cen 8688

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-er 8456  df-en 8692

This theorem is referenced by:  ensymi  8745  ensymd  8746  sbthb  8834  domnsym  8839  sdomdomtr  8846  domsdomtr  8848  enen1  8853  enen2  8854  domen1  8855  domen2  8856  sdomen1  8857  sdomen2  8858  domtriord  8859  xpen  8876  pwen  8886  nneneq  8896  php2  8898  php3  8899  phpeqd  8902  ominf  8964  fineqvlem  8966  en1eqsn  8977  dif1enALT  8980  enp1i  8982  findcard3  8987  isfinite2  9002  nnsdomg  9003  domunfican  9017  infcntss  9018  fiint  9021  wdomen1  9265  wdomen2  9266  unxpwdom2  9277  karden  9584  finnum  9637  carden2b  9656  fidomtri2  9683  cardmin2  9688  pr2ne  9692  en2eleq  9695  infxpenlem  9700  acnen  9740  acnen2  9742  infpwfien  9749  alephordi  9761  alephinit  9782  dfac12lem2  9831  dfac12r  9833  undjudom  9854  djucomen  9864  djuinf  9875  pwsdompw  9891  infmap2  9905  ackbij1b  9926  cflim2  9950  fin4en1  9996  domfin4  9998  fin23lem25  10011  fin23lem23  10013  enfin1ai  10071  fin67  10082  isfin7-2  10083  fin1a2lem11  10097  axcc2lem  10123  axcclem  10144  numthcor  10181  carden  10238  sdomsdomcard  10247  canthnum  10336  canthwe  10338  canthp1lem2  10340  canthp1  10341  pwxpndom2  10352  gchdjuidm  10355  gchxpidm  10356  gchpwdom  10357  inawinalem  10376  grudomon  10504  isfinite4  14005  hashfn  14018  ramub2  16643  dfod2  19086  sylow2blem1  19140  znhash  20678  hauspwdom  22560  rectbntr0  23901  ovolctb  24559  dyadmbl  24669  eupthfi  28470  derangen  33034  finminlem  34434  domalom  35502  phpreu  35688  pellexlem4  40570  pellexlem5  40571  pellex  40573