Theorem sseq2i 3220

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 3217	. 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 1373   C_ wss 3166

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-in 3172  df-ss 3179

This theorem is referenced by:  sseqtri  3227  sseqtrdi  3241  abss  3262  ssrab  3271  ssintrab  3908  iunpwss  4019  iotass  5249  dffun2  5281  ssimaex  5640  pw1fin  7007  pw1dc0el  7008  ss1o0el1o  7010  isstructim  12846  isstructr  12847  issubm  13304  grpissubg  13530  issubrng  13961  bj-ssom  15872  ss1oel2o  15928