Theorem ensym 8170

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

Syntax hints:   → wi 4   class class class wbr 4804   ≈ cen 8118

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-er 7911  df-en 8122

This theorem is referenced by:  ensymi  8171  ensymd  8172  sbthb  8246  domnsym  8251  sdomdomtr  8258  domsdomtr  8260  enen1  8265  enen2  8266  domen1  8267  domen2  8268  sdomen1  8269  sdomen2  8270  domtriord  8271  xpen  8288  pwen  8298  nneneq  8308  php2  8310  php3  8311  ominf  8337  fineqvlem  8339  en1eqsn  8355  dif1en  8358  enp1i  8360  findcard3  8368  isfinite2  8383  nnsdomg  8384  domunfican  8398  infcntss  8399  fiint  8402  wdomen1  8646  wdomen2  8647  unxpwdom2  8658  karden  8931  finnum  8964  carden2b  8983  fidomtri2  9010  cardmin2  9014  pr2ne  9018  en2eleq  9021  infxpenlem  9026  acnen  9066  acnen2  9068  infpwfien  9075  alephordi  9087  alephinit  9108  dfac12lem2  9158  dfac12r  9160  uncdadom  9185  cdacomen  9195  cdainf  9206  pwsdompw  9218  infmap2  9232  ackbij1b  9253  cflim2  9277  fin4en1  9323  domfin4  9325  fin23lem25  9338  fin23lem23  9340  enfin1ai  9398  fin67  9409  isfin7-2  9410  fin1a2lem11  9424  axcc2lem  9450  axcclem  9471  numthcor  9508  carden  9565  sdomsdomcard  9574  canthnum  9663  canthwe  9665  canthp1lem2  9667  canthp1  9668  pwxpndom2  9679  gchcdaidm  9682  gchxpidm  9683  gchpwdom  9684  inawinalem  9703  grudomon  9831  isfinite4  13345  hashfn  13356  ramub2  15920  dfod2  18181  sylow2blem1  18235  znhash  20109  hauspwdom  21506  rectbntr0  22836  ovolctb  23458  dyadmbl  23568  eupthfi  27357  derangen  31461  finminlem  32618  phpreu  33706  pellexlem4  37898  pellexlem5  37899  pellex  37901