Theorem sseq2d 3225

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1373   ⊆ wss 3168

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-in 3174  df-ss 3181

This theorem is referenced by:  sseq12d  3226  sseqtrd  3233  exmidsssn  4251  exmidsssnc  4252  onsucsssucexmid  4580  sbcrel  4766  funimass2  5358  fnco  5390  fnssresb  5394  fnimaeq0  5404  foimacnv  5549  fvelimab  5645  ssimaexg  5651  fvmptss2  5664  rdgss  6479  tapeq2  7378  fzowrddc  11114  swrdnd  11126  swrd0g  11127  summodclem2  11743  summodc  11744  zsumdc  11745  fsum3cvg3  11757  prodmodclem2  11938  prodmodc  11939  zproddc  11940  ennnfoneleminc  12832  tgval  13144  prdsval  13155  releqgg  13606  eqgex  13607  eqgfval  13608  opprsubgg  13896  unitsubm  13931  subrngpropd  14028  subrgsubm  14046  issubrg3  14059  subrgpropd  14065  lsslss  14193  lsspropdg  14243  islidlm  14291  rspcl  14303  rspssid  14304  isbasisg  14566  tgss3  14600  restbasg  14690  tgrest  14691  restopn2  14705  cnpnei  14741  cnptopresti  14760  txbas  14780  elmopn  14968  neibl  15013  dvfgg  15210  incistruhgr  15736