Theorem sseq1d 3277

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 3271	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1402   ⊆ wss 3220

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is referenced by:  sseq12d  3279  eqsstrd  3284  snssgOLD  3849  ssiun2s  4054  treq  4233  onsucsssucexmid  4672  funimass1  5456  feq1  5514  sbcfg  5530  fvmptssdm  5787  fvimacnvi  5817  nnsucsssuc  6759  ereq1  6808  elpm2r  6934  fipwssg  7307  nnnninf  7460  ctssexmid  7484  rspssp  14814  iscnp  15283  iscnp4  15302  cnntr  15309  cnconst2  15317  cnptopresti  15322  cnptoprest  15323  txbas  15342  txcnp  15355  txdis  15361  txdis1cn  15362  blssps  15511  blss  15512  ssblex  15515  blin2  15516  metss2  15582  metrest  15590  metcnp3  15595  cnopnap  15695  limccl  15743  ellimc3apf  15744  ausgrumgrien  16394  ausgrusgrien  16395  eupth2lem3lem4fi  16697