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  4285  exmidsssnc  4286  onsucsssucexmid  4616  sbcrel  4802  funimass2  5395  fnco  5427  fnssresb  5431  fnimaeq0  5441  foimacnv  5586  fvelimab  5683  ssimaexg  5689  fvmptss2  5702  rdgss  6519  tapeq2  7427  fzowrddc  11165  swrdnd  11177  swrd0g  11178  summodclem2  11879  summodc  11880  zsumdc  11881  fsum3cvg3  11893  prodmodclem2  12074  prodmodc  12075  zproddc  12076  ennnfoneleminc  12968  tgval  13281  prdsval  13292  releqgg  13743  eqgex  13744  eqgfval  13745  opprsubgg  14033  unitsubm  14068  subrngpropd  14165  subrgsubm  14183  issubrg3  14196  subrgpropd  14202  lsslss  14330  lsspropdg  14380  islidlm  14428  rspcl  14440  rspssid  14441  isbasisg  14703  tgss3  14737  restbasg  14827  tgrest  14828  restopn2  14842  cnpnei  14878  cnptopresti  14897  txbas  14917  elmopn  15105  neibl  15150  dvfgg  15347  incistruhgr  15875  edgssv2en  15982