Theorem sseq2 3960

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 3949	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3941	. . . 4 ⊢ (𝐶 ⊆ 𝐴 → (𝐴 ⊆ 𝐵 → 𝐶 ⊆ 𝐵))
3	2	com12 32	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵))
4		sstr2 3941	. . . 4 ⊢ (𝐶 ⊆ 𝐵 → (𝐵 ⊆ 𝐴 → 𝐶 ⊆ 𝐴))
5	4	com12 32	. . 3 ⊢ (𝐵 ⊆ 𝐴 → (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴))
6	3, 5	anbiim 650	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))
7	1, 6	sylbi 219	1 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1559   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ss 3919

This theorem is referenced by:  sseq12  3961  sseq2i  3963  sseq2d  3966  nssne1  3996  psseq2  4042  sseq0  4354  un00  4396  disjpss  4412  pweqALT  4567  ssintab  4920  ssintub  4921  intmin  4923  treq  5211  al0ssb  5255  sseliALT  5256  ssexg  5276  intabs  5302  iunopeqop  5487  iunopeqopOLD  5488  onelssex  6389  ordunidif  6390  ordssun  6444  fununi  6590  feq3  6665  ssimaexg  6947  fnssintima  7340  iunpw  7748  tfindsg  7835  limomss  7845  findsg  7872  funcnvuni  7907  frxp  8099  frrlem1  8260  frrlem13  8272  onfununi  8305  oawordeu  8517  oawordexr  8518  nnawordex  8600  eldifsucnn  8627  coflton  8634  cofon1  8635  cofon2  8636  cofonr  8637  naddcllem  8639  naddunif  8657  ereq1  8679  xpider  8763  domeng  8936  sbthlem4  9055  sbthlem5  9056  domssex  9103  ssfi  9134  finsschain  9295  dffi2  9362  dffi3  9370  hartogslem1  9483  inf3lema  9572  cantnflem1  9637  dfttrcl2  9672  tz9.1  9677  tz9.1c  9678  tctr  9686  tcmin  9687  tcrank  9835  scottex  9836  cardlim  9923  infxpenlem  9962  infxpenc2  9971  isinfcard  10041  alephinit  10044  alephval3  10059  dfac3  10070  cflem  10194  cflemOLD  10195  cfval  10196  cflecard  10202  cfsuc  10207  cff1  10208  cfflb  10209  cflim2  10213  isf32lem2  10304  fin1a2lem13  10362  ac7g  10424  ttukeylem5  10463  ttukeylem7  10465  pwcfsdom  10534  pwfseqlem5  10614  pwfseq  10615  gch2  10626  winalim  10646  wunex  10690  wuncss  10696  eltskg  10701  eltsk2g  10702  gruina  10769  grur1a  10770  axgroth6  10779  swrdnd2  14662  trcleq2lem  14997  dfrtrcl2  15068  fprodss  15968  mrcflem  17628  mrcval  17632  isacs2  17675  acsfiel  17676  ipoval  18552  fpwipodrs  18562  ipodrsima  18563  mreclatBAD  18585  slwispgp  19641  pgpssslw  19644  lsmss1b  19696  lsmss2b  19698  cntzcmnss  19871  gsumzres  19939  rgspnval  20648  rgspncl  20649  rgspnmin  20651  lspf  21028  lspval  21029  lbsextlem1  21215  lbsextlem3  21217  lbsextlem4  21218  aspval  21911  mplsubglem  22037  mpllsslem  22038  basis2  22998  eltg2  23005  clsval  23084  clscld  23094  clsval2  23097  ntrcls0  23123  isnei  23150  neiint  23151  neips  23160  opnneissb  23161  opnssneib  23162  neindisj2  23170  innei  23172  neiptoptop  23178  neiptopnei  23179  neitr  23227  restcls  23228  cnpimaex  23303  cnprest2  23337  regsep  23381  nrmsep3  23402  nrmsep  23404  regsep2  23423  tgcmp  23448  uncmp  23450  bwth  23457  1stcfb  23492  1stcrest  23500  2ndcctbss  23502  1stcelcls  23508  lly1stc  23543  ssref  23559  refref  23560  comppfsc  23579  xkoopn  23636  neitx  23654  txcnp  23667  txcmplem1  23688  kqnrmlem1  23790  kqnrmlem2  23791  nrmhmph  23841  fbssfi  23884  opnfbas  23889  fbasfip  23915  fbunfip  23916  fgss2  23921  fgcl  23925  supfil  23942  isufil2  23955  filssufilg  23958  ssufl  23965  ufileu  23966  elfm3  23997  fmfnfm  24005  ufldom  24009  fbflim2  24024  flfneii  24039  flftg  24043  txflf  24053  supnfcls  24067  fclscf  24072  fclsfnflim  24074  flimfnfcls  24075  alexsubALTlem2  24095  alexsubALTlem3  24096  alexsubALTlem4  24097  alexsubALT  24098  tsmsfbas  24175  tsmsres  24191  tsmsf1o  24192  tsmsxplem1  24200  tsmsxp  24202  ustssel  24253  ustincl  24255  ustdiag  24256  ustinvel  24257  ustexhalf  24258  ust0  24267  elutop  24280  ustuqtop4  24291  cfiluexsm  24336  cfiluweak  24341  blssps  24471  blss  24472  metss  24555  metrest  24571  metcnp3  24587  metnrmlem3  24909  lebnumlem3  25012  lebnum  25013  ellimc3  25928  lhop1lem  26062  dchrelbas  27287  eqcuts2  27866  cutsun12  27870  madebdayim  27968  madebday  27980  oniso  28351  bdayn0p1  28449  upgredgpr  29299  dfnbgr3  29495  nbupgr  29501  nbumgrvtx  29503  nbgr2vtx1edg  29507  nbuhgr2vtx1edgb  29509  cusgrexilem2  29599  wlkvtxiedg  29781  wlkres  29825  upgr1wlkdlem2  30304  1pthon2v  30311  1pthon2ve  30312  cusconngr  30349  isfrgr  30418  avril1  30621  spanval  31492  spancl  31495  shsval2i  31546  omlsi  31563  ococin  31567  chsupsn  31572  pjoml  31595  shs00i  31609  chj00i  31646  chsscon3  31659  chlejb1  31671  chnle  31673  pjoml2  31770  pjoml3  31771  lecm  31776  stcltr1i  32433  mdbr  32453  dmdmd  32459  dmdi  32461  dmdbr3  32464  dmdbr4  32465  mdsl1i  32480  mdslmd1lem3  32486  mdslmd1lem4  32487  csmdsymi  32493  hatomic  32519  chrelat2  32529  atord  32547  atcvat4i  32556  fz1nntr  32964  elrgspnlem4  33386  fldgenval  33459  fldgensdrg  33461  fldgenssv  33462  fldgenssp  33465  nsgmgc  33558  nsgqusf1olem2  33560  isprmidl  33584  ssdifidllem  33603  ssdifidl  33604  ssdifidlprm  33605  mxidlmax  33613  ssmxidllem  33621  ssmxidl  33622  dflringlem  33650  1arithufdlem4  33703  reff  34096  cmpcref  34107  zarcls1  34126  zarclsiin  34128  zarclssn  34130  zart0  34136  zarmxt1  34137  zarcmp  34139  rhmpreimacnlem  34141  sigagenval  34397  dmsigagen  34401  sigagenss  34406  ldsysgenld  34417  ldgenpisyslem1  34420  ldgenpisyslem2  34421  dynkin  34424  carsgmon  34571  carsgclctunlem2  34576  bnj1286  35274  bnj1452  35307  fineqvac  35372  tz9.1regs  35390  onvf1odlem4  35409  vonf1wev  35411  vonf1owevOLD  35413  kur14lem9  35524  mclsssvlem  35872  mclsind  35880  imagesset  36263  altopthsn  36271  fnessref  36677  refssfne  36678  topjoin  36685  neifg  36691  tz9.1tco  36803  ttc00  36828  dfttc3gw  36843  bj-snglex  37418  bj-imdirvallem  37632  relowlssretop  37817  relowlpssretop  37818  exrecfnlem  37833  finxpreclem3  37847  pibt2  37871  poimirlem29  38108  poimir  38112  mblfinlem3  38118  totbndss  38236  heibor1lem  38268  unichnidl  38490  ispridl  38493  maxidlmax  38502  igenval  38520  igenidl  38522  igenmin  38523  igenval2  38525  dfsuccl4  38933  brssr  39040  suceldisj  39277  lsatcmp  39587  lcvexchlem4  39621  lcvexchlem5  39622  pclvalN  40474  pclclN  40475  elpcliN  40477  docaclN  41708  dihglb2  41926  doch2val2  41948  dochocss  41950  dochexmidlem7  42050  lpolconN  42071  mapdval  42212  nacsfix  43253  mzpcompact2  43293  superficl  44103  superuncl  44104  cleq2lem  44144  clcnvlem  44159  dfrtrcl3  44269  clsk1indlem2  44578  neik0pk1imk0  44583  isotone1  44584  isotone2  44585  ntrclsiso  44603  gneispacess2  44682  mnuunid  44813  mnurndlem2  44818  ssrecnpr  44844  founiiun  45717  founiiun0  45728  islptre  46155  salgenval  46855  salgenn0  46865  salgencl  46866  sssalgen  46869  salgenss  46870  salgenuni  46871  issalgend  46872  dfsalgen2  46875  salgencntex  46877  dfclnbgr3  48408  predgclnbgrel  48421  clnbgredg  48422  clnbgrgrimlem  48515  clnbgrgrim  48516  opndisj  49484  opnneilem  49487  sepfsepc  49509  iscnrm3rlem8  49528  iscnrm3llem2  49531  intubeu  49565  ipolubdm  49568  ipoglbdm  49571  setrec1lem1  50268  setrec1lem3  50270  setrec2fun  50273