Theorem sseq2d 3183

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1353   ⊆ wss 3127

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 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-11 1504  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-in 3133  df-ss 3140

This theorem is referenced by:  sseq12d  3184  sseqtrd  3191  exmidsssn  4197  exmidsssnc  4198  onsucsssucexmid  4520  sbcrel  4706  funimass2  5286  fnco  5316  fnssresb  5320  fnimaeq0  5329  foimacnv  5471  fvelimab  5564  ssimaexg  5570  fvmptss2  5583  rdgss  6374  summodclem2  11356  summodc  11357  zsumdc  11358  fsum3cvg3  11370  prodmodclem2  11551  prodmodc  11552  zproddc  11553  ennnfoneleminc  12377  isbasisg  13093  tgval  13100  tgss3  13129  restbasg  13219  tgrest  13220  restopn2  13234  cnpnei  13270  cnptopresti  13289  txbas  13309  elmopn  13497  neibl  13542  dvfgg  13708