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  4149  ssexg  4184  exmidundif  4251  frforeq3  4395  frirrg  4398  iunpw  4528  ordtri2orexmid  4572  ontr2exmid  4574  onsucsssucexmid  4576  ordtri2or2exmid  4620  ontri2orexmidim  4621  iotaexab  5251  fununi  5343  funcnvuni  5344  feq3  5412  ssimaexg  5643  nnawordex  6617  ereq1  6629  xpider  6695  domeng  6843  ssfiexmid  6975  fisseneq  7033  sbthlemi4  7064  sbthlemi5  7065  nninfninc  7227  acfun  7321  onntri45  7355  ccfunen  7378  fprodssdc  11934  lspf  14184  lspval  14185  basis2  14553  eltg2  14558  clsval  14616  ntrcls0  14636  isnei  14649  neiint  14650  neipsm  14659  opnneissb  14660  opnssneib  14661  innei  14668  icnpimaex  14716  cnptoprest2  14745  neitx  14773  txcnp  14776  blssps  14932  blss  14933  metss  14999  metrest  15011  metcnp3  15016  bdssexg  15877  bj-nntrans  15924  bj-omtrans  15929