Theorem ensym 8919

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

Syntax hints:   → wi 4   class class class wbr 5088   ≈ cen 8860

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 2701  ax-sep 5231  ax-nul 5241  ax-pow 5300  ax-pr 5367  ax-un 7662

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3393  df-v 3435  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5089  df-opab 5151  df-id 5508  df-xp 5619  df-rel 5620  df-cnv 5621  df-co 5622  df-dm 5623  df-rn 5624  df-res 5625  df-ima 5626  df-fun 6478  df-fn 6479  df-f 6480  df-f1 6481  df-fo 6482  df-f1o 6483  df-er 8616  df-en 8864

This theorem is referenced by:  ensymi  8920  ensymd  8921  sbthb  9005  domnsym  9010  sdomdomtr  9017  domsdomtr  9019  enen1  9024  enen2  9025  domen1  9026  domen2  9027  sdomen1  9028  sdomen2  9029  domtriord  9030  xpen  9047  pwen  9057  fineqvlem  9144  dif1ennnALT  9155  isfinite2  9176  domunfican  9200  infcntss  9201  wdomen1  9456  wdomen2  9457  unxpwdom2  9468  karden  9779  finnum  9832  carden2b  9851  fidomtri2  9878  cardmin2  9883  en2eleq  9890  infxpenlem  9895  acnen  9935  acnen2  9937  infpwfien  9944  alephordi  9956  alephinit  9977  dfac12lem2  10027  dfac12r  10029  undjudom  10050  djucomen  10060  djuinf  10071  pwsdompw  10085  infmap2  10099  ackbij1b  10120  cflim2  10145  fin4en1  10191  domfin4  10193  fin23lem25  10206  fin23lem23  10208  enfin1ai  10266  fin67  10277  isfin7-2  10278  fin1a2lem11  10292  axcc2lem  10318  axcclem  10339  numthcor  10376  carden  10433  sdomsdomcard  10442  canthnum  10531  canthwe  10533  canthp1lem2  10535  canthp1  10536  pwxpndom2  10547  gchdjuidm  10550  gchxpidm  10551  gchpwdom  10552  inawinalem  10571  grudomon  10699  isfinite4  14257  hashfn  14270  ramub2  16913  dfod2  19430  sylow2blem1  19486  znhash  21449  hauspwdom  23370  rectbntr0  24702  ovolctb  25372  dyadmbl  25482  eupthfi  30136  derangen  35162  finminlem  36309  domalom  37395  phpreu  37601  pellexlem4  42822  pellexlem5  42823  pellex  42825