Theorem sseq1d 3131

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1332   ⊆ wss 3076

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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-11 1485  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-in 3082  df-ss 3089

This theorem is referenced by:  sseq12d  3133  eqsstrd  3138  snssg  3664  ssiun2s  3865  treq  4040  onsucsssucexmid  4450  funimass1  5208  feq1  5263  sbcfg  5279  fvmptssdm  5513  fvimacnvi  5542  nnsucsssuc  6396  ereq1  6444  elpm2r  6568  fipwssg  6875  nnnninf  7031  ctssexmid  7032  iscnp  12407  iscnp4  12426  cnntr  12433  cnconst2  12441  cnptopresti  12446  cnptoprest  12447  txbas  12466  txcnp  12479  txdis  12485  txdis1cn  12486  blssps  12635  blss  12636  ssblex  12639  blin2  12640  metss2  12706  metrest  12714  metcnp3  12719  cnopnap  12802  limccl  12836  ellimc3apf  12837