Theorem eqimss2 3807

Description: Equality implies the subclass relation. (Contributed by NM, 23-Nov-2003.)

Assertion

Ref	Expression
eqimss2	⊢ (𝐵 = 𝐴 → 𝐴 ⊆ 𝐵)

Proof of Theorem eqimss2

Step	Hyp	Ref	Expression
1		eqimss 3806	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	eqcoms 2779	1 ⊢ (𝐵 = 𝐴 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   = wceq 1631   ⊆ wss 3723

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-in 3730  df-ss 3737

This theorem is referenced by:  ifpprsnss  4436  disjeq2  4759  disjeq1  4762  poeq2  5175  freq2  5221  seeq1  5222  seeq2  5223  dmcoeq  5525  xp11  5709  suc11  5973  funeq  6050  fconst3  6623  sorpssuni  7096  sorpssint  7097  tposeq  7509  oaass  7798  odi  7816  oen0  7823  inficl  8490  cantnfp1lem1  8742  cantnflem1  8753  fodomfi2  9086  zorng  9531  rlimclim  14484  imasaddfnlem  16395  imasvscafn  16404  gasubg  17941  pgpssslw  18235  dprddisj2  18645  dprd2da  18648  evlslem6  19727  topgele  20954  topontopn  20964  toponmre  21117  connima  21448  islocfin  21540  ptbasfi  21604  txdis  21655  neifil  21903  elfm3  21973  rnelfmlem  21975  alexsubALTlem3  22072  alexsubALTlem4  22073  utopsnneiplem  22270  lmclimf  23320  uniiccdif  23565  dv11cn  23983  plypf1  24187  2pthon3v  27089  hstoh  29430  dmdi2  29502  disjeq1f  29724  eulerpartlemd  30767  rrvdmss  30850  refssfne  32689  neibastop3  32693  topmeet  32695  topjoin  32696  fnemeet2  32698  fnejoin1  32699  bj-restuni  33381  heiborlem3  33943  lsatelbN  34814  lkrscss  34906  lshpset2N  34927  mapdrvallem2  37455  hdmaprnlem3eN  37668  hdmaplkr  37723  uneqsn  38847  ssrecnpr  39033  founiiun  39879  founiiun0  39896  caragendifcl  41245