Theorem sseq2 2083

Description: Equality theorem for the subclass relationship.

Assertion

Ref	Expression
sseq2	|- (A = B -> (C (_ A <-> C (_ B))

Proof of Theorem sseq2

Step	Hyp	Ref	Expression
1		sstr2 2071	. . . 4 |- (C (_ A -> (A (_ B -> C (_ B))
2	1	com12 11	. . 3 |- (A (_ B -> (C (_ A -> C (_ B))
3		sstr2 2071	. . . 4 |- (C (_ B -> (B (_ A -> C (_ A))
4	3	com12 11	. . 3 |- (B (_ A -> (C (_ B -> C (_ A))
5	2, 4	anim12i 333	. 2 |- ((A (_ B /\ B (_ A) -> ((C (_ A -> C (_ B) /\ (C (_ B -> C (_ A)))
6		eqss 2077	. 2 |- (A = B <-> (A (_ B /\ B (_ A))
7		dfbi2 514	. 2 |- ((C (_ A <-> C (_ B) <-> ((C (_ A -> C (_ B) /\ (C (_ B -> C (_ A)))
8	5, 6, 7	3imtr4 219	1 |- (A = B -> (C (_ A <-> C (_ B))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 956   (_ wss 2047

This theorem is referenced by:  sseq12 2084  sseq2i 2086  sseq2d 2089  eqimss 2109  psseq2 2136  sseq0 2304  un00 2306  disjpss 2319  pweq 2403  ssuni 2522  ssintab 2550  ssintub 2551  intmin 2553  treq 2686  ssexg 2721  intabs 2733  iunpw 2914  ordunidif 3005  ordssun 3079  limomss 3137  findsg 3157  tfindsg 3162  unixp0 3518  fununi 3563  funcnvuni 3564  feq3 3622  feq23 3623  ssimaexg 3769  oawordeu 4189  oawordexr 4190  ereq 4267  domeng 4380  undom 4438  sbthlem4 4450  sbthlem5 4451  mapdom2lem 4493  php3 4515  php3OLD 4516  abfii4OLD 4564  inf3lema 4609  tz9.1 4646  scottex 4716  aceq3 4733  ac7g 4749  cardlim 4851  isinfcard 4887  alephval3 4903  cflem 4905  cfval 4906  cflecard 4912  cfsuc 4915  infxpidmlem7 7558  infxpidmlem11 7562  istopg 7596  basis2t 7615  eltg2t 7619  tgss2t 7637  basgen2t 7639  bastop 7642  ntrval 7676  clsval 7677  clscld 7683  clsval2 7685  ntrcls0 7707  isnei 7718  neiint 7719  neips 7727  opnneissb 7728  opnssneib 7729  innei 7736  islp2 7747  cnpimaex 7765  isopn 7859  metcnp 7887  tgioo 7915  resgrprn 8095  issubg 8116  avril1 8784  omls 9246  pjomlt 9269  ococint 9297  spanvalt 9299  hsupval2t 9300  spanclt 9304  chsupsn 9312  shlubt 9354  shsumval2 9360  shs00 9373  chj00 9410  chsscon3t 9423  chlejb1t 9435  chnlet 9437  pjoml2t 9554  pjoml3t 9555  lecmt 9560  stcltr1 10201  mdbrt 10221  dmdmdt 10227  dmdit 10229  dmdbr3 10232  dmdbr4 10233  mdsl1 10248  mdslmd1lem3 10254  mdslmd1lem4 10255  csmdsym 10261  hatomict 10287  chrelat2t 10297  atordt 10315  atcvat4 10324  fiv 10482  fivOLD 10483  iseuctopg 10502  mapdiscn 10511  isfil 10558  fillsb 10560  neifil 10568  fgsb 10570  fgsbOLD 10571  efilcp 10572  efilcpOLD 10573  fgsb2 10580  efilcp2 10581  efilcp2OLD 10582  limfillem1OLD 10607  isalg 10653  algi 10660

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-in 2051  df-ss 2053

Copyright terms: Public domain