Theorem sseq2 3225

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 3208	. . . 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 3208	. . . 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 3216	. 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 3174

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-in 3180  df-ss 3187

This theorem is referenced by:  sseq12  3226  sseq2i  3228  sseq2d  3231  sseqtrid  3251  nssne1  3259  sseq0  3510  un00  3515  pweq  3629  ssintab  3916  ssintub  3917  intmin  3919  treq  4164  ssexg  4199  exmidundif  4266  frforeq3  4412  frirrg  4415  iunpw  4545  ordtri2orexmid  4589  ontr2exmid  4591  onsucsssucexmid  4593  ordtri2or2exmid  4637  ontri2orexmidim  4638  iotaexab  5269  fununi  5361  funcnvuni  5362  feq3  5430  ssimaexg  5664  nnawordex  6638  ereq1  6650  xpider  6716  domeng  6864  ssfiexmid  6999  fisseneq  7057  sbthlemi4  7088  sbthlemi5  7089  nninfninc  7251  acfun  7350  onntri45  7387  ccfunen  7411  fprodssdc  12016  lspf  14266  lspval  14267  basis2  14635  eltg2  14640  clsval  14698  ntrcls0  14718  isnei  14731  neiint  14732  neipsm  14741  opnneissb  14742  opnssneib  14743  innei  14750  icnpimaex  14798  cnptoprest2  14827  neitx  14855  txcnp  14858  blssps  15014  blss  15015  metss  15081  metrest  15093  metcnp3  15098  upgredgpr  15853  bdssexg  16039  bj-nntrans  16086  bj-omtrans  16091