Theorem eqsstrd 3260

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)

Hypotheses

Ref	Expression
eqsstrd.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqsstrd.2	⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Assertion

Ref	Expression
eqsstrd	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem eqsstrd

Step	Hyp	Ref	Expression
1		eqsstrd.2	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
2		eqsstrd.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	2	sseq1d 3253	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
4	1, 3	mpbird 167	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1395   ⊆ wss 3197

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  eqsstrrd  3261  eqsstrdi  3276  tfisi  4678  funresdfunsnss  5841  suppssof1  6234  pw2f1odclem  6991  phplem4dom  7019  fival  7133  fiuni  7141  cardonle  7355  exmidfodomrlemim  7375  frecuzrdgtclt  10638  4sqlem19  12927  ennnfonelemkh  12978  ennnfonelemf1  12984  strfvssn  13049  setscom  13067  imasaddfnlemg  13342  imasaddflemg  13344  reldvdsrsrg  14050  znleval  14611  tgrest  14837  resttopon  14839  rest0  14847  lmtopcnp  14918  metequiv2  15164  xmettx  15178  ellimc3apf  15328  dvfvalap  15349  dvcjbr  15376  dvcj  15377  dvfre  15378  uhgredgm  15928  upgredgssen  15931  umgredgssen  15932  edgumgren  15934  usgredgssen  15954  nnsf  16330