Theorem sseq2 3181

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 3164	. . . 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 3164	. . . 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 3172	. 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 1353   C_ wss 3131

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3137  df-ss 3144

This theorem is referenced by:  sseq12  3182  sseq2i  3184  sseq2d  3187  sseqtrid  3207  nssne1  3215  sseq0  3466  un00  3471  pweq  3580  ssintab  3863  ssintub  3864  intmin  3866  treq  4109  ssexg  4144  exmidundif  4208  frforeq3  4349  frirrg  4352  iunpw  4482  ordtri2orexmid  4524  ontr2exmid  4526  onsucsssucexmid  4528  ordtri2or2exmid  4572  ontri2orexmidim  4573  fununi  5286  funcnvuni  5287  feq3  5352  ssimaexg  5580  nnawordex  6532  ereq1  6544  xpider  6608  domeng  6754  ssfiexmid  6878  fisseneq  6933  sbthlemi4  6961  sbthlemi5  6962  acfun  7208  onntri45  7242  ccfunen  7265  fprodssdc  11600  lspf  13481  lspval  13482  basis2  13633  eltg2  13638  clsval  13696  ntrcls0  13716  isnei  13729  neiint  13730  neipsm  13739  opnneissb  13740  opnssneib  13741  innei  13748  icnpimaex  13796  cnptoprest2  13825  neitx  13853  txcnp  13856  blssps  14012  blss  14013  metss  14079  metrest  14091  metcnp3  14096  bdssexg  14741  bj-nntrans  14788  bj-omtrans  14793