Theorem sseq1d 3176

Description: An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.)

Hypothesis

Ref	Expression
sseq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
sseq1d	⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))

Proof of Theorem sseq1d

Step	Hyp	Ref	Expression
1		sseq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		sseq1 3170	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1348   ⊆ wss 3121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134

This theorem is referenced by:  sseq12d  3178  eqsstrd  3183  snssg  3714  ssiun2s  3915  treq  4091  onsucsssucexmid  4509  funimass1  5273  feq1  5328  sbcfg  5344  fvmptssdm  5578  fvimacnvi  5607  nnsucsssuc  6468  ereq1  6516  elpm2r  6640  fipwssg  6952  nnnninf  7098  ctssexmid  7122  iscnp  12952  iscnp4  12971  cnntr  12978  cnconst2  12986  cnptopresti  12991  cnptoprest  12992  txbas  13011  txcnp  13024  txdis  13030  txdis1cn  13031  blssps  13180  blss  13181  ssblex  13184  blin2  13185  metss2  13251  metrest  13259  metcnp3  13264  cnopnap  13347  limccl  13381  ellimc3apf  13382