Theorem sseq2 3207

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 3190	. . . 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 3190	. . . 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 3198	. 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 3157

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170

This theorem is referenced by:  sseq12  3208  sseq2i  3210  sseq2d  3213  sseqtrid  3233  nssne1  3241  sseq0  3492  un00  3497  pweq  3608  ssintab  3891  ssintub  3892  intmin  3894  treq  4137  ssexg  4172  exmidundif  4239  frforeq3  4382  frirrg  4385  iunpw  4515  ordtri2orexmid  4559  ontr2exmid  4561  onsucsssucexmid  4563  ordtri2or2exmid  4607  ontri2orexmidim  4608  iotaexab  5237  fununi  5326  funcnvuni  5327  feq3  5392  ssimaexg  5623  nnawordex  6587  ereq1  6599  xpider  6665  domeng  6811  ssfiexmid  6937  fisseneq  6995  sbthlemi4  7026  sbthlemi5  7027  nninfninc  7189  acfun  7274  onntri45  7308  ccfunen  7331  fprodssdc  11755  lspf  13945  lspval  13946  basis2  14284  eltg2  14289  clsval  14347  ntrcls0  14367  isnei  14380  neiint  14381  neipsm  14390  opnneissb  14391  opnssneib  14392  innei  14399  icnpimaex  14447  cnptoprest2  14476  neitx  14504  txcnp  14507  blssps  14663  blss  14664  metss  14730  metrest  14742  metcnp3  14747  bdssexg  15550  bj-nntrans  15597  bj-omtrans  15602