Theorem ensym 9033

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

This proof depends on syntax axioms:   → wi 4   class class class wbr 5102   ≈ cen 8973

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pow 5326  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-er 8720  df-en 8977

This theorem is used by:  ensymi  9034  ensymd  9035  sbthb  9120  domnsym  9125  sdomdomtr  9132  domsdomtr  9134  enen1  9139  enen2  9140  domen1  9141  domen2  9142  sdomen1  9143  sdomen2  9144  domtriord  9145  xpen  9162  pwen  9172  fineqvlem  9260  dif1ennnALT  9271  isfinite2  9293  domunfican  9316  infcntss  9317  wdomen1  9573  wdomen2  9574  unxpwdom2  9585  kardenOLD  9963  finnum  10032  carden2b  10051  fidomtri2  10078  cardmin2  10083  en2eleq  10090  infxpenlem  10095  acnen  10135  acnen2  10137  infpwfien  10144  alephordi  10156  alephinit  10177  dfac12lem2  10226  dfac12r  10228  undjudom  10249  djucomen  10259  djuinf  10270  pwsdompw  10284  infmap2  10298  ackbij1b  10319  cflim2  10344  fin4en1  10390  domfin4  10392  fin23lem25  10405  fin23lem23  10407  enfin1ai  10465  fin67  10476  isfin7-2  10477  fin1a2lem11  10491  axcc2lem  10517  axcclem  10538  numthcor  10575  carden  10638  sdomsdomcard  10647  canthnum  10737  canthwe  10739  canthp1lem2  10741  canthp1  10742  pwxpndom2  10753  gchdjuidm  10756  gchxpidm  10757  gchpwdom  10758  inawinalem  10777  grudomon  10905  isfinite4  14509  hashfn  14522  ramub2  17197  dfod2  19783  sylow2blem1  19839  znhash  21869  hauspwdom  23825  rectbntr0  25157  ovolctb  25816  dyadmbl  25926  eupthfi  30811  padct  33357  dfac16  35810  karddom  35885  kardsdom  35886  kardexen  35887  derangen  36023  finminlem  37198  domalom  38420  phpreu  38620  pellexlem4  43932  pellexlem5  43933  pellex  43935