Theorem eqimss2 3820

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 3819	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	eqcoms 2773	1 ⊢ (𝐵 = 𝐴 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   = wceq 1652   ⊆ wss 3734

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-in 3741  df-ss 3748

This theorem is referenced by:  ifpprsnss  4456  disjeq2  4783  disjeq1  4786  poeq2  5204  freq2  5250  seeq1  5251  seeq2  5252  dmcoeq  5559  xp11  5754  suc11  6013  funeq  6090  fconst3  6672  sorpssuni  7146  sorpssint  7147  tposeq  7559  oaass  7848  odi  7866  oen0  7873  inficl  8540  cantnfp1lem1  8792  fodomfi2  9136  zorng  9581  rlimclim  14565  imasaddfnlem  16457  imasvscafn  16466  gasubg  18001  pgpssslw  18296  dprddisj2  18708  dprd2da  18711  evlslem6  19789  topgele  21017  topontopn  21027  toponmre  21180  connima  21511  islocfin  21603  ptbasfi  21667  txdis  21718  neifil  21966  elfm3  22036  rnelfmlem  22038  alexsubALTlem3  22135  alexsubALTlem4  22136  utopsnneiplem  22333  lmclimf  23384  uniiccdif  23639  dv11cn  24058  plypf1  24262  2pthon3v  27169  hstoh  29550  dmdi2  29622  disjeq1f  29838  eulerpartlemd  30878  rrvdmss  30962  refssfne  32799  neibastop3  32803  topmeet  32805  topjoin  32806  fnemeet2  32808  fnejoin1  32809  bj-restuni  33481  heiborlem3  34037  lsatelbN  34965  lkrscss  35057  lshpset2N  35078  mapdrvallem2  37604  hdmaprnlem3eN  37817  hdmaplkr  37872  uneqsn  38998  ssrecnpr  39184  founiiun  40010  founiiun0  40027  caragendifcl  41371