Theorem sseq2d 3257

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1397   ⊆ wss 3200

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  sseq12d  3258  sseqtrd  3265  exmidsssn  4292  exmidsssnc  4293  onsucsssucexmid  4625  sbcrel  4812  funimass2  5408  fnco  5440  fnssresb  5444  fnimaeq0  5454  foimacnv  5601  fvelimab  5702  ssimaexg  5708  fvmptss2  5721  rdgss  6549  tapeq2  7472  fzowrddc  11232  swrdnd  11244  swrd0g  11245  summodclem2  11948  summodc  11949  zsumdc  11950  fsum3cvg3  11962  prodmodclem2  12143  prodmodc  12144  zproddc  12145  ennnfoneleminc  13037  tgval  13350  prdsval  13361  releqgg  13812  eqgex  13813  eqgfval  13814  opprsubgg  14103  unitsubm  14139  subrngpropd  14236  subrgsubm  14254  issubrg3  14267  subrgpropd  14273  lsslss  14401  lsspropdg  14451  islidlm  14499  rspcl  14511  rspssid  14512  isbasisg  14774  tgss3  14808  restbasg  14898  tgrest  14899  restopn2  14913  cnpnei  14949  cnptopresti  14968  txbas  14988  elmopn  15176  neibl  15221  dvfgg  15418  incistruhgr  15947  edgssv2en  16056  wksfval  16179