Theorem ensym 8980

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

Syntax hints:   → wi 4   class class class wbr 5099   ≈ cen 8920

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-pow 5321  ax-pr 5389  ax-un 7714

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-id 5540  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-res 5657  df-ima 5658  df-fun 6519  df-fn 6520  df-f 6521  df-f1 6522  df-fo 6523  df-f1o 6524  df-er 8673  df-en 8924

This theorem is referenced by:  ensymi  8981  ensymd  8982  sbthb  9066  domnsym  9071  sdomdomtr  9078  domsdomtr  9080  enen1  9085  enen2  9086  domen1  9087  domen2  9088  sdomen1  9089  sdomen2  9090  domtriord  9091  xpen  9108  pwen  9118  fineqvlem  9206  dif1ennnALT  9217  isfinite2  9238  domunfican  9262  infcntss  9263  wdomen1  9521  wdomen2  9522  unxpwdom2  9533  karden  9850  finnum  9903  carden2b  9922  fidomtri2  9949  cardmin2  9954  en2eleq  9961  infxpenlem  9966  acnen  10006  acnen2  10008  infpwfien  10015  alephordi  10027  alephinit  10048  dfac12lem2  10098  dfac12r  10100  undjudom  10121  djucomen  10131  djuinf  10142  pwsdompw  10156  infmap2  10170  ackbij1b  10191  cflim2  10217  fin4en1  10263  domfin4  10265  fin23lem25  10278  fin23lem23  10280  enfin1ai  10338  fin67  10349  isfin7-2  10350  fin1a2lem11  10364  axcc2lem  10390  axcclem  10411  numthcor  10448  carden  10505  sdomsdomcard  10514  canthnum  10604  canthwe  10606  canthp1lem2  10608  canthp1  10609  pwxpndom2  10620  gchdjuidm  10623  gchxpidm  10624  gchpwdom  10625  inawinalem  10644  grudomon  10772  isfinite4  14372  hashfn  14385  ramub2  17033  dfod2  19587  sylow2blem1  19643  znhash  21590  hauspwdom  23541  rectbntr0  24873  ovolctb  25532  dyadmbl  25642  eupthfi  30353  padct  32870  derangen  35486  finminlem  36642  domalom  37862  phpreu  38067  pellexlem4  43373  pellexlem5  43374  pellex  43376