Theorem eqsstrd 2098

Description: Substitution of equality into a subclass relationship.

Hypotheses

Ref	Expression
eqsstrd.1	⊢ (φ → A = B)
eqsstrd.2	⊢ (φ → B ⊆ C)

Assertion

Ref	Expression
eqsstrd	⊢ (φ → A ⊆ C)

Proof of Theorem eqsstrd

Step	Hyp	Ref	Expression
1		eqsstrd.2	. 2 ⊢ (φ → B ⊆ C)
2		eqsstrd.1	. . 3 ⊢ (φ → A = B)
3	2	sseq1d 2091	. 2 ⊢ (φ → (A ⊆ C ↔ B ⊆ C))
4	1, 3	mpbird 196	1 ⊢ (φ → A ⊆ C)

Syntax hints:   → wi 3   = wceq 958   ⊆ wss 2050

This theorem is referenced by:  eqsstr3d 2099  snsspr 2474  fimacnv 3816  oawordeulem 4194  oewordri 4225  oaabslem 4257  mapsspw 4347  fodomr 4489  r1val1 4668  cardonle 4832  carduniima 4901  cfub 4920  cflecard 4924  uzssz 6431  infxpidmlem7 7559  infxpidmlem8 7560  ntrss2 7687  lpsscls 7742  cnconst 7777  blssm 7847  rnblssm 7848  opnfss 7855  tgioolem 7911  chssoct 9414  specclt 9820  elnlfn2t 9848  mdsl0 10232  mdexch 10257  atcvat3 10318  dmdbr5at 10344  clsrebb 10479  subsp 10540

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-in 2054  df-ss 2056

Copyright terms: Public domain