Theorem ensymi 8944

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 8943	. 2 ⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴)
3	1, 2	ax-mp 5	1 ⊢ 𝐵 ≈ 𝐴

Syntax hints:   class class class wbr 5086   ≈ cen 8883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-pow 5302  ax-pr 5370  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-er 8636  df-en 8887

This theorem is referenced by:  entr2i  8949  entr3i  8950  entr4i  8951  pm54.43  9916  infxpenlem  9926  unsnen  10466  cfpwsdom  10498  tskinf  10683  inar1  10689  gruina  10732  uzenom  13917  znnen  16170  qnnen  16171  rexpen  16186  rucALT  16188  aleph1re  16203  aleph1irr  16204  unben  16871  ex-chn2  18595  1stcfb  23420  2ndcredom  23425  hauspwdom  23476  met1stc  24496  ovolctb2  25469  ovolfi  25471  ovoliunlem3  25481  uniiccdif  25555  dyadmbl  25577  mbfimaopnlem  25632  aannenlem3  26307  f1ocnt  32888  dmvlsiga  34289  sigapildsys  34322  omssubadd  34460  carsgclctunlem3  34480  pellex  43281  tr3dom  43973  nnfoctb  45497  nnf1oxpnn  45643  ioonct  45985  caragenunicl  46970  rrx2xpreen  49207  aacllem  50288