Theorem ensym 8932

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

Syntax hints:   → wi 4   class class class wbr 5093   ≈ cen 8872

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674

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 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-er 8628  df-en 8876

This theorem is referenced by:  ensymi  8933  ensymd  8934  sbthb  9018  domnsym  9023  sdomdomtr  9030  domsdomtr  9032  enen1  9037  enen2  9038  domen1  9039  domen2  9040  sdomen1  9041  sdomen2  9042  domtriord  9043  xpen  9060  pwen  9070  fineqvlem  9157  dif1ennnALT  9168  isfinite2  9189  domunfican  9213  infcntss  9214  wdomen1  9469  wdomen2  9470  unxpwdom2  9481  karden  9795  finnum  9848  carden2b  9867  fidomtri2  9894  cardmin2  9899  en2eleq  9906  infxpenlem  9911  acnen  9951  acnen2  9953  infpwfien  9960  alephordi  9972  alephinit  9993  dfac12lem2  10043  dfac12r  10045  undjudom  10066  djucomen  10076  djuinf  10087  pwsdompw  10101  infmap2  10115  ackbij1b  10136  cflim2  10161  fin4en1  10207  domfin4  10209  fin23lem25  10222  fin23lem23  10224  enfin1ai  10282  fin67  10293  isfin7-2  10294  fin1a2lem11  10308  axcc2lem  10334  axcclem  10355  numthcor  10392  carden  10449  sdomsdomcard  10458  canthnum  10547  canthwe  10549  canthp1lem2  10551  canthp1  10552  pwxpndom2  10563  gchdjuidm  10566  gchxpidm  10567  gchpwdom  10568  inawinalem  10587  grudomon  10715  isfinite4  14271  hashfn  14284  ramub2  16928  dfod2  19478  sylow2blem1  19534  znhash  21497  hauspwdom  23417  rectbntr0  24749  ovolctb  25419  dyadmbl  25529  eupthfi  30187  derangen  35237  finminlem  36383  domalom  37469  phpreu  37664  pellexlem4  42949  pellexlem5  42950  pellex  42952