Theorem sseq2d 3272

Description: An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.)

Hypothesis

Ref	Expression
sseq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
sseq2d	⊢ (𝜑 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))

Proof of Theorem sseq2d

Step	Hyp	Ref	Expression
1		sseq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		sseq2 3266	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))

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

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 3220  df-ss 3227

This theorem is referenced by:  sseq12d  3273  sseqtrd  3280  exmidsssn  4320  exmidsssnc  4321  onsucsssucexmid  4654  sbcrel  4841  funimass2  5439  fnco  5471  fnssresb  5475  fnimaeq0  5485  foimacnv  5637  fvelimab  5738  ssimaexg  5744  fvmptss2  5757  rdgss  6627  papeq2  7574  tapeq2  7583  fzowrddc  11367  swrdnd  11379  swrd0g  11380  summodclem2  12097  summodc  12098  zsumdc  12099  fsum3cvg3  12111  prodmodclem2  12292  prodmodc  12293  zproddc  12294  ennnfoneleminc  13250  tgval  13563  releqgg  13977  eqgex  13978  eqgfval  13979  prdsval  14119  opprsubgg  14332  unitsubm  14368  subrngpropd  14466  subrgsubm  14484  issubrg3  14497  subrgpropd  14503  lsslss  14659  lsspropdg  14709  islidlm  14757  rspcl  14769  rspssid  14770  isbasisg  15039  tgss3  15073  restbasg  15163  tgrest  15164  restopn2  15178  cnpnei  15214  cnptopresti  15233  txbas  15253  elmopn  15441  neibl  15486  dvfgg  15683  incistruhgr  16215  edgssv2en  16324  wksfval  16447