Theorem sseq1d 3233

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1375   ⊆ wss 3177

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 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-11 1532  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-ext 2191

This theorem depends on definitions:  df-bi 117  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-in 3183  df-ss 3190

This theorem is referenced by:  sseq12d  3235  eqsstrd  3240  snssgOLD  3783  ssiun2s  3988  treq  4167  onsucsssucexmid  4596  funimass1  5374  feq1  5432  sbcfg  5448  fvmptssdm  5692  fvimacnvi  5722  nnsucsssuc  6608  ereq1  6657  elpm2r  6783  fipwssg  7114  nnnninf  7261  ctssexmid  7285  rspssp  14423  iscnp  14838  iscnp4  14857  cnntr  14864  cnconst2  14872  cnptopresti  14877  cnptoprest  14878  txbas  14897  txcnp  14910  txdis  14916  txdis1cn  14917  blssps  15066  blss  15067  ssblex  15070  blin2  15071  metss2  15137  metrest  15145  metcnp3  15150  cnopnap  15250  limccl  15298  ellimc3apf  15299  ausgrumgrien  15933  ausgrusgrien  15934