Theorem eqimss2 3914

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

Syntax hints:   → wi 4   = wceq 1507   ⊆ wss 3829

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2750

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-in 3836  df-ss 3843

This theorem is referenced by:  ifpprsnss  4574  disjeq2  4901  disjeq1  4904  poeq2  5330  freq2  5378  seeq1  5379  seeq2  5380  dmcoeq  5687  xp11  5872  suc11  6132  funeq  6208  fimadmfoALT  6430  fconst3  6802  sorpssuni  7276  sorpssint  7277  tposeq  7697  oaass  7988  odi  8006  oen0  8013  inficl  8684  fodomfi2  9280  zorng  9724  rlimclim  14764  imasaddfnlem  16657  imasvscafn  16666  gasubg  18203  pgpssslw  18500  dprddisj2  18911  dprd2da  18914  evlslem6  20006  topgele  21242  topontopn  21252  connima  21737  islocfin  21829  ptbasfi  21893  txdis  21944  neifil  22192  elfm3  22262  rnelfmlem  22264  alexsubALTlem3  22361  alexsubALTlem4  22362  utopsnneiplem  22559  lmclimf  23610  uniiccdif  23882  dv11cn  24301  plypf1  24505  2pthon3v  27449  hstoh  29790  dmdi2  29862  disjeq1f  30090  eulerpartlemd  31275  rrvdmss  31359  refssfne  33233  neibastop3  33237  topmeet  33239  topjoin  33240  fnemeet2  33242  fnejoin1  33243  bj-restuni  33904  heiborlem3  34539  funALTVeq  35384  disjeq  35418  lsatelbN  35593  lkrscss  35685  lshpset2N  35706  mapdrvallem2  38232  hdmaprnlem3eN  38445  hdmaplkr  38500  uneqsn  39742  ssrecnpr  40062  founiiun  40865  founiiun0  40881  caragendifcl  42233