Theorem ensym 8005

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

Syntax hints:   → wi 4   class class class wbr 4653   ≈ cen 7952

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-er 7742  df-en 7956

This theorem is referenced by:  ensymi  8006  ensymd  8007  sbthb  8081  domnsym  8086  sdomdomtr  8093  domsdomtr  8095  enen1  8100  enen2  8101  domen1  8102  domen2  8103  sdomen1  8104  sdomen2  8105  domtriord  8106  xpen  8123  pwen  8133  nneneq  8143  php2  8145  php3  8146  ominf  8172  fineqvlem  8174  en1eqsn  8190  dif1en  8193  enp1i  8195  findcard3  8203  isfinite2  8218  nnsdomg  8219  domunfican  8233  infcntss  8234  fiint  8237  wdomen1  8481  wdomen2  8482  unxpwdom2  8493  karden  8758  finnum  8774  carden2b  8793  fidomtri2  8820  cardmin2  8824  pr2ne  8828  en2eleq  8831  infxpenlem  8836  acnen  8876  acnen2  8878  infpwfien  8885  alephordi  8897  alephinit  8918  dfac12lem2  8966  dfac12r  8968  uncdadom  8993  cdacomen  9003  cdainf  9014  pwsdompw  9026  infmap2  9040  ackbij1b  9061  cflim2  9085  fin4en1  9131  domfin4  9133  fin23lem25  9146  fin23lem23  9148  enfin1ai  9206  fin67  9217  isfin7-2  9218  fin1a2lem11  9232  axcc2lem  9258  axcclem  9279  numthcor  9316  carden  9373  sdomsdomcard  9382  canthnum  9471  canthwe  9473  canthp1lem2  9475  canthp1  9476  pwxpndom2  9487  gchcdaidm  9490  gchxpidm  9491  gchpwdom  9492  inawinalem  9511  grudomon  9639  isfinite4  13153  hashfn  13164  ramub2  15718  dfod2  17981  sylow2blem1  18035  znhash  19907  hauspwdom  21304  rectbntr0  22635  ovolctb  23258  dyadmbl  23368  eupthfi  27065  derangen  31154  finminlem  32312  phpreu  33393  pellexlem4  37396  pellexlem5  37397  pellex  37399