Theorem sseq1d 3186

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1353   ⊆ wss 3131

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3137  df-ss 3144

This theorem is referenced by:  sseq12d  3188  eqsstrd  3193  snssgOLD  3730  ssiun2s  3932  treq  4109  onsucsssucexmid  4528  funimass1  5295  feq1  5350  sbcfg  5366  fvmptssdm  5602  fvimacnvi  5632  nnsucsssuc  6495  ereq1  6544  elpm2r  6668  fipwssg  6980  nnnninf  7126  ctssexmid  7150  iscnp  13738  iscnp4  13757  cnntr  13764  cnconst2  13772  cnptopresti  13777  cnptoprest  13778  txbas  13797  txcnp  13810  txdis  13816  txdis1cn  13817  blssps  13966  blss  13967  ssblex  13970  blin2  13971  metss2  14037  metrest  14045  metcnp3  14050  cnopnap  14133  limccl  14167  ellimc3apf  14168