Theorem sseq2d 3258

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1398   ⊆ wss 3201

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  sseq12d  3259  sseqtrd  3266  exmidsssn  4298  exmidsssnc  4299  onsucsssucexmid  4631  sbcrel  4818  funimass2  5415  fnco  5447  fnssresb  5451  fnimaeq0  5461  foimacnv  5610  fvelimab  5711  ssimaexg  5717  fvmptss2  5730  rdgss  6592  tapeq2  7515  fzowrddc  11275  swrdnd  11287  swrd0g  11288  summodclem2  12004  summodc  12005  zsumdc  12006  fsum3cvg3  12018  prodmodclem2  12199  prodmodc  12200  zproddc  12201  ennnfoneleminc  13093  tgval  13406  prdsval  13417  releqgg  13868  eqgex  13869  eqgfval  13870  opprsubgg  14159  unitsubm  14195  subrngpropd  14292  subrgsubm  14310  issubrg3  14323  subrgpropd  14329  lsslss  14457  lsspropdg  14507  islidlm  14555  rspcl  14567  rspssid  14568  isbasisg  14835  tgss3  14869  restbasg  14959  tgrest  14960  restopn2  14974  cnpnei  15010  cnptopresti  15029  txbas  15049  elmopn  15237  neibl  15282  dvfgg  15479  incistruhgr  16011  edgssv2en  16120  wksfval  16243