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 ⊢ (𝜑 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   = wceq 1402   ⊆ wss 3220

This proof depends on 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 proof 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 used by:  sseq12d  3279  sseqtrd  3286  exmidsssn  4341  exmidsssnc  4342  onsucsssucexmid  4676  sbcrel  4863  funimass2  5462  fnco  5494  fnssresb  5498  fnimaeq0  5508  foimacnv  5660  fvelimab  5762  ssimaexg  5768  fvmptss2  5783  rdgss  6658  papeq2  7617  tapeq2  7626  fzowrddc  11442  swrdnd  11454  swrd0g  11455  summodclem2  12175  summodc  12176  zsumdc  12177  fsum3cvg3  12189  prodmodclem2  12370  prodmodc  12371  zproddc  12372  ennnfoneleminc  13361  tgval  13676  releqgg  14083  eqgex  14084  eqgfval  14085  sscntz  14159  resscntz  14167  prdsval  14281  opprsubgg  14500  unitsubm  14536  subrngpropd  14634  subrgsubm  14652  issubrg3  14665  subrgpropd  14671  lsslss  14828  lsspropdg  14878  islidlm  14926  rspcl  14938  rspssid  14939  isbasisg  15282  tgss3  15316  restbasg  15406  tgrest  15407  restopn2  15421  cnpnei  15457  cnptopresti  15476  txbas  15496  elmopn  15684  neibl  15729  dvfgg  15926  incistruhgr  16548  edgssv2en  16657  wksfval  16780