Theorem sseq1d 3266

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

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

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 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-in 3216  df-ss 3223

This theorem is referenced by:  sseq12d  3268  eqsstrd  3273  snssgOLD  3829  ssiun2s  4034  treq  4213  onsucsssucexmid  4648  funimass1  5432  feq1  5490  sbcfg  5506  fvmptssdm  5761  fvimacnvi  5791  nnsucsssuc  6724  ereq1  6773  elpm2r  6899  fipwssg  7265  nnnninf  7416  ctssexmid  7440  rspssp  14629  iscnp  15051  iscnp4  15070  cnntr  15077  cnconst2  15085  cnptopresti  15090  cnptoprest  15091  txbas  15110  txcnp  15123  txdis  15129  txdis1cn  15130  blssps  15279  blss  15280  ssblex  15283  blin2  15284  metss2  15350  metrest  15358  metcnp3  15363  cnopnap  15463  limccl  15511  ellimc3apf  15512  ausgrumgrien  16152  ausgrusgrien  16153  eupth2lem3lem4fi  16455