Theorem ensym 8864

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

Syntax hints:   → wi 4   class class class wbr 5092   ≈ cen 8801

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5243  ax-nul 5250  ax-pow 5308  ax-pr 5372  ax-un 7650

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3443  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4270  df-if 4474  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4853  df-br 5093  df-opab 5155  df-id 5518  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-fun 6481  df-fn 6482  df-f 6483  df-f1 6484  df-fo 6485  df-f1o 6486  df-er 8569  df-en 8805

This theorem is referenced by:  ensymi  8865  ensymd  8866  sbthb  8959  domnsym  8964  sdomdomtr  8975  domsdomtr  8977  enen1  8982  enen2  8983  domen1  8984  domen2  8985  sdomen1  8986  sdomen2  8987  domtriord  8988  xpen  9005  pwen  9015  nneneqOLD  9086  php2OLD  9088  php3OLD  9089  phpeqdOLD  9090  ominfOLD  9124  fineqvlem  9127  en1eqsnOLD  9140  dif1ennnALT  9142  enp1iOLD  9145  findcard3OLD  9151  isfinite2  9166  nnsdomgOLD  9168  domunfican  9185  infcntss  9186  fiint  9189  wdomen1  9433  wdomen2  9434  unxpwdom2  9445  karden  9752  finnum  9805  carden2b  9824  fidomtri2  9851  cardmin2  9856  pr2neOLD  9862  en2eleq  9865  infxpenlem  9870  acnen  9910  acnen2  9912  infpwfien  9919  alephordi  9931  alephinit  9952  dfac12lem2  10001  dfac12r  10003  undjudom  10024  djucomen  10034  djuinf  10045  pwsdompw  10061  infmap2  10075  ackbij1b  10096  cflim2  10120  fin4en1  10166  domfin4  10168  fin23lem25  10181  fin23lem23  10183  enfin1ai  10241  fin67  10252  isfin7-2  10253  fin1a2lem11  10267  axcc2lem  10293  axcclem  10314  numthcor  10351  carden  10408  sdomsdomcard  10417  canthnum  10506  canthwe  10508  canthp1lem2  10510  canthp1  10511  pwxpndom2  10522  gchdjuidm  10525  gchxpidm  10526  gchpwdom  10527  inawinalem  10546  grudomon  10674  isfinite4  14177  hashfn  14190  ramub2  16812  dfod2  19267  sylow2blem1  19321  znhash  20872  hauspwdom  22758  rectbntr0  24101  ovolctb  24760  dyadmbl  24870  eupthfi  28857  derangen  33433  finminlem  34603  domalom  35680  phpreu  35866  pellexlem4  40916  pellexlem5  40917  pellex  40919