Theorem sseq2d 3154

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1332   ⊆ wss 3098

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-11 1483  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-ext 2136

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1740  df-clab 2141  df-cleq 2147  df-clel 2150  df-in 3104  df-ss 3111

This theorem is referenced by:  sseq12d  3155  sseqtrd  3162  exmidsssn  4158  exmidsssnc  4159  onsucsssucexmid  4480  sbcrel  4665  funimass2  5241  fnco  5271  fnssresb  5275  fnimaeq0  5284  foimacnv  5425  fvelimab  5517  ssimaexg  5523  fvmptss2  5536  rdgss  6320  summodclem2  11256  summodc  11257  zsumdc  11258  fsum3cvg3  11270  prodmodclem2  11451  prodmodc  11452  zproddc  11453  ennnfoneleminc  12091  isbasisg  12381  tgval  12388  tgss3  12417  restbasg  12507  tgrest  12508  restopn2  12522  cnpnei  12558  cnptopresti  12577  txbas  12597  elmopn  12785  neibl  12830  dvfgg  12996