Theorem ensym 9058

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

This proof depends on syntax axioms:   → wi 4   class class class wbr 5106   ≈ cen 8998

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-pow 5331  ax-pr 5395  ax-un 7775

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 2102  df-mo 2567  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-er 8745  df-en 9002

This theorem is used by:  ensymi  9059  ensymd  9060  sbthb  9145  domnsym  9150  sdomdomtr  9157  domsdomtr  9159  enen1  9164  enen2  9165  domen1  9166  domen2  9167  sdomen1  9168  sdomen2  9169  domtriord  9170  xpen  9187  pwen  9197  fineqvlem  9285  dif1ennnALT  9296  isfinite2  9318  domunfican  9341  infcntss  9342  wdomen1  9597  wdomen2  9598  unxpwdom2  9609  kardenOLD  9987  finnum  10056  carden2b  10075  fidomtri2  10102  cardmin2  10107  en2eleq  10114  infxpenlem  10119  acnen  10159  acnen2  10161  infpwfien  10168  alephordi  10180  alephinit  10201  dfac12lem2  10250  dfac12r  10252  undjudom  10273  djucomen  10283  djuinf  10294  pwsdompw  10308  infmap2  10322  ackbij1b  10343  cflim2  10368  fin4en1  10414  domfin4  10416  fin23lem25  10429  fin23lem23  10431  enfin1ai  10489  fin67  10500  isfin7-2  10501  fin1a2lem11  10515  axcc2lem  10541  axcclem  10562  numthcor  10599  carden  10662  sdomsdomcard  10671  canthnum  10761  canthwe  10763  canthp1lem2  10765  canthp1  10766  pwxpndom2  10777  gchdjuidm  10780  gchxpidm  10781  gchpwdom  10782  inawinalem  10801  grudomon  10929  isfinite4  14533  hashfn  14546  ramub2  17221  dfod2  19808  sylow2blem1  19864  znhash  21894  hauspwdom  23850  rectbntr0  25182  ovolctb  25841  dyadmbl  25951  eupthfi  30836  padct  33381  dfac16  35846  karddom  35929  kardsdom  35930  kardexen  35931  jltalephlem  36025  derangen  36104  finminlem  37284  domalom  38519  phpreu  38719  pellexlem4  44032  pellexlem5  44033  pellex  44035