Theorem sseq1d 3269

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1398   ⊆ wss 3213

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3219  df-ss 3226

This theorem is referenced by:  sseq12d  3271  eqsstrd  3276  snssgOLD  3832  ssiun2s  4037  treq  4216  onsucsssucexmid  4651  funimass1  5435  feq1  5493  sbcfg  5509  fvmptssdm  5764  fvimacnvi  5794  nnsucsssuc  6727  ereq1  6776  elpm2r  6902  fipwssg  7268  nnnninf  7419  ctssexmid  7443  rspssp  14691  iscnp  15113  iscnp4  15132  cnntr  15139  cnconst2  15147  cnptopresti  15152  cnptoprest  15153  txbas  15172  txcnp  15185  txdis  15191  txdis1cn  15192  blssps  15341  blss  15342  ssblex  15345  blin2  15346  metss2  15412  metrest  15420  metcnp3  15425  cnopnap  15525  limccl  15573  ellimc3apf  15574  ausgrumgrien  16214  ausgrusgrien  16215  eupth2lem3lem4fi  16517