Theorem ensym 8974

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

Syntax hints:   → wi 4   class class class wbr 5107   ≈ cen 8915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-er 8671  df-en 8919

This theorem is referenced by:  ensymi  8975  ensymd  8976  sbthb  9062  domnsym  9067  sdomdomtr  9074  domsdomtr  9076  enen1  9081  enen2  9082  domen1  9083  domen2  9084  sdomen1  9085  sdomen2  9086  domtriord  9087  xpen  9104  pwen  9114  ominfOLD  9206  fineqvlem  9209  en1eqsnOLD  9220  dif1ennnALT  9222  enp1iOLD  9225  findcard3OLD  9230  isfinite2  9245  nnsdomgOLD  9247  domunfican  9272  infcntss  9273  fiintOLD  9278  wdomen1  9529  wdomen2  9530  unxpwdom2  9541  karden  9848  finnum  9901  carden2b  9920  fidomtri2  9947  cardmin2  9952  pr2neOLD  9958  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  10216  fin4en1  10262  domfin4  10264  fin23lem25  10277  fin23lem23  10279  enfin1ai  10337  fin67  10348  isfin7-2  10349  fin1a2lem11  10363  axcc2lem  10389  axcclem  10410  numthcor  10447  carden  10504  sdomsdomcard  10513  canthnum  10602  canthwe  10604  canthp1lem2  10606  canthp1  10607  pwxpndom2  10618  gchdjuidm  10621  gchxpidm  10622  gchpwdom  10623  inawinalem  10642  grudomon  10770  isfinite4  14327  hashfn  14340  ramub2  16985  dfod2  19494  sylow2blem1  19550  znhash  21468  hauspwdom  23388  rectbntr0  24721  ovolctb  25391  dyadmbl  25501  eupthfi  30134  derangen  35159  finminlem  36306  domalom  37392  phpreu  37598  pellexlem4  42820  pellexlem5  42821  pellex  42823