Theorem sseq2 2079

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 2067	. . . 4 |- (C (_ A -> (A (_ B -> C (_ B))
2	1	com12 11	. . 3 |- (A (_ B -> (C (_ A -> C (_ B))
3		sstr2 2067	. . . 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 2073	. 2 |- (A = B <-> (A (_ B /\ B (_ A))
7		bi 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 954   (_ wss 2043

This theorem is referenced by:  sseq12 2080  sseq2i 2082  sseq2d 2085  eqimss 2105  psseq2 2132  sseq0 2300  un00 2302  disjpss 2315  pweq 2399  ssuni 2517  ssintab 2545  ssintub 2546  intmin 2548  treq 2681  ssexg 2716  intabs 2728  iunpw 2909  ordunidif 3000  ordssun 3074  limomss 3132  findsg 3152  tfindsg 3157  unixp0 3510  fununi 3555  funcnvuni 3556  feq3 3614  feq23 3615  ssimaexg 3760  oawordeu 4179  oawordexr 4180  ereq 4257  domeng 4368  undom 4424  sbthlem4 4436  sbthlem5 4437  mapdom2lem 4479  php3 4501  abfii4 4544  inf3lema 4589  tz9.1 4626  scottex 4696  aceq3 4713  ac7g 4729  cardlim 4831  isinfcard 4867  alephval3 4883  cflem 4885  cfval 4886  cflecard 4892  cfsuc 4895  infxpidmlem7 7509  infxpidmlem11 7513  istopg 7546  basis2t 7565  eltg2t 7569  tgss2t 7587  basgen2t 7589  bastop 7592  ntrval 7626  clsval 7627  clscld 7633  clsval2 7635  ntrcls0 7657  isnei 7668  neiint 7669  neips 7677  opnneissb 7678  opnssneib 7679  innei 7686  islp2 7697  cnpimaex 7715  isopn 7811  metcnp 7839  tgioo 7867  resgrprn 8045  issubg 8068  avril1 8723  omls 9184  pjomlt 9207  ococint 9235  spanvalt 9237  hsupval2t 9238  spanclt 9242  chsupsn 9250  shlubt 9292  shsumval2 9298  shs00 9311  chj00 9348  chsscon3t 9361  chlejb1t 9373  chnlet 9375  pjoml2t 9494  pjoml3t 9495  lecmt 9500  stcltr1 10139  mdbrt 10159  dmdmdt 10165  dmdit 10167  dmdbr3 10170  dmdbr4 10171  mdsl1 10185  mdslmd1lem3 10191  mdslmd1lem4 10192  csmdsym 10198  hatomict 10224  chrelat2t 10234  atordt 10252  atcvat4 10261  fiv 10410  iseuctopg 10425  mapdiscn 10434  isfil 10469  fillsb 10471  neifil 10478  fgsb 10480  efilcp 10481  fgsb2 10485  efilcp2 10486  isalg 10533  algi 10540

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-in 2047  df-ss 2049

Copyright terms: Public domain