Theorem sseq2 4000

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 3981	. . . 4 ⊢ (𝐶 ⊆ 𝐴 → (𝐴 ⊆ 𝐵 → 𝐶 ⊆ 𝐵))
2	1	com12 32	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵))
3		sstr2 3981	. . . 4 ⊢ (𝐶 ⊆ 𝐵 → (𝐵 ⊆ 𝐴 → 𝐶 ⊆ 𝐴))
4	3	com12 32	. . 3 ⊢ (𝐵 ⊆ 𝐴 → (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴))
5	2, 4	anim12i 612	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → ((𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵) ∧ (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴)))
6		eqss 3989	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
7		dfbi2 474	. 2 ⊢ ((𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵) ↔ ((𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵) ∧ (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴)))
8	5, 6, 7	3imtr4i 292	1 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1533   ⊆ wss 3940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-v 3468  df-in 3947  df-ss 3957

This theorem is referenced by:  sseq12  4001  sseq2i  4003  sseq2d  4006  nssne1  4036  psseq2  4080  sseq0  4391  un00  4434  disjpss  4452  pweqALT  4609  ssintab  4959  ssintub  4960  intmin  4962  treq  5263  al0ssb  5298  sseliALT  5299  ssexg  5313  intabs  5332  iunopeqop  5511  onelssex  6402  ordunidif  6403  ordssun  6456  fununi  6613  feq3  6690  ssimaexg  6967  fnssintima  7351  iunpw  7751  tfindsg  7843  limomss  7853  findsg  7883  funcnvuni  7915  frxp  8106  frrlem1  8266  frrlem13  8278  wrecseq123OLD  8295  wfrlem1OLD  8303  wfrlem4OLD  8307  wfrlem15OLD  8318  onfununi  8336  oawordeu  8550  oawordexr  8551  nnawordex  8632  eldifsucnn  8659  coflton  8666  cofon1  8667  cofon2  8668  cofonr  8669  naddcllem  8671  naddunif  8688  ereq1  8706  xpider  8778  domeng  8954  sbthlem4  9082  sbthlem5  9083  domssex  9134  ssfi  9169  finsschain  9355  dffi2  9414  dffi3  9422  hartogslem1  9533  inf3lema  9615  cantnflem1  9680  dfttrcl2  9715  tz9.1  9720  tz9.1c  9721  tctr  9731  tcmin  9732  tcrank  9875  scottex  9876  cardlim  9963  infxpenlem  10004  infxpenc2  10013  isinfcard  10083  alephinit  10086  alephval3  10101  dfac3  10112  cflem  10237  cfval  10238  cflecard  10244  cfsuc  10248  cff1  10249  cfflb  10250  cflim2  10254  isf32lem2  10345  fin1a2lem13  10403  ac7g  10465  ttukeylem5  10504  ttukeylem7  10506  pwcfsdom  10574  pwfseqlem5  10654  pwfseq  10655  gch2  10666  winalim  10686  wunex  10730  wuncss  10736  eltskg  10741  eltsk2g  10742  gruina  10809  grur1a  10810  axgroth6  10819  swrdnd2  14602  trcleq2lem  14935  dfrtrcl2  15006  fprodss  15889  mrcflem  17549  mrcval  17553  isacs2  17596  acsfiel  17597  ipoval  18485  fpwipodrs  18495  ipodrsima  18496  mreclatBAD  18518  slwispgp  19521  pgpssslw  19524  lsmss1b  19576  lsmss2b  19578  cntzcmnss  19751  gsumzres  19819  lspf  20811  lspval  20812  lbsextlem1  20999  lbsextlem3  21001  lbsextlem4  21002  aspval  21735  mplsubglem  21868  mpllsslem  21869  basis2  22776  eltg2  22783  clsval  22863  clscld  22873  clsval2  22876  ntrcls0  22902  isnei  22929  neiint  22930  neips  22939  opnneissb  22940  opnssneib  22941  neindisj2  22949  innei  22951  neiptoptop  22957  neiptopnei  22958  neitr  23006  restcls  23007  cnpimaex  23082  cnprest2  23116  regsep  23160  nrmsep3  23181  nrmsep  23183  regsep2  23202  tgcmp  23227  uncmp  23229  bwth  23236  1stcfb  23271  1stcrest  23279  2ndcctbss  23281  1stcelcls  23287  lly1stc  23322  ssref  23338  refref  23339  comppfsc  23358  xkoopn  23415  neitx  23433  txcnp  23446  txcmplem1  23467  kqnrmlem1  23569  kqnrmlem2  23570  nrmhmph  23620  fbssfi  23663  opnfbas  23668  fbasfip  23694  fbunfip  23695  fgss2  23700  fgcl  23704  supfil  23721  isufil2  23734  filssufilg  23737  ssufl  23744  ufileu  23745  elfm3  23776  fmfnfm  23784  ufldom  23788  fbflim2  23803  flfneii  23818  flftg  23822  txflf  23832  supnfcls  23846  fclscf  23851  fclsfnflim  23853  flimfnfcls  23854  alexsubALTlem2  23874  alexsubALTlem3  23875  alexsubALTlem4  23876  alexsubALT  23877  tsmsfbas  23954  tsmsres  23970  tsmsf1o  23971  tsmsxplem1  23979  tsmsxp  23981  ustssel  24032  ustincl  24034  ustdiag  24035  ustinvel  24036  ustexhalf  24037  ust0  24046  elutop  24060  ustuqtop4  24071  cfiluexsm  24117  cfiluweak  24122  blssps  24252  blss  24253  metss  24339  metrest  24355  metcnp3  24371  metnrmlem3  24699  lebnumlem3  24811  lebnum  24812  ellimc3  25730  lhop1lem  25868  dchrelbas  27085  eqscut2  27655  scutun12  27659  madebdayim  27730  madebday  27742  upgredgpr  28871  dfnbgr3  29064  nbupgr  29070  nbumgrvtx  29072  nbgr2vtx1edg  29076  nbuhgr2vtx1edgb  29078  cusgrexilem2  29168  wlkvtxiedg  29351  wlkres  29396  upgr1wlkdlem2  29868  1pthon2v  29875  1pthon2ve  29876  cusconngr  29913  isfrgr  29982  avril1  30185  spanval  31055  spancl  31058  shsval2i  31109  omlsi  31126  ococin  31130  chsupsn  31135  pjoml  31158  shs00i  31172  chj00i  31209  chsscon3  31222  chlejb1  31234  chnle  31236  pjoml2  31333  pjoml3  31334  lecm  31339  stcltr1i  31996  mdbr  32016  dmdmd  32022  dmdi  32024  dmdbr3  32027  dmdbr4  32028  mdsl1i  32043  mdslmd1lem3  32049  mdslmd1lem4  32050  csmdsymi  32056  hatomic  32082  chrelat2  32092  atord  32110  atcvat4i  32119  fz1nntr  32484  fldgenval  32868  fldgensdrg  32870  fldgenssv  32871  fldgenssp  32874  nsgmgc  32992  nsgqusf1olem2  32994  isprmidl  33025  mxidlmax  33050  ssmxidllem  33058  ssmxidl  33059  reff  33308  cmpcref  33319  zarcls1  33338  zarclsiin  33340  zarclssn  33342  zart0  33348  zarmxt1  33349  zarcmp  33351  rhmpreimacnlem  33353  sigagenval  33627  dmsigagen  33631  sigagenss  33636  ldsysgenld  33647  ldgenpisyslem1  33650  ldgenpisyslem2  33651  dynkin  33654  carsgmon  33802  carsgclctunlem2  33807  bnj1286  34519  bnj1452  34552  fineqvac  34586  kur14lem9  34694  mclsssvlem  35042  mclsind  35050  imagesset  35420  altopthsn  35428  fnessref  35732  refssfne  35733  topjoin  35740  neifg  35746  bj-snglex  36344  bj-imdirvallem  36551  relowlssretop  36734  relowlpssretop  36735  exrecfnlem  36750  finxpreclem3  36764  pibt2  36788  poimirlem29  37007  poimir  37011  mblfinlem3  37017  totbndss  37135  heibor1lem  37167  unichnidl  37389  ispridl  37392  maxidlmax  37401  igenval  37419  igenidl  37421  igenmin  37422  igenval2  37424  brssr  37861  lsatcmp  38363  lcvexchlem4  38397  lcvexchlem5  38398  pclvalN  39251  pclclN  39252  elpcliN  39254  docaclN  40485  dihglb2  40703  doch2val2  40725  dochocss  40727  dochexmidlem7  40827  lpolconN  40848  mapdval  40989  nacsfix  41939  mzpcompact2  41979  rgspnval  42399  rgspncl  42400  rgspnmin  42402  superficl  42807  superuncl  42808  cleq2lem  42848  clcnvlem  42863  dfrtrcl3  42973  clsk1indlem2  43282  neik0pk1imk0  43287  isotone1  43288  isotone2  43289  ntrclsiso  43307  gneispacess2  43386  mnuunid  43525  mnurndlem2  43530  ssrecnpr  43556  founiiun  44363  founiiun0  44374  islptre  44820  salgenval  45522  salgenn0  45532  salgencl  45533  sssalgen  45536  salgenss  45537  salgenuni  45538  issalgend  45539  dfsalgen2  45542  salgencntex  45544  isomgreqve  46978  opndisj  47723  opnneilem  47726  sepfsepc  47748  iscnrm3rlem8  47768  iscnrm3llem2  47771  intubeu  47797  ipolubdm  47800  ipoglbdm  47803  setrec1lem1  47920  setrec1lem3  47922  setrec2fun  47925