Theorem sseq2 3973

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 3962	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3953	. . . 4 ⊢ (𝐶 ⊆ 𝐴 → (𝐴 ⊆ 𝐵 → 𝐶 ⊆ 𝐵))
3	2	com12 32	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵))
4		sstr2 3953	. . . 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 1540   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3931

This theorem is referenced by:  sseq12  3974  sseq2i  3976  sseq2d  3979  nssne1  4009  psseq2  4054  sseq0  4366  un00  4408  disjpss  4424  pweqALT  4578  ssintab  4929  ssintub  4930  intmin  4932  treq  5222  al0ssb  5263  sseliALT  5264  ssexg  5278  intabs  5304  iunopeqop  5481  onelssex  6381  ordunidif  6382  ordssun  6436  fununi  6591  feq3  6668  ssimaexg  6947  fnssintima  7337  iunpw  7747  tfindsg  7837  limomss  7847  findsg  7873  funcnvuni  7908  frxp  8105  frrlem1  8265  frrlem13  8277  onfununi  8310  oawordeu  8519  oawordexr  8520  nnawordex  8601  eldifsucnn  8628  coflton  8635  cofon1  8636  cofon2  8637  cofonr  8638  naddcllem  8640  naddunif  8657  ereq1  8678  xpider  8761  domeng  8934  sbthlem4  9054  sbthlem5  9055  domssex  9102  ssfi  9137  finsschain  9310  dffi2  9374  dffi3  9382  hartogslem1  9495  inf3lema  9577  cantnflem1  9642  dfttrcl2  9677  tz9.1  9682  tz9.1c  9683  tctr  9693  tcmin  9694  tcrank  9837  scottex  9838  cardlim  9925  infxpenlem  9966  infxpenc2  9975  isinfcard  10045  alephinit  10048  alephval3  10063  dfac3  10074  cflem  10198  cflemOLD  10199  cfval  10200  cflecard  10206  cfsuc  10210  cff1  10211  cfflb  10212  cflim2  10216  isf32lem2  10307  fin1a2lem13  10365  ac7g  10427  ttukeylem5  10466  ttukeylem7  10468  pwcfsdom  10536  pwfseqlem5  10616  pwfseq  10617  gch2  10628  winalim  10648  wunex  10692  wuncss  10698  eltskg  10703  eltsk2g  10704  gruina  10771  grur1a  10772  axgroth6  10781  swrdnd2  14620  trcleq2lem  14957  dfrtrcl2  15028  fprodss  15914  mrcflem  17567  mrcval  17571  isacs2  17614  acsfiel  17615  ipoval  18489  fpwipodrs  18499  ipodrsima  18500  mreclatBAD  18522  slwispgp  19541  pgpssslw  19544  lsmss1b  19596  lsmss2b  19598  cntzcmnss  19771  gsumzres  19839  rgspnval  20521  rgspncl  20522  rgspnmin  20524  lspf  20880  lspval  20881  lbsextlem1  21068  lbsextlem3  21070  lbsextlem4  21071  aspval  21782  mplsubglem  21908  mpllsslem  21909  basis2  22838  eltg2  22845  clsval  22924  clscld  22934  clsval2  22937  ntrcls0  22963  isnei  22990  neiint  22991  neips  23000  opnneissb  23001  opnssneib  23002  neindisj2  23010  innei  23012  neiptoptop  23018  neiptopnei  23019  neitr  23067  restcls  23068  cnpimaex  23143  cnprest2  23177  regsep  23221  nrmsep3  23242  nrmsep  23244  regsep2  23263  tgcmp  23288  uncmp  23290  bwth  23297  1stcfb  23332  1stcrest  23340  2ndcctbss  23342  1stcelcls  23348  lly1stc  23383  ssref  23399  refref  23400  comppfsc  23419  xkoopn  23476  neitx  23494  txcnp  23507  txcmplem1  23528  kqnrmlem1  23630  kqnrmlem2  23631  nrmhmph  23681  fbssfi  23724  opnfbas  23729  fbasfip  23755  fbunfip  23756  fgss2  23761  fgcl  23765  supfil  23782  isufil2  23795  filssufilg  23798  ssufl  23805  ufileu  23806  elfm3  23837  fmfnfm  23845  ufldom  23849  fbflim2  23864  flfneii  23879  flftg  23883  txflf  23893  supnfcls  23907  fclscf  23912  fclsfnflim  23914  flimfnfcls  23915  alexsubALTlem2  23935  alexsubALTlem3  23936  alexsubALTlem4  23937  alexsubALT  23938  tsmsfbas  24015  tsmsres  24031  tsmsf1o  24032  tsmsxplem1  24040  tsmsxp  24042  ustssel  24093  ustincl  24095  ustdiag  24096  ustinvel  24097  ustexhalf  24098  ust0  24107  elutop  24121  ustuqtop4  24132  cfiluexsm  24177  cfiluweak  24182  blssps  24312  blss  24313  metss  24396  metrest  24412  metcnp3  24428  metnrmlem3  24750  lebnumlem3  24862  lebnum  24863  ellimc3  25780  lhop1lem  25918  dchrelbas  27147  eqscut2  27718  scutun12  27722  madebdayim  27799  madebday  27811  onsiso  28169  bdayn0p1  28258  upgredgpr  29069  dfnbgr3  29265  nbupgr  29271  nbumgrvtx  29273  nbgr2vtx1edg  29277  nbuhgr2vtx1edgb  29279  cusgrexilem2  29369  wlkvtxiedg  29553  wlkres  29598  upgr1wlkdlem2  30075  1pthon2v  30082  1pthon2ve  30083  cusconngr  30120  isfrgr  30189  avril1  30392  spanval  31262  spancl  31265  shsval2i  31316  omlsi  31333  ococin  31337  chsupsn  31342  pjoml  31365  shs00i  31379  chj00i  31416  chsscon3  31429  chlejb1  31441  chnle  31443  pjoml2  31540  pjoml3  31541  lecm  31546  stcltr1i  32203  mdbr  32223  dmdmd  32229  dmdi  32231  dmdbr3  32234  dmdbr4  32235  mdsl1i  32250  mdslmd1lem3  32256  mdslmd1lem4  32257  csmdsymi  32263  hatomic  32289  chrelat2  32299  atord  32317  atcvat4i  32326  fz1nntr  32727  elrgspnlem4  33196  fldgenval  33262  fldgensdrg  33264  fldgenssv  33265  fldgenssp  33268  nsgmgc  33383  nsgqusf1olem2  33385  isprmidl  33409  ssdifidllem  33427  ssdifidl  33428  ssdifidlprm  33429  mxidlmax  33436  ssmxidllem  33444  ssmxidl  33445  1arithufdlem4  33518  reff  33829  cmpcref  33840  zarcls1  33859  zarclsiin  33861  zarclssn  33863  zart0  33869  zarmxt1  33870  zarcmp  33872  rhmpreimacnlem  33874  sigagenval  34130  dmsigagen  34134  sigagenss  34139  ldsysgenld  34150  ldgenpisyslem1  34153  ldgenpisyslem2  34154  dynkin  34157  carsgmon  34305  carsgclctunlem2  34310  bnj1286  35009  bnj1452  35042  fineqvac  35087  onvf1odlem4  35093  vonf1owev  35095  kur14lem9  35201  mclsssvlem  35549  mclsind  35557  imagesset  35941  altopthsn  35949  fnessref  36345  refssfne  36346  topjoin  36353  neifg  36359  bj-snglex  36961  bj-imdirvallem  37168  relowlssretop  37351  relowlpssretop  37352  exrecfnlem  37367  finxpreclem3  37381  pibt2  37405  poimirlem29  37643  poimir  37647  mblfinlem3  37653  totbndss  37771  heibor1lem  37803  unichnidl  38025  ispridl  38028  maxidlmax  38037  igenval  38055  igenidl  38057  igenmin  38058  igenval2  38060  brssr  38492  lsatcmp  38996  lcvexchlem4  39030  lcvexchlem5  39031  pclvalN  39884  pclclN  39885  elpcliN  39887  docaclN  41118  dihglb2  41336  doch2val2  41358  dochocss  41360  dochexmidlem7  41460  lpolconN  41481  mapdval  41622  nacsfix  42700  mzpcompact2  42740  superficl  43556  superuncl  43557  cleq2lem  43597  clcnvlem  43612  dfrtrcl3  43722  clsk1indlem2  44031  neik0pk1imk0  44036  isotone1  44037  isotone2  44038  ntrclsiso  44056  gneispacess2  44135  mnuunid  44266  mnurndlem2  44271  ssrecnpr  44297  founiiun  45173  founiiun0  45184  islptre  45617  salgenval  46319  salgenn0  46329  salgencl  46330  sssalgen  46333  salgenss  46334  salgenuni  46335  issalgend  46336  dfsalgen2  46339  salgencntex  46341  dfclnbgr3  47827  predgclnbgrel  47839  clnbgredg  47840  clnbgrgrimlem  47933  clnbgrgrim  47934  opndisj  48891  opnneilem  48894  sepfsepc  48916  iscnrm3rlem8  48935  iscnrm3llem2  48938  intubeu  48972  ipolubdm  48975  ipoglbdm  48978  setrec1lem1  49676  setrec1lem3  49678  setrec2fun  49681