Theorem sseq2 3194

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 3177	. . . 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 3177	. . . 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 3185	. 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 1364   C_ wss 3144

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-in 3150  df-ss 3157

This theorem is referenced by:  sseq12  3195  sseq2i  3197  sseq2d  3200  sseqtrid  3220  nssne1  3228  sseq0  3479  un00  3484  pweq  3593  ssintab  3876  ssintub  3877  intmin  3879  treq  4122  ssexg  4157  exmidundif  4224  frforeq3  4365  frirrg  4368  iunpw  4498  ordtri2orexmid  4540  ontr2exmid  4542  onsucsssucexmid  4544  ordtri2or2exmid  4588  ontri2orexmidim  4589  iotaexab  5214  fununi  5303  funcnvuni  5304  feq3  5369  ssimaexg  5599  nnawordex  6555  ereq1  6567  xpider  6633  domeng  6779  ssfiexmid  6905  fisseneq  6961  sbthlemi4  6990  sbthlemi5  6991  acfun  7237  onntri45  7271  ccfunen  7294  fprodssdc  11633  lspf  13722  lspval  13723  basis2  14025  eltg2  14030  clsval  14088  ntrcls0  14108  isnei  14121  neiint  14122  neipsm  14131  opnneissb  14132  opnssneib  14133  innei  14140  icnpimaex  14188  cnptoprest2  14217  neitx  14245  txcnp  14248  blssps  14404  blss  14405  metss  14471  metrest  14483  metcnp3  14488  bdssexg  15134  bj-nntrans  15181  bj-omtrans  15186