Theorem sseq1d 3184

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

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

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 3135  df-ss 3142

This theorem is referenced by:  sseq12d  3186  eqsstrd  3191  snssgOLD  3728  ssiun2s  3930  treq  4107  onsucsssucexmid  4526  funimass1  5293  feq1  5348  sbcfg  5364  fvmptssdm  5600  fvimacnvi  5630  nnsucsssuc  6492  ereq1  6541  elpm2r  6665  fipwssg  6977  nnnninf  7123  ctssexmid  7147  iscnp  13669  iscnp4  13688  cnntr  13695  cnconst2  13703  cnptopresti  13708  cnptoprest  13709  txbas  13728  txcnp  13741  txdis  13747  txdis1cn  13748  blssps  13897  blss  13898  ssblex  13901  blin2  13902  metss2  13968  metrest  13976  metcnp3  13981  cnopnap  14064  limccl  14098  ellimc3apf  14099