Theorem ensym 8952

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

Syntax hints:   → wi 4   class class class wbr 5100   ≈ cen 8892

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-pow 5312  ax-pr 5379  ax-un 7690

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-er 8645  df-en 8896

This theorem is referenced by:  ensymi  8953  ensymd  8954  sbthb  9038  domnsym  9043  sdomdomtr  9050  domsdomtr  9052  enen1  9057  enen2  9058  domen1  9059  domen2  9060  sdomen1  9061  sdomen2  9062  domtriord  9063  xpen  9080  pwen  9090  fineqvlem  9178  dif1ennnALT  9189  isfinite2  9210  domunfican  9234  infcntss  9235  wdomen1  9493  wdomen2  9494  unxpwdom2  9505  karden  9819  finnum  9872  carden2b  9891  fidomtri2  9918  cardmin2  9923  en2eleq  9930  infxpenlem  9935  acnen  9975  acnen2  9977  infpwfien  9984  alephordi  9996  alephinit  10017  dfac12lem2  10067  dfac12r  10069  undjudom  10090  djucomen  10100  djuinf  10111  pwsdompw  10125  infmap2  10139  ackbij1b  10160  cflim2  10185  fin4en1  10231  domfin4  10233  fin23lem25  10246  fin23lem23  10248  enfin1ai  10306  fin67  10317  isfin7-2  10318  fin1a2lem11  10332  axcc2lem  10358  axcclem  10379  numthcor  10416  carden  10473  sdomsdomcard  10482  canthnum  10572  canthwe  10574  canthp1lem2  10576  canthp1  10577  pwxpndom2  10588  gchdjuidm  10591  gchxpidm  10592  gchpwdom  10593  inawinalem  10612  grudomon  10740  isfinite4  14297  hashfn  14310  ramub2  16954  dfod2  19505  sylow2blem1  19561  znhash  21525  hauspwdom  23457  rectbntr0  24789  ovolctb  25459  dyadmbl  25569  eupthfi  30292  derangen  35385  finminlem  36531  domalom  37653  phpreu  37849  pellexlem4  43183  pellexlem5  43184  pellex  43186