Theorem ensym 8988

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

Syntax hints:   → wi 4   class class class wbr 5104   ≈ cen 8928

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5250  ax-pow 5326  ax-pr 5394  ax-un 7722

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5105  df-opab 5167  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 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-er 8682  df-en 8932

This theorem is referenced by:  ensymi  8989  ensymd  8990  sbthb  9074  domnsym  9079  sdomdomtr  9086  domsdomtr  9088  enen1  9093  enen2  9094  domen1  9095  domen2  9096  sdomen1  9097  sdomen2  9098  domtriord  9099  xpen  9116  pwen  9126  fineqvlem  9214  dif1ennnALT  9225  isfinite2  9246  domunfican  9269  infcntss  9270  wdomen1  9526  wdomen2  9527  unxpwdom2  9538  karden  9869  finnum  9922  carden2b  9941  fidomtri2  9968  cardmin2  9973  en2eleq  9980  infxpenlem  9985  acnen  10025  acnen2  10027  infpwfien  10034  alephordi  10046  alephinit  10067  dfac12lem2  10116  dfac12r  10118  undjudom  10139  djucomen  10149  djuinf  10160  pwsdompw  10174  infmap2  10188  ackbij1b  10209  cflim2  10235  fin4en1  10281  domfin4  10283  fin23lem25  10296  fin23lem23  10298  enfin1ai  10356  fin67  10367  isfin7-2  10368  fin1a2lem11  10382  axcc2lem  10408  axcclem  10429  numthcor  10466  carden  10523  sdomsdomcard  10532  canthnum  10622  canthwe  10624  canthp1lem2  10626  canthp1  10627  pwxpndom2  10638  gchdjuidm  10641  gchxpidm  10642  gchpwdom  10643  inawinalem  10662  grudomon  10790  isfinite4  14386  hashfn  14399  ramub2  17062  dfod2  19622  sylow2blem1  19678  znhash  21665  hauspwdom  23615  rectbntr0  24947  ovolctb  25606  dyadmbl  25716  eupthfi  30461  padct  32971  derangen  35530  finminlem  36686  domalom  37905  phpreu  38110  pellexlem4  43416  pellexlem5  43417  pellex  43419