Theorem ensymi 8948

Description: Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by NM, 25-Sep-2004.)

Hypothesis

Ref	Expression
ensymi.2	⊢ 𝐴 ≈ 𝐵

Assertion

Ref	Expression
ensymi	⊢ 𝐵 ≈ 𝐴

Proof of Theorem ensymi

Step	Hyp	Ref	Expression
1		ensymi.2	. 2 ⊢ 𝐴 ≈ 𝐵
2		ensym 8947	. 2 ⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴)
3	1, 2	ax-mp 5	1 ⊢ 𝐵 ≈ 𝐴

Syntax hints:   class class class wbr 5079   ≈ cen 8887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-pow 5301  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-er 8640  df-en 8891

This theorem is referenced by:  entr2i  8953  entr3i  8954  entr4i  8955  pm54.43  9923  infxpenlem  9933  unsnen  10473  cfpwsdom  10505  tskinf  10690  inar1  10696  gruina  10739  uzenom  13924  znnen  16177  qnnen  16178  rexpen  16193  rucALT  16195  aleph1re  16210  aleph1irr  16211  unben  16878  ex-chn2  18602  1stcfb  23435  2ndcredom  23440  hauspwdom  23491  met1stc  24511  ovolctb2  25484  ovolfi  25486  ovoliunlem3  25496  uniiccdif  25570  dyadmbl  25592  mbfimaopnlem  25647  aannenlem3  26321  f1ocnt  32899  dmvlsiga  34320  sigapildsys  34353  omssubadd  34491  carsgclctunlem3  34511  pellex  43287  tr3dom  43979  nnfoctb  45503  nnf1oxpnn  45649  ioonct  45989  caragenunicl  46974  rrx2xpreen  49217  aacllem  50298