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  6659  isfsuppfi  7296  funisfsuppdc  7299  papeq2  7617  tapeq2  7626  fzowrddc  11441  swrdnd  11453  swrd0g  11454  summodclem2  12174  summodc  12175  zsumdc  12176  fsum3cvg3  12188  prodmodclem2  12369  prodmodc  12370  zproddc  12371  ennnfoneleminc  13360  tgval  13675  releqgg  14082  eqgex  14083  eqgfval  14084  sscntz  14158  resscntz  14166  prdsval  14280  opprsubgg  14499  unitsubm  14535  subrngpropd  14633  subrgsubm  14651  issubrg3  14664  subrgpropd  14670  lsslss  14827  lsspropdg  14877  islidlm  14925  rspcl  14937  rspssid  14938  psrbagfsuppub  15192  mplsubgfilemcl  15246  mplsubgfileminv  15247  isbasisg  15303  tgss3  15337  restbasg  15427  tgrest  15428  restopn2  15442  cnpnei  15478  cnptopresti  15497  txbas  15517  elmopn  15705  neibl  15750  dvfgg  15947  incistruhgr  16569  edgssv2en  16678  wksfval  16801