Theorem eqimss2 3621

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

Syntax hints:   → wi 4   = wceq 1475   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554

This theorem is referenced by:  disjeq2  4557  disjeq1  4560  poeq2  4963  freq2  5009  seeq1  5010  seeq2  5011  dmcoeq  5309  xp11  5488  suc11  5748  funeq  5823  fconst3  6382  sorpssuni  6844  sorpssint  6845  tposeq  7241  oaass  7528  odi  7546  oen0  7553  inficl  8214  cantnfp1lem1  8458  cantnflem1  8469  fodomfi2  8766  zorng  9209  rlimclim  14125  imasaddfnlem  16011  imasvscafn  16020  gasubg  17558  pgpssslw  17852  dprddisj2  18261  dprd2da  18264  evlslem6  19334  topgele  20549  topontopn  20557  toponmre  20707  conima  21038  islocfin  21130  ptbasfi  21194  txdis  21245  neifil  21494  elfm3  21564  rnelfmlem  21566  alexsubALTlem3  21663  alexsubALTlem4  21664  utopsnneiplem  21861  lmclimf  22910  uniiccdif  23152  dv11cn  23568  plypf1  23772  hstoh  28475  dmdi2  28547  disjeq1f  28769  eulerpartlemd  29755  rrvdmss  29838  refssfne  31523  neibastop3  31527  topmeet  31529  topjoin  31530  fnemeet2  31532  fnejoin1  31533  bj-restuni  32231  heiborlem3  32782  lsatelbN  33311  lkrscss  33403  lshpset2N  33424  mapdrvallem2  35952  hdmaprnlem3eN  36168  hdmaplkr  36223  uneqsn  37341  ssrecnpr  37529  founiiun  38355  founiiun0  38372  caragendifcl  39404  ifpprsnss  40845  2pthon3v-av  41150