Theorem sseq2 3934

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 3923	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3915	. . . 4 ⊢ (𝐶 ⊆ 𝐴 → (𝐴 ⊆ 𝐵 → 𝐶 ⊆ 𝐵))
3	2	com12 33	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵))
4		sstr2 3915	. . . 4 ⊢ (𝐶 ⊆ 𝐵 → (𝐵 ⊆ 𝐴 → 𝐶 ⊆ 𝐴))
5	4	com12 33	. . 3 ⊢ (𝐵 ⊆ 𝐴 → (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴))
6	3, 5	anbiim 653	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))
7	1, 6	sylbi 220	1 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ⊆ wss 3895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ss 3896

This theorem is used by:  sseq12  3935  sseq2i  3937  sseq2d  3940  nssne1  3970  psseq2  4018  sseq0b  4352  un00  4356  disjpss  4413  pweqALT  4571  ssintab  4924  ssintub  4925  intmin  4927  treq  5218  al0ssb  5261  sseliALT  5262  ssexgOLD  5284  intabs  5309  iunopeqop  5493  iunopeqopOLD  5494  onelssex  6412  ordunidif  6413  ordssun  6467  fununi  6616  feq3  6690  ssimaexg  6972  fnssintima  7373  iunpw  7786  tfindsg  7873  limomss  7883  findsg  7910  funcnvuni  7945  frxp  8141  frrlem1  8308  frrlem13  8320  onfununi  8353  oawordeu  8567  oawordexr  8568  nnawordex  8650  eldifsucnn  8677  coflton  8684  cofon1  8685  cofon2  8686  cofonr  8687  naddcllem  8689  naddunif  8707  ereq1  8729  xpider  8813  domeng  8993  sbthlem4  9113  sbthlem5  9114  domssex  9161  ssfi  9192  finsschain  9352  dffi2  9419  dffi3  9427  hartogslem1  9540  inf3lema  9629  cantnflem1  9694  dfttrcl2  9729  tz9.1  9734  tz9.1c  9735  tctr  9743  tcmin  9744  tcrank  9905  scottex  9937  scottexOLD  9938  setrec1lem1  9970  setrec1lem3  9973  setrec2fun  9977  cardlim  10057  infxpenlem  10096  infxpenc2  10105  isinfcard  10175  alephinit  10178  alephval3  10193  dfac3  10204  cflem  10327  cfval  10328  cflecard  10334  cfsuc  10339  cff1  10340  cfflb  10341  cflim2  10345  isf32lem2  10436  fin1a2lem13  10494  ac7g  10556  ttukeylem5  10595  ttukeylem7  10597  pwcfsdom  10672  pwfseqlem5  10752  pwfseq  10753  gch2  10764  winalim  10784  wunex  10828  wuncss  10834  eltskg  10839  eltsk2g  10840  gruina  10907  grur1a  10908  axgroth6  10917  swrdnd2  14810  trcleq2lem  15150  dfrtrcl2  15221  fprodss  16121  mrcflem  17786  mrcval  17790  isacs2  17833  acsfiel  17834  ipoval  18710  fpwipodrs  18720  ipodrsima  18721  mreclatBAD  18743  slwispgp  19831  pgpssslw  19834  lsmss1b  19886  lsmss2b  19888  cntzcmnss  20061  gsumzres  20129  rgspnval  20870  rgspncl  20871  rgspnmin  20873  lspf  21255  lspval  21256  lbsextlem1  21442  lbsextlem3  21444  lbsextlem4  21445  unichnlidl  21522  rspprop  21530  isprmidl  21625  ssdifidllem  21646  ssdifidl  21647  ssdifidlprm  21648  aspval  22186  mplsubglem  22312  mpllsslem  22313  basis2  23275  eltg2  23282  clsval  23361  clscld  23371  clsval2  23374  ntrcls0  23400  isnei  23427  neiint  23428  neips  23437  opnneissb  23438  opnssneib  23439  neindisj2  23447  innei  23449  neiptoptop  23455  neiptopnei  23456  neitr  23504  restcls  23505  cnpimaex  23580  cnprest2  23614  regsep  23658  nrmsep3  23679  nrmsep  23681  regsep2  23700  tgcmp  23725  uncmp  23727  bwth  23734  1stcfb  23769  1stcrest  23777  2ndcctbss  23780  1stcelcls  23786  lly1stc  23821  ssref  23837  refref  23838  comppfsc  23857  xkoopn  23914  neitx  23932  txcnp  23945  txcmplem1  23966  kqnrmlem1  24068  kqnrmlem2  24069  nrmhmph  24119  fbssfi  24162  opnfbas  24167  fbasfip  24193  fbunfip  24194  fgss2  24199  fgcl  24203  supfil  24220  isufil2  24233  filssufilg  24236  ssufl  24243  ufileu  24244  elfm3  24275  fmfnfm  24283  ufldom  24287  fbflim2  24302  flfneii  24317  flftg  24321  txflf  24331  supnfcls  24345  fclscf  24350  fclsfnflim  24352  flimfnfcls  24353  alexsubALTlem2  24373  alexsubALTlem3  24374  alexsubALTlem4  24375  alexsubALT  24376  tsmsfbas  24453  tsmsres  24469  tsmsf1o  24470  tsmsxplem1  24478  tsmsxp  24480  ustssel  24531  ustincl  24533  ustdiag  24534  ustinvel  24535  ustexhalf  24536  ust0  24545  elutop  24558  ustuqtop4  24569  cfiluexsm  24614  cfiluweak  24619  blssps  24749  blss  24750  metss  24833  metrest  24849  metcnp3  24865  metnrmlem3  25187  lebnumlem3  25290  lebnum  25291  ellimc3  26205  lhop1lem  26339  dchrelbas  27569  eqcuts2  28178  cutsun12  28182  madebdayim  28280  madebday  28292  oniso  28663  bdayn0p1  28761  prlngd  29423  dfprlng2  29431  upgredgpr  29726  dfnbgr3  29925  nbupgr  29931  nbumgrvtx  29933  nbgr2vtx1edg  29937  nbuhgr2vtx1edgb  29939  cusgrexilem2  30029  wlkvtxiedg  30211  wlkres  30255  upgr1wlkdlem2  30743  1pthon2v  30760  1pthon2ve  30761  cusconngr  30798  isfrgr  30867  avril1  31070  spanval  31941  spancl  31944  shsval2i  31995  omlsi  32012  ococin  32016  chsupsn  32021  pjoml  32044  shs00i  32058  chj00i  32095  chsscon3  32108  chlejb1  32120  chnle  32122  pjoml2  32219  pjoml3  32220  lecm  32225  stcltr1i  32882  mdbr  32902  dmdmd  32908  dmdi  32910  dmdbr3  32913  dmdbr4  32914  mdsl1i  32929  mdslmd1lem3  32935  mdslmd1lem4  32936  csmdsymi  32942  hatomic  32968  chrelat2  32978  atord  32996  atcvat4i  33005  fz1nntr  33441  elrgspnlem4  33853  fldgenval  33921  fldgensdrg  33923  fldgenssv  33924  fldgenssp  33927  nsgmgc  34010  nsgqusf1olem2  34012  mxidlmax  34037  ssmxidllem  34045  ssmxidl  34046  dflringlem  34073  1arithufdlem4  34126  reff  34518  cmpcref  34529  zarcls1  34548  zarclsiin  34550  zarclssn  34552  zart0  34558  zarmxt1  34559  zarcmp  34561  rhmpreimacnlem  34563  sigagenval  34820  dmsigagen  34824  sigagenss  34829  ldsysgenld  34840  ldgenpisyslem1  34843  ldgenpisyslem2  34844  dynkin  34847  carsgmon  34993  carsgclctunlem2  34998  bnj1286  35696  bnj1452  35729  rankse  35794  fineqvac  35841  tz9.1regs  35859  onvf1odlem4  35954  vonf1wev  35956  vonf1owevOLD  35958  kur14lem9  36066  mclsssvlem  36414  mclsind  36422  imagesset  36810  altopthsn  36819  fnessref  37238  refssfne  37239  topjoin  37246  neifg  37252  tz9.1tco  37364  ttc00  37389  dfttc3gw  37404  bj-snglex  37979  bj-imdirvallem  38195  relowlssretop  38380  relowlpssretop  38381  exrecfnlem  38396  finxpreclem3  38410  pibt2  38434  poimirlem29  38661  poimir  38665  mblfinlem3  38671  totbndss  38805  heibor1lem  38837  unichnidl  39059  ispridl  39062  maxidlmax  39071  igenval  39089  igenidl  39091  igenmin  39092  igenval2  39094  dfsuccl4  39500  brssr  39607  suceldisj  39844  lsatcmp  40154  lcvexchlem4  40188  lcvexchlem5  40189  pclvalN  41041  pclclN  41042  elpcliN  41044  docaclN  42275  dihglb2  42493  doch2val2  42515  dochocss  42517  dochexmidlem7  42617  lpolconN  42638  mapdval  42779  nacsfix  43817  mzpcompact2  43857  superficl  44662  superuncl  44663  cleq2lem  44702  clcnvlem  44717  dfrtrcl3  44827  clsk1indlem2  45136  neik0pk1imk0  45141  isotone1  45142  isotone2  45143  ntrclsiso  45161  gneispacess2  45240  mnuunid  45355  mnurndlem2  45360  ssrecnpr  45386  founiiun  46288  founiiun0  46299  islptre  46725  salgenval  47425  salgenn0  47435  salgencl  47436  sssalgen  47439  salgenss  47440  salgenuni  47441  issalgend  47442  dfsalgen2  47445  salgencntex  47447  dfclnbgr3  49018  predgclnbgrel  49031  clnbgredg  49032  clnbgrgrimlem  49125  clnbgrgrim  49126  opndisj  50111  opnneilem  50114  sepfsepc  50136  iscnrm3rlem8  50155  iscnrm3llem2  50158  intubeu  50192  ipolubdm  50195  ipoglbdm  50198