Theorem sseq2d 3254

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1395   ⊆ wss 3197

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  sseq12d  3255  sseqtrd  3262  exmidsssn  4286  exmidsssnc  4287  onsucsssucexmid  4619  sbcrel  4805  funimass2  5399  fnco  5431  fnssresb  5435  fnimaeq0  5445  foimacnv  5592  fvelimab  5692  ssimaexg  5698  fvmptss2  5711  rdgss  6535  tapeq2  7447  fzowrddc  11187  swrdnd  11199  swrd0g  11200  summodclem2  11901  summodc  11902  zsumdc  11903  fsum3cvg3  11915  prodmodclem2  12096  prodmodc  12097  zproddc  12098  ennnfoneleminc  12990  tgval  13303  prdsval  13314  releqgg  13765  eqgex  13766  eqgfval  13767  opprsubgg  14055  unitsubm  14091  subrngpropd  14188  subrgsubm  14206  issubrg3  14219  subrgpropd  14225  lsslss  14353  lsspropdg  14403  islidlm  14451  rspcl  14463  rspssid  14464  isbasisg  14726  tgss3  14760  restbasg  14850  tgrest  14851  restopn2  14865  cnpnei  14901  cnptopresti  14920  txbas  14940  elmopn  15128  neibl  15173  dvfgg  15370  incistruhgr  15898  edgssv2en  16005  wksfval  16043