Theorem ensym 8925

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

Syntax hints:   → wi 4   class class class wbr 5091   ≈ cen 8866

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pow 5303  ax-pr 5370  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-id 5511  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-er 8622  df-en 8870

This theorem is referenced by:  ensymi  8926  ensymd  8927  sbthb  9011  domnsym  9016  sdomdomtr  9023  domsdomtr  9025  enen1  9030  enen2  9031  domen1  9032  domen2  9033  sdomen1  9034  sdomen2  9035  domtriord  9036  xpen  9053  pwen  9063  fineqvlem  9150  dif1ennnALT  9161  isfinite2  9182  domunfican  9206  infcntss  9207  wdomen1  9462  wdomen2  9463  unxpwdom2  9474  karden  9785  finnum  9838  carden2b  9857  fidomtri2  9884  cardmin2  9889  en2eleq  9896  infxpenlem  9901  acnen  9941  acnen2  9943  infpwfien  9950  alephordi  9962  alephinit  9983  dfac12lem2  10033  dfac12r  10035  undjudom  10056  djucomen  10066  djuinf  10077  pwsdompw  10091  infmap2  10105  ackbij1b  10126  cflim2  10151  fin4en1  10197  domfin4  10199  fin23lem25  10212  fin23lem23  10214  enfin1ai  10272  fin67  10283  isfin7-2  10284  fin1a2lem11  10298  axcc2lem  10324  axcclem  10345  numthcor  10382  carden  10439  sdomsdomcard  10448  canthnum  10537  canthwe  10539  canthp1lem2  10541  canthp1  10542  pwxpndom2  10553  gchdjuidm  10556  gchxpidm  10557  gchpwdom  10558  inawinalem  10577  grudomon  10705  isfinite4  14266  hashfn  14279  ramub2  16923  dfod2  19474  sylow2blem1  19530  znhash  21493  hauspwdom  23414  rectbntr0  24746  ovolctb  25416  dyadmbl  25526  eupthfi  30180  derangen  35204  finminlem  36351  domalom  37437  phpreu  37643  pellexlem4  42864  pellexlem5  42865  pellex  42867