Theorem sseq2 4009

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		eqss 3998	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3989	. . . 4 ⊢ (𝐶 ⊆ 𝐴 → (𝐴 ⊆ 𝐵 → 𝐶 ⊆ 𝐵))
3	2	com12 32	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵))
4		sstr2 3989	. . . 4 ⊢ (𝐶 ⊆ 𝐵 → (𝐵 ⊆ 𝐴 → 𝐶 ⊆ 𝐴))
5	4	com12 32	. . 3 ⊢ (𝐵 ⊆ 𝐴 → (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴))
6	3, 5	anbiim 641	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))
7	1, 6	sylbi 217	1 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1539   ⊆ wss 3950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2728  df-ss 3967

This theorem is referenced by:  sseq12  4010  sseq2i  4012  sseq2d  4015  nssne1  4045  psseq2  4090  sseq0  4402  un00  4444  disjpss  4460  pweqALT  4614  ssintab  4964  ssintub  4965  intmin  4967  treq  5266  al0ssb  5307  sseliALT  5308  ssexg  5322  intabs  5348  iunopeqop  5525  onelssex  6431  ordunidif  6432  ordssun  6485  fununi  6640  feq3  6717  ssimaexg  6994  fnssintima  7383  iunpw  7792  tfindsg  7883  limomss  7893  findsg  7920  funcnvuni  7955  frxp  8152  frrlem1  8312  frrlem13  8324  wrecseq123OLD  8341  wfrlem1OLD  8349  wfrlem4OLD  8353  wfrlem15OLD  8364  onfununi  8382  oawordeu  8594  oawordexr  8595  nnawordex  8676  eldifsucnn  8703  coflton  8710  cofon1  8711  cofon2  8712  cofonr  8713  naddcllem  8715  naddunif  8732  ereq1  8753  xpider  8829  domeng  9004  sbthlem4  9127  sbthlem5  9128  domssex  9179  ssfi  9214  finsschain  9400  dffi2  9464  dffi3  9472  hartogslem1  9583  inf3lema  9665  cantnflem1  9730  dfttrcl2  9765  tz9.1  9770  tz9.1c  9771  tctr  9781  tcmin  9782  tcrank  9925  scottex  9926  cardlim  10013  infxpenlem  10054  infxpenc2  10063  isinfcard  10133  alephinit  10136  alephval3  10151  dfac3  10162  cflem  10286  cflemOLD  10287  cfval  10288  cflecard  10294  cfsuc  10298  cff1  10299  cfflb  10300  cflim2  10304  isf32lem2  10395  fin1a2lem13  10453  ac7g  10515  ttukeylem5  10554  ttukeylem7  10556  pwcfsdom  10624  pwfseqlem5  10704  pwfseq  10705  gch2  10716  winalim  10736  wunex  10780  wuncss  10786  eltskg  10791  eltsk2g  10792  gruina  10859  grur1a  10860  axgroth6  10869  swrdnd2  14694  trcleq2lem  15031  dfrtrcl2  15102  fprodss  15985  mrcflem  17650  mrcval  17654  isacs2  17697  acsfiel  17698  ipoval  18576  fpwipodrs  18586  ipodrsima  18587  mreclatBAD  18609  slwispgp  19630  pgpssslw  19633  lsmss1b  19685  lsmss2b  19687  cntzcmnss  19860  gsumzres  19928  rgspnval  20613  rgspncl  20614  rgspnmin  20616  lspf  20973  lspval  20974  lbsextlem1  21161  lbsextlem3  21163  lbsextlem4  21164  aspval  21894  mplsubglem  22020  mpllsslem  22021  basis2  22959  eltg2  22966  clsval  23046  clscld  23056  clsval2  23059  ntrcls0  23085  isnei  23112  neiint  23113  neips  23122  opnneissb  23123  opnssneib  23124  neindisj2  23132  innei  23134  neiptoptop  23140  neiptopnei  23141  neitr  23189  restcls  23190  cnpimaex  23265  cnprest2  23299  regsep  23343  nrmsep3  23364  nrmsep  23366  regsep2  23385  tgcmp  23410  uncmp  23412  bwth  23419  1stcfb  23454  1stcrest  23462  2ndcctbss  23464  1stcelcls  23470  lly1stc  23505  ssref  23521  refref  23522  comppfsc  23541  xkoopn  23598  neitx  23616  txcnp  23629  txcmplem1  23650  kqnrmlem1  23752  kqnrmlem2  23753  nrmhmph  23803  fbssfi  23846  opnfbas  23851  fbasfip  23877  fbunfip  23878  fgss2  23883  fgcl  23887  supfil  23904  isufil2  23917  filssufilg  23920  ssufl  23927  ufileu  23928  elfm3  23959  fmfnfm  23967  ufldom  23971  fbflim2  23986  flfneii  24001  flftg  24005  txflf  24015  supnfcls  24029  fclscf  24034  fclsfnflim  24036  flimfnfcls  24037  alexsubALTlem2  24057  alexsubALTlem3  24058  alexsubALTlem4  24059  alexsubALT  24060  tsmsfbas  24137  tsmsres  24153  tsmsf1o  24154  tsmsxplem1  24162  tsmsxp  24164  ustssel  24215  ustincl  24217  ustdiag  24218  ustinvel  24219  ustexhalf  24220  ust0  24229  elutop  24243  ustuqtop4  24254  cfiluexsm  24300  cfiluweak  24305  blssps  24435  blss  24436  metss  24522  metrest  24538  metcnp3  24554  metnrmlem3  24884  lebnumlem3  24996  lebnum  24997  ellimc3  25915  lhop1lem  26053  dchrelbas  27281  eqscut2  27852  scutun12  27856  madebdayim  27927  madebday  27939  upgredgpr  29160  dfnbgr3  29356  nbupgr  29362  nbumgrvtx  29364  nbgr2vtx1edg  29368  nbuhgr2vtx1edgb  29370  cusgrexilem2  29460  wlkvtxiedg  29644  wlkres  29689  upgr1wlkdlem2  30166  1pthon2v  30173  1pthon2ve  30174  cusconngr  30211  isfrgr  30280  avril1  30483  spanval  31353  spancl  31356  shsval2i  31407  omlsi  31424  ococin  31428  chsupsn  31433  pjoml  31456  shs00i  31470  chj00i  31507  chsscon3  31520  chlejb1  31532  chnle  31534  pjoml2  31631  pjoml3  31632  lecm  31637  stcltr1i  32294  mdbr  32314  dmdmd  32320  dmdi  32322  dmdbr3  32325  dmdbr4  32326  mdsl1i  32341  mdslmd1lem3  32347  mdslmd1lem4  32348  csmdsymi  32354  hatomic  32380  chrelat2  32390  atord  32408  atcvat4i  32417  fz1nntr  32807  elrgspnlem4  33250  fldgenval  33315  fldgensdrg  33317  fldgenssv  33318  fldgenssp  33321  nsgmgc  33441  nsgqusf1olem2  33443  isprmidl  33467  ssdifidllem  33485  ssdifidl  33486  ssdifidlprm  33487  mxidlmax  33494  ssmxidllem  33502  ssmxidl  33503  1arithufdlem4  33576  reff  33839  cmpcref  33850  zarcls1  33869  zarclsiin  33871  zarclssn  33873  zart0  33879  zarmxt1  33880  zarcmp  33882  rhmpreimacnlem  33884  sigagenval  34142  dmsigagen  34146  sigagenss  34151  ldsysgenld  34162  ldgenpisyslem1  34165  ldgenpisyslem2  34166  dynkin  34169  carsgmon  34317  carsgclctunlem2  34322  bnj1286  35034  bnj1452  35067  fineqvac  35112  kur14lem9  35220  mclsssvlem  35568  mclsind  35576  imagesset  35955  altopthsn  35963  fnessref  36359  refssfne  36360  topjoin  36367  neifg  36373  bj-snglex  36975  bj-imdirvallem  37182  relowlssretop  37365  relowlpssretop  37366  exrecfnlem  37381  finxpreclem3  37395  pibt2  37419  poimirlem29  37657  poimir  37661  mblfinlem3  37667  totbndss  37785  heibor1lem  37817  unichnidl  38039  ispridl  38042  maxidlmax  38051  igenval  38069  igenidl  38071  igenmin  38072  igenval2  38074  brssr  38503  lsatcmp  39005  lcvexchlem4  39039  lcvexchlem5  39040  pclvalN  39893  pclclN  39894  elpcliN  39896  docaclN  41127  dihglb2  41345  doch2val2  41367  dochocss  41369  dochexmidlem7  41469  lpolconN  41490  mapdval  41631  nacsfix  42728  mzpcompact2  42768  superficl  43585  superuncl  43586  cleq2lem  43626  clcnvlem  43641  dfrtrcl3  43751  clsk1indlem2  44060  neik0pk1imk0  44065  isotone1  44066  isotone2  44067  ntrclsiso  44085  gneispacess2  44164  mnuunid  44301  mnurndlem2  44306  ssrecnpr  44332  founiiun  45189  founiiun0  45200  islptre  45639  salgenval  46341  salgenn0  46351  salgencl  46352  sssalgen  46355  salgenss  46356  salgenuni  46357  issalgend  46358  dfsalgen2  46361  salgencntex  46363  dfclnbgr3  47818  predgclnbgrel  47830  clnbgredg  47831  clnbgrgrimlem  47906  clnbgrgrim  47907  opndisj  48807  opnneilem  48810  sepfsepc  48832  iscnrm3rlem8  48851  iscnrm3llem2  48854  intubeu  48888  ipolubdm  48891  ipoglbdm  48894  setrec1lem1  49261  setrec1lem3  49263  setrec2fun  49266