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 5105   ≈ 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 5251  ax-pow 5327  ax-pr 5395  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 4869  df-br 5106  df-opab 5168  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  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  14389  hashfn  14402  ramub2  17064  dfod2  19625  sylow2blem1  19681  znhash  21668  hauspwdom  23619  rectbntr0  24951  ovolctb  25610  dyadmbl  25720  eupthfi  30465  padct  32975  derangen  35535  finminlem  36691  domalom  37910  phpreu  38115  pellexlem4  43421  pellexlem5  43422  pellex  43424