Theorem sseq1d 3126

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1331   ⊆ wss 3071

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 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-in 3077  df-ss 3084

This theorem is referenced by:  sseq12d  3128  eqsstrd  3133  snssg  3656  ssiun2s  3857  treq  4032  onsucsssucexmid  4442  funimass1  5200  feq1  5255  sbcfg  5271  fvmptssdm  5505  fvimacnvi  5534  nnsucsssuc  6388  ereq1  6436  elpm2r  6560  fipwssg  6867  nnnninf  7023  ctssexmid  7024  iscnp  12368  iscnp4  12387  cnntr  12394  cnconst2  12402  cnptopresti  12407  cnptoprest  12408  txbas  12427  txcnp  12440  txdis  12446  txdis1cn  12447  blssps  12596  blss  12597  ssblex  12600  blin2  12601  metss2  12667  metrest  12675  metcnp3  12680  cnopnap  12763  limccl  12797  ellimc3apf  12798