Theorem sseq1d 3076

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1299   ⊆ wss 3021

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-11 1452  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-in 3027  df-ss 3034

This theorem is referenced by:  sseq12d  3078  eqsstrd  3083  snssg  3603  ssiun2s  3804  treq  3972  onsucsssucexmid  4380  funimass1  5136  feq1  5191  sbcfg  5207  fvmptssdm  5437  fvimacnvi  5466  nnsucsssuc  6318  ereq1  6366  elpm2r  6490  nnnninf  6935  ctssexmid  6936  iscnp  12149  iscnp4  12168  cnntr  12175  cnconst2  12183  cnptopresti  12188  cnptoprest  12189  txbas  12208  txcnp  12221  txdis  12227  txdis1cn  12228  blssps  12355  blss  12356  ssblex  12359  blin2  12360  metss2  12426  metrest  12434  metcnp3  12435  limccl  12510  ellimc3ap  12511