Theorem sseq2 3851

Description: Equality theorem for the subclass relationship. (Contributed by NM, 25-Jun-1998.)

Assertion

Ref	Expression
sseq2	⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))

Proof of Theorem sseq2

Step	Hyp	Ref	Expression
1		sstr2 3833	. . . 4 ⊢ (𝐶 ⊆ 𝐴 → (𝐴 ⊆ 𝐵 → 𝐶 ⊆ 𝐵))
2	1	com12 32	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵))
3		sstr2 3833	. . . 4 ⊢ (𝐶 ⊆ 𝐵 → (𝐵 ⊆ 𝐴 → 𝐶 ⊆ 𝐴))
4	3	com12 32	. . 3 ⊢ (𝐵 ⊆ 𝐴 → (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴))
5	2, 4	anim12i 608	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → ((𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵) ∧ (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴)))
6		eqss 3841	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
7		dfbi2 468	. 2 ⊢ ((𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵) ↔ ((𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵) ∧ (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴)))
8	5, 6, 7	3imtr4i 284	1 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   = wceq 1658   ⊆ wss 3797

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2802

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2811  df-cleq 2817  df-clel 2820  df-in 3804  df-ss 3811

This theorem is referenced by:  sseq12  3852  sseq2i  3854  sseq2d  3857  syl5sseq  3877  nssne1  3885  psseq2  3920  sseq0  4199  un00  4235  disjpss  4251  pweq  4380  ssintab  4713  ssintub  4714  intmin  4716  treq  4980  al0ssb  5014  sseliALT  5015  ssexg  5028  intabs  5046  iunopeqop  5206  ordunidif  6010  ordssun  6061  fununi  6196  feq3  6260  ssimaexg  6510  iunpw  7238  tfindsg  7320  limomss  7330  findsg  7353  funcnvuni  7380  frxp  7550  wrecseq123  7672  wfrlem1  7678  wfrlem4  7682  wfrlem4OLD  7683  wfrlem15  7694  onfununi  7703  oawordeu  7901  oawordexr  7902  nnawordex  7983  ereq1  8015  xpider  8082  domeng  8235  sbthlem4  8341  sbthlem5  8342  domssex  8389  finsschain  8541  dffi2  8597  dffi3  8605  hartogslem1  8715  inf3lema  8797  cantnflem1  8862  tz9.1  8881  tz9.1c  8882  tctr  8892  tcmin  8893  tcrank  9023  scottex  9024  cardlim  9110  infxpenlem  9148  infxpenc2  9157  isinfcard  9227  alephinit  9230  alephval3  9245  dfac3  9256  cflem  9382  cfval  9383  cflecard  9389  cfsuc  9393  cff1  9394  cfflb  9395  cflim2  9399  isf32lem2  9490  fin1a2lem13  9548  ac7g  9610  ttukeylem5  9649  ttukeylem7  9651  pwcfsdom  9719  pwfseqlem5  9799  pwfseq  9800  gch2  9811  winalim  9831  wunex  9875  wuncss  9881  eltskg  9886  eltsk2g  9887  gruina  9954  grur1a  9955  axgroth6  9964  swrdnd2  13719  trcleq2lem  14108  dfrtrcl2  14178  fprodss  15050  mrcflem  16618  mrcval  16622  isacs2  16665  acsfiel  16666  ipoval  17506  fpwipodrs  17516  ipodrsima  17517  mreclatBAD  17539  slwispgp  18376  pgpssslw  18379  lsmss1b  18430  lsmss2b  18432  cntzcmnss  18598  gsumzres  18662  lspf  19332  lspval  19333  lbsextlem1  19518  lbsextlem3  19520  lbsextlem4  19521  aspval  19688  mplsubglem  19794  mpllsslem  19795  basis2  21125  eltg2  21132  clsval  21211  clscld  21221  clsval2  21224  ntrcls0  21250  isnei  21277  neiint  21278  neips  21287  opnneissb  21288  opnssneib  21289  neindisj2  21297  innei  21299  neiptoptop  21305  neiptopnei  21306  neitr  21354  restcls  21355  cnpimaex  21430  cnprest2  21464  regsep  21508  nrmsep3  21529  nrmsep  21531  regsep2  21550  tgcmp  21574  uncmp  21576  bwth  21583  1stcfb  21618  1stcrest  21626  2ndcctbss  21628  1stcelcls  21634  lly1stc  21669  ssref  21685  refref  21686  comppfsc  21705  xkoopn  21762  neitx  21780  txcnp  21793  txcmplem1  21814  kqnrmlem1  21916  kqnrmlem2  21917  nrmhmph  21967  fbssfi  22010  opnfbas  22015  fbasfip  22041  fbunfip  22042  fgss2  22047  fgcl  22051  supfil  22068  isufil2  22081  filssufilg  22084  ssufl  22091  ufileu  22092  elfm3  22123  fmfnfm  22131  ufldom  22135  fbflim2  22150  flfneii  22165  flftg  22169  txflf  22179  supnfcls  22193  fclscf  22198  fclsfnflim  22200  flimfnfcls  22201  alexsubALTlem2  22221  alexsubALTlem3  22222  alexsubALTlem4  22223  alexsubALT  22224  tsmsfbas  22300  tsmsres  22316  tsmsf1o  22317  tsmsxplem1  22325  tsmsxp  22327  ustssel  22378  ustincl  22380  ustdiag  22381  ustinvel  22382  ustexhalf  22383  ust0  22392  elutop  22406  ustuqtop4  22417  cfiluexsm  22463  cfiluweak  22468  blssps  22598  blss  22599  metss  22682  metrest  22698  metcnp3  22714  metnrmlem3  23033  lebnumlem3  23131  lebnum  23132  ellimc3  24041  lhop1lem  24174  dchrelbas  25373  upgredgpr  26440  dfnbgr3  26634  nbupgr  26640  nbumgrvtx  26642  nbgr2vtx1edg  26646  nbuhgr2vtx1edgb  26648  cusgrexilem2  26739  wlkvtxiedg  26921  wlkres  26968  wlkresOLD  26970  upgr1wlkdlem2  27521  1pthon2v  27528  1pthon2ve  27529  cusconngr  27566  avril1  27876  spanval  28746  spancl  28749  shsval2i  28800  omlsi  28817  ococin  28821  chsupsn  28826  pjoml  28849  shs00i  28863  chj00i  28900  chsscon3  28913  chlejb1  28925  chnle  28927  pjoml2  29024  pjoml3  29025  lecm  29030  stcltr1i  29687  mdbr  29707  dmdmd  29713  dmdi  29715  dmdbr3  29718  dmdbr4  29719  mdsl1i  29734  mdslmd1lem3  29740  mdslmd1lem4  29741  csmdsymi  29747  hatomic  29773  chrelat2  29783  atord  29801  atcvat4i  29810  fz1nntr  30107  reff  30450  cmpcref  30461  sigagenval  30747  dmsigagen  30751  sigagenss  30756  ldsysgenld  30767  ldgenpisyslem1  30770  ldgenpisyslem2  30771  dynkin  30774  carsgmon  30920  carsgclctunlem2  30925  bnj1286  31632  bnj1452  31665  kur14lem9  31741  mclsssvlem  32004  mclsind  32012  frrlem1  32318  scutun12  32455  imagesset  32598  altopthsn  32606  fnessref  32889  refssfne  32890  topjoin  32897  neifg  32903  bj-snglex  33482  relowlssretop  33755  relowlpssretop  33756  finxpreclem3  33774  poimirlem29  33981  poimir  33985  mblfinlem3  33991  totbndss  34117  heibor1lem  34149  unichnidl  34371  ispridl  34374  maxidlmax  34383  igenval  34401  igenidl  34403  igenmin  34404  igenval2  34406  brssr  34798  lsatcmp  35077  lcvexchlem4  35111  lcvexchlem5  35112  pclvalN  35964  pclclN  35965  elpcliN  35967  docaclN  37198  dihglb2  37416  doch2val2  37438  dochocss  37440  dochexmidlem7  37540  lpolconN  37561  mapdval  37702  nacsfix  38118  mzpcompact2  38158  rgspnval  38580  rgspncl  38581  rgspnmin  38583  superficl  38712  superuncl  38713  cleq2lem  38754  clcnvlem  38770  dfrtrcl3  38865  clsk1indlem2  39179  neik0pk1imk0  39184  isotone1  39185  isotone2  39186  ntrclsiso  39204  gneispacess2  39283  ssrecnpr  39346  founiiun  40168  founiiun0  40184  islptre  40645  salgenval  41331  salgenn0  41339  salgencl  41340  sssalgen  41343  salgenss  41344  salgenuni  41345  issalgend  41346  dfsalgen2  41349  salgencntex  41351  isomgreqve  42542  setrec1lem1  43328  setrec1lem3  43330  setrec2fun  43333