Theorem ensym 9001

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

Syntax hints:   → wi 4   class class class wbr 5110   ≈ cen 8941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-pow 5338  ax-pr 5406  ax-un 7734

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-er 8695  df-en 8945

This theorem is referenced by:  ensymi  9002  ensymd  9003  sbthb  9087  domnsym  9092  sdomdomtr  9099  domsdomtr  9101  enen1  9106  enen2  9107  domen1  9108  domen2  9109  sdomen1  9110  sdomen2  9111  domtriord  9112  xpen  9129  pwen  9139  fineqvlem  9227  dif1ennnALT  9238  isfinite2  9259  domunfican  9282  infcntss  9283  wdomen1  9539  wdomen2  9540  unxpwdom2  9551  karden  9882  finnum  9935  carden2b  9954  fidomtri2  9981  cardmin2  9986  en2eleq  9993  infxpenlem  9998  acnen  10038  acnen2  10040  infpwfien  10047  alephordi  10059  alephinit  10080  dfac12lem2  10129  dfac12r  10131  undjudom  10152  djucomen  10162  djuinf  10173  pwsdompw  10187  infmap2  10201  ackbij1b  10222  cflim2  10248  fin4en1  10294  domfin4  10296  fin23lem25  10309  fin23lem23  10311  enfin1ai  10369  fin67  10380  isfin7-2  10381  fin1a2lem11  10395  axcc2lem  10421  axcclem  10442  numthcor  10479  carden  10536  sdomsdomcard  10545  canthnum  10635  canthwe  10637  canthp1lem2  10639  canthp1  10640  pwxpndom2  10651  gchdjuidm  10654  gchxpidm  10655  gchpwdom  10656  inawinalem  10675  grudomon  10803  isfinite4  14400  hashfn  14413  ramub2  17075  dfod2  19635  sylow2blem1  19691  znhash  21689  hauspwdom  23639  rectbntr0  24971  ovolctb  25630  dyadmbl  25740  eupthfi  30534  padct  33041  karddom  35552  kardsdom  35553  kardexen  35554  derangen  35642  finminlem  36807  domalom  38028  phpreu  38233  pellexlem4  43539  pellexlem5  43540  pellex  43542