Theorem ensym 8947

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

Syntax hints:   → wi 4   class class class wbr 5079   ≈ cen 8887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-pow 5301  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-er 8640  df-en 8891

This theorem is referenced by:  ensymi  8948  ensymd  8949  sbthb  9033  domnsym  9038  sdomdomtr  9045  domsdomtr  9047  enen1  9052  enen2  9053  domen1  9054  domen2  9055  sdomen1  9056  sdomen2  9057  domtriord  9058  xpen  9075  pwen  9085  fineqvlem  9173  dif1ennnALT  9184  isfinite2  9205  domunfican  9229  infcntss  9230  wdomen1  9488  wdomen2  9489  unxpwdom2  9500  karden  9817  finnum  9870  carden2b  9889  fidomtri2  9916  cardmin2  9921  en2eleq  9928  infxpenlem  9933  acnen  9973  acnen2  9975  infpwfien  9982  alephordi  9994  alephinit  10015  dfac12lem2  10065  dfac12r  10067  undjudom  10088  djucomen  10098  djuinf  10109  pwsdompw  10123  infmap2  10137  ackbij1b  10158  cflim2  10183  fin4en1  10229  domfin4  10231  fin23lem25  10244  fin23lem23  10246  enfin1ai  10304  fin67  10315  isfin7-2  10316  fin1a2lem11  10330  axcc2lem  10356  axcclem  10377  numthcor  10414  carden  10471  sdomsdomcard  10480  canthnum  10570  canthwe  10572  canthp1lem2  10574  canthp1  10575  pwxpndom2  10586  gchdjuidm  10589  gchxpidm  10590  gchpwdom  10591  inawinalem  10610  grudomon  10738  isfinite4  14322  hashfn  14335  ramub2  16983  dfod2  19537  sylow2blem1  19593  znhash  21540  hauspwdom  23491  rectbntr0  24823  ovolctb  25482  dyadmbl  25592  eupthfi  30300  padct  32817  derangen  35407  finminlem  36553  domalom  37773  phpreu  37978  pellexlem4  43284  pellexlem5  43285  pellex  43287