Theorem eqimss2 3799

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

Syntax hints:   → wi 4   = wceq 1632   ⊆ wss 3715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-in 3722  df-ss 3729

This theorem is referenced by:  ifpprsnss  4443  disjeq2  4776  disjeq1  4779  poeq2  5191  freq2  5237  seeq1  5238  seeq2  5239  dmcoeq  5543  xp11  5727  suc11  5992  funeq  6069  fconst3  6641  sorpssuni  7111  sorpssint  7112  tposeq  7523  oaass  7810  odi  7828  oen0  7835  inficl  8496  cantnfp1lem1  8748  cantnflem1  8759  fodomfi2  9073  zorng  9518  rlimclim  14476  imasaddfnlem  16390  imasvscafn  16399  gasubg  17935  pgpssslw  18229  dprddisj2  18638  dprd2da  18641  evlslem6  19715  topgele  20936  topontopn  20946  toponmre  21099  connima  21430  islocfin  21522  ptbasfi  21586  txdis  21637  neifil  21885  elfm3  21955  rnelfmlem  21957  alexsubALTlem3  22054  alexsubALTlem4  22055  utopsnneiplem  22252  lmclimf  23302  uniiccdif  23546  dv11cn  23963  plypf1  24167  2pthon3v  27063  hstoh  29400  dmdi2  29472  disjeq1f  29694  eulerpartlemd  30737  rrvdmss  30820  refssfne  32659  neibastop3  32663  topmeet  32665  topjoin  32666  fnemeet2  32668  fnejoin1  32669  bj-restuni  33356  heiborlem3  33925  lsatelbN  34796  lkrscss  34888  lshpset2N  34909  mapdrvallem2  37436  hdmaprnlem3eN  37652  hdmaplkr  37707  uneqsn  38823  ssrecnpr  39009  founiiun  39859  founiiun0  39876  caragendifcl  41234