Theorem sseq2d 3213

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1364   ⊆ wss 3157

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170

This theorem is referenced by:  sseq12d  3214  sseqtrd  3221  exmidsssn  4235  exmidsssnc  4236  onsucsssucexmid  4563  sbcrel  4749  funimass2  5336  fnco  5366  fnssresb  5370  fnimaeq0  5379  foimacnv  5522  fvelimab  5617  ssimaexg  5623  fvmptss2  5636  rdgss  6441  tapeq2  7320  summodclem2  11547  summodc  11548  zsumdc  11549  fsum3cvg3  11561  prodmodclem2  11742  prodmodc  11743  zproddc  11744  ennnfoneleminc  12628  tgval  12933  releqgg  13350  eqgex  13351  eqgfval  13352  opprsubgg  13640  unitsubm  13675  subrngpropd  13772  subrgsubm  13790  issubrg3  13803  subrgpropd  13809  lsslss  13937  lsspropdg  13987  islidlm  14035  rspcl  14047  rspssid  14048  isbasisg  14280  tgss3  14314  restbasg  14404  tgrest  14405  restopn2  14419  cnpnei  14455  cnptopresti  14474  txbas  14494  elmopn  14682  neibl  14727  dvfgg  14924