Theorem sseq2d 3278

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1402   ⊆ wss 3220

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is referenced by:  sseq12d  3279  sseqtrd  3286  exmidsssn  4337  exmidsssnc  4338  onsucsssucexmid  4672  sbcrel  4859  funimass2  5457  fnco  5489  fnssresb  5493  fnimaeq0  5503  foimacnv  5655  fvelimab  5756  ssimaexg  5762  fvmptss2  5777  rdgss  6648  papeq2  7604  tapeq2  7613  fzowrddc  11402  swrdnd  11414  swrd0g  11415  summodclem2  12132  summodc  12133  zsumdc  12134  fsum3cvg3  12146  prodmodclem2  12327  prodmodc  12328  zproddc  12329  ennnfoneleminc  13285  tgval  13599  releqgg  14006  eqgex  14007  eqgfval  14008  prdsval  14156  opprsubgg  14373  unitsubm  14409  subrngpropd  14507  subrgsubm  14525  issubrg3  14538  subrgpropd  14544  lsslss  14701  lsspropdg  14751  islidlm  14799  rspcl  14811  rspssid  14812  isbasisg  15128  tgss3  15162  restbasg  15252  tgrest  15253  restopn2  15267  cnpnei  15303  cnptopresti  15322  txbas  15342  elmopn  15530  neibl  15575  dvfgg  15772  incistruhgr  16314  edgssv2en  16423  wksfval  16546