Theorem sseq2i 3251

Description: An equality inference for the subclass relationship. (Contributed by NM, 30-Aug-1993.)

Hypothesis

Ref	Expression
sseq1i.1	|- A = B

Assertion

Ref	Expression
sseq2i	|- ( C C_ A <-> C C_ B )

Proof of Theorem sseq2i

Step	Hyp	Ref	Expression
1		sseq1i.1	. 2 |- A = B
2		sseq2 3248	. 2 |- ( A = B -> ( C C_ A <-> C C_ B ) )
3	1, 2	ax-mp 5	1 |- ( C C_ A <-> C C_ B )

Syntax hints:   <-> wb 105   = wceq 1395   C_ 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:  sseqtri  3258  sseqtrdi  3272  abss  3293  ssrab  3302  ssintrab  3946  iunpwss  4057  iotass  5296  dffun2  5328  ssimaex  5695  pw1fin  7072  pw1dc0el  7073  ss1o0el1o  7075  isstructim  13046  isstructr  13047  issubm  13505  grpissubg  13731  issubrng  14163  umgredg  15943  bj-ssom  16299  ss1oel2o  16355