Theorem sseq2 3272

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 3255	. . . 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 3255	. . . 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 3263	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
7		dfbi2 392	. 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 1402   C_ wss 3220

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is referenced by:  sseq12  3273  sseq2i  3275  sseq2d  3278  sseqtrid  3298  nssne1  3306  sseq0  3564  un00  3566  pweq  3688  ssintab  3982  ssintub  3983  intmin  3985  treq  4230  ssexg  4267  exmidundif  4338  frforeq3  4487  frirrg  4490  iunpw  4621  ordtri2orexmid  4665  ontr2exmid  4667  onsucsssucexmid  4669  ordtri2or2exmid  4713  ontri2orexmidim  4714  iotaexab  5351  fununi  5444  funcnvuni  5445  feq3  5513  ssimaexg  5759  nnawordex  6792  ereq1  6804  xpider  6870  domeng  7026  ssfiexmid  7168  ssfiexmidt  7170  fisseneq  7232  sbthlemi4  7267  sbthlemi5  7268  nninfninc  7453  acfun  7553  onntri45  7590  ccfunen  7620  fprodssdc  12335  lspf  14698  lspval  14699  basis2  15072  eltg2  15077  clsval  15135  ntrcls0  15155  isnei  15168  neiint  15169  neipsm  15178  opnneissb  15179  opnssneib  15180  innei  15187  icnpimaex  15235  cnptoprest2  15264  neitx  15292  txcnp  15295  blssps  15451  blss  15452  metss  15518  metrest  15530  metcnp3  15535  upgredgpr  16304  wlkvtxiedg  16500  wlkvtxiedgg  16501  wlkres  16534  bdssexg  16844  bj-nntrans  16891  bj-omtrans  16896