Theorem sseq2 3249

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 3232	. . . 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 3232	. . . 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 3240	. 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 1395   C_ wss 3198

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3204  df-ss 3211

This theorem is referenced by:  sseq12  3250  sseq2i  3252  sseq2d  3255  sseqtrid  3275  nssne1  3283  sseq0  3534  un00  3539  pweq  3653  ssintab  3943  ssintub  3944  intmin  3946  treq  4191  ssexg  4226  exmidundif  4294  frforeq3  4442  frirrg  4445  iunpw  4575  ordtri2orexmid  4619  ontr2exmid  4621  onsucsssucexmid  4623  ordtri2or2exmid  4667  ontri2orexmidim  4668  iotaexab  5303  fununi  5395  funcnvuni  5396  feq3  5464  ssimaexg  5704  nnawordex  6692  ereq1  6704  xpider  6770  domeng  6918  ssfiexmid  7058  fisseneq  7119  sbthlemi4  7150  sbthlemi5  7151  nninfninc  7313  acfun  7412  onntri45  7449  ccfunen  7473  fprodssdc  12141  lspf  14393  lspval  14394  basis2  14762  eltg2  14767  clsval  14825  ntrcls0  14845  isnei  14858  neiint  14859  neipsm  14868  opnneissb  14869  opnssneib  14870  innei  14877  icnpimaex  14925  cnptoprest2  14954  neitx  14982  txcnp  14985  blssps  15141  blss  15142  metss  15208  metrest  15220  metcnp3  15225  upgredgpr  15988  wlkvtxiedg  16142  wlkvtxiedgg  16143  wlkres  16174  bdssexg  16435  bj-nntrans  16482  bj-omtrans  16487