Theorem sseq2 3217

Description: Equality theorem for the subclass relationship. (Contributed by NM, 25-Jun-1998.)

Assertion

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

Proof of Theorem sseq2

Step	Hyp	Ref	Expression
1		sstr2 3200	. . . 4 |- ( C C_ A -> ( A C_ B -> C C_ B ) )
2	1	com12 30	. . 3 |- ( A C_ B -> ( C C_ A -> C C_ B ) )
3		sstr2 3200	. . . 4 |- ( C C_ B -> ( B C_ A -> C C_ A ) )
4	3	com12 30	. . 3 |- ( B C_ A -> ( C C_ B -> C C_ A ) )
5	2, 4	anim12i 338	. 2 |- ( ( A C_ B /\ B C_ A ) -> ( ( C C_ A -> C C_ B ) /\ ( C C_ B -> C C_ A ) ) )
6		eqss 3208	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
7		dfbi2 388	. 2 |- ( ( C C_ A <-> C C_ B ) <-> ( ( C C_ A -> C C_ B ) /\ ( C C_ B -> C C_ A ) ) )
8	5, 6, 7	3imtr4i 201	1 |- ( A = B -> ( C C_ A <-> C C_ B ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> 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:  sseq12  3218  sseq2i  3220  sseq2d  3223  sseqtrid  3243  nssne1  3251  sseq0  3502  un00  3507  pweq  3619  ssintab  3902  ssintub  3903  intmin  3905  treq  4148  ssexg  4183  exmidundif  4250  frforeq3  4394  frirrg  4397  iunpw  4527  ordtri2orexmid  4571  ontr2exmid  4573  onsucsssucexmid  4575  ordtri2or2exmid  4619  ontri2orexmidim  4620  iotaexab  5250  fununi  5342  funcnvuni  5343  feq3  5410  ssimaexg  5641  nnawordex  6615  ereq1  6627  xpider  6693  domeng  6841  ssfiexmid  6973  fisseneq  7031  sbthlemi4  7062  sbthlemi5  7063  nninfninc  7225  acfun  7319  onntri45  7353  ccfunen  7376  fprodssdc  11901  lspf  14151  lspval  14152  basis2  14520  eltg2  14525  clsval  14583  ntrcls0  14603  isnei  14616  neiint  14617  neipsm  14626  opnneissb  14627  opnssneib  14628  innei  14635  icnpimaex  14683  cnptoprest2  14712  neitx  14740  txcnp  14743  blssps  14899  blss  14900  metss  14966  metrest  14978  metcnp3  14983  bdssexg  15840  bj-nntrans  15887  bj-omtrans  15892