Theorem ensym 8409

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

Syntax hints:   → wi 4   class class class wbr 4964   ≈ cen 8357

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-8 2082  ax-9 2090  ax-10 2111  ax-11 2125  ax-12 2140  ax-13 2343  ax-ext 2768  ax-sep 5097  ax-nul 5104  ax-pow 5160  ax-pr 5224  ax-un 7322

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1763  df-nf 1767  df-sb 2042  df-mo 2575  df-eu 2611  df-clab 2775  df-cleq 2787  df-clel 2862  df-nfc 2934  df-ral 3109  df-rex 3110  df-rab 3113  df-v 3438  df-dif 3864  df-un 3866  df-in 3868  df-ss 3876  df-nul 4214  df-if 4384  df-pw 4457  df-sn 4475  df-pr 4477  df-op 4481  df-uni 4748  df-br 4965  df-opab 5027  df-id 5351  df-xp 5452  df-rel 5453  df-cnv 5454  df-co 5455  df-dm 5456  df-rn 5457  df-res 5458  df-ima 5459  df-fun 6230  df-fn 6231  df-f 6232  df-f1 6233  df-fo 6234  df-f1o 6235  df-er 8142  df-en 8361

This theorem is referenced by:  ensymi  8410  ensymd  8411  sbthb  8488  domnsym  8493  sdomdomtr  8500  domsdomtr  8502  enen1  8507  enen2  8508  domen1  8509  domen2  8510  sdomen1  8511  sdomen2  8512  domtriord  8513  xpen  8530  pwen  8540  nneneq  8550  php2  8552  php3  8553  ominf  8579  fineqvlem  8581  en1eqsn  8597  dif1en  8600  enp1i  8602  findcard3  8610  isfinite2  8625  nnsdomg  8626  domunfican  8640  infcntss  8641  fiint  8644  wdomen1  8889  wdomen2  8890  unxpwdom2  8901  karden  9173  finnum  9226  carden2b  9245  fidomtri2  9272  cardmin2  9276  pr2ne  9280  en2eleq  9283  infxpenlem  9288  acnen  9328  acnen2  9330  infpwfien  9337  alephordi  9349  alephinit  9370  dfac12lem2  9419  dfac12r  9421  undjudom  9442  djucomen  9452  djuinf  9463  pwsdompw  9475  infmap2  9489  ackbij1b  9510  cflim2  9534  fin4en1  9580  domfin4  9582  fin23lem25  9595  fin23lem23  9597  enfin1ai  9655  fin67  9666  isfin7-2  9667  fin1a2lem11  9681  axcc2lem  9707  axcclem  9728  numthcor  9765  carden  9822  sdomsdomcard  9831  canthnum  9920  canthwe  9922  canthp1lem2  9924  canthp1  9925  pwxpndom2  9936  gchdjuidm  9939  gchxpidm  9940  gchpwdom  9941  inawinalem  9960  grudomon  10088  isfinite4  13573  hashfn  13584  ramub2  16179  dfod2  18421  sylow2blem1  18475  znhash  20387  hauspwdom  21793  rectbntr0  23123  ovolctb  23774  dyadmbl  23884  eupthfi  27666  derangen  32021  finminlem  33269  domalom  34229  phpreu  34420  pellexlem4  38927  pellexlem5  38928  pellex  38930  rr-php2d  40066