MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  endom Unicode version

Theorem endom 7562
Description: Equinumerosity implies dominance. Theorem 15 of [Suppes] p. 94. (Contributed by NM, 28-May-1998.)
Assertion
Ref Expression
endom

Proof of Theorem endom
StepHypRef Expression
1 enssdom 7560 . 2
21ssbri 4494 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4   class class class wbr 4452   cen 7533   cdom 7534
This theorem is referenced by:  bren2  7566  domrefg  7570  endomtr  7593  domentr  7594  domunsncan  7637  sbthb  7658  sdomentr  7671  ensdomtr  7673  domtriord  7683  domunsn  7687  xpen  7700  unxpdom2  7748  sucxpdom  7749  wdomen1  8023  wdomen2  8024  fidomtri2  8396  prdom2  8405  acnen  8455  acnen2  8457  alephdom  8483  alephinit  8497  uncdadom  8572  pwcdadom  8617  fin1a2lem11  8811  hsmexlem1  8827  gchdomtri  9028  gchcdaidm  9067  gchxpidm  9068  gchpwdom  9069  gchhar  9078  gruina  9217  odinf  16585  hauspwdom  20002  ufildom1  20427  iscmet3  21732  ovolctb2  21903  mbfaddlem  22067  nnct  27529  heiborlem3  30309
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-opab 4511  df-xp 5010  df-rel 5011  df-f1o 5600  df-en 7537  df-dom 7538
  Copyright terms: Public domain W3C validator