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  11228  swrdnd  11240  swrd0g  11241  summodclem2  11944  summodc  11945  zsumdc  11946  fsum3cvg3  11958  prodmodclem2  12139  prodmodc  12140  zproddc  12141  ennnfoneleminc  13033  tgval  13346  prdsval  13357  releqgg  13808  eqgex  13809  eqgfval  13810  opprsubgg  14099  unitsubm  14135  subrngpropd  14232  subrgsubm  14250  issubrg3  14263  subrgpropd  14269  lsslss  14397  lsspropdg  14447  islidlm  14495  rspcl  14507  rspssid  14508  isbasisg  14770  tgss3  14804  restbasg  14894  tgrest  14895  restopn2  14909  cnpnei  14945  cnptopresti  14964  txbas  14984  elmopn  15172  neibl  15217  dvfgg  15414  incistruhgr  15943  edgssv2en  16052  wksfval  16175