Theorem ensym 9014

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

This proof depends on syntax axioms:   → wi 4   class class class wbr 5103   ≈ cen 8954

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-pow 5327  ax-pr 5391  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-er 8701  df-en 8958

This theorem is used by:  ensymi  9015  ensymd  9016  sbthb  9101  domnsym  9106  sdomdomtr  9113  domsdomtr  9115  enen1  9120  enen2  9121  domen1  9122  domen2  9123  sdomen1  9124  sdomen2  9125  domtriord  9126  xpen  9143  pwen  9153  fineqvlem  9241  dif1ennnALT  9252  isfinite2  9274  domunfican  9297  infcntss  9298  wdomen1  9554  wdomen2  9555  unxpwdom2  9566  kardenOLD  9941  finnum  10010  carden2b  10029  fidomtri2  10056  cardmin2  10061  en2eleq  10068  infxpenlem  10073  acnen  10113  acnen2  10115  infpwfien  10122  alephordi  10134  alephinit  10155  dfac12lem2  10204  dfac12r  10206  undjudom  10227  djucomen  10237  djuinf  10248  pwsdompw  10262  infmap2  10276  ackbij1b  10297  cflim2  10322  fin4en1  10368  domfin4  10370  fin23lem25  10383  fin23lem23  10385  enfin1ai  10443  fin67  10454  isfin7-2  10455  fin1a2lem11  10469  axcc2lem  10495  axcclem  10516  numthcor  10553  carden  10616  sdomsdomcard  10625  canthnum  10715  canthwe  10717  canthp1lem2  10719  canthp1  10720  pwxpndom2  10731  gchdjuidm  10734  gchxpidm  10735  gchpwdom  10736  inawinalem  10755  grudomon  10883  isfinite4  14486  hashfn  14499  ramub2  17172  dfod2  19758  sylow2blem1  19814  znhash  21844  hauspwdom  23800  rectbntr0  25132  ovolctb  25791  dyadmbl  25901  eupthfi  30788  padct  33292  karddom  35802  kardsdom  35803  kardexen  35804  derangen  35906  finminlem  37076  domalom  38295  phpreu  38495  pellexlem4  43792  pellexlem5  43793  pellex  43795