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 33	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵))
4		sstr2 3941	. . . 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 1570   ⊆ wss 3902

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-ss 3919

This theorem is used by:  sseq12  3961  sseq2i  3963  sseq2d  3966  nssne1  3996  psseq2  4042  sseq0b  4356  un00  4360  disjpss  4417  pweqALT  4575  ssintab  4928  ssintub  4929  intmin  4931  treq  5223  al0ssb  5269  sseliALT  5270  ssexgOLD  5292  intabs  5317  iunopeqop  5502  iunopeqopOLD  5503  onelssex  6411  ordunidif  6412  ordssun  6466  fununi  6612  feq3  6686  ssimaexg  6968  fnssintima  7369  iunpw  7774  tfindsg  7861  limomss  7871  findsg  7898  funcnvuni  7933  frxp  8128  frrlem1  8289  frrlem13  8301  onfununi  8334  oawordeu  8546  oawordexr  8547  nnawordex  8629  eldifsucnn  8656  coflton  8663  cofon1  8664  cofon2  8665  cofonr  8666  naddcllem  8668  naddunif  8686  ereq1  8708  xpider  8792  domeng  8972  sbthlem4  9092  sbthlem5  9093  domssex  9140  ssfi  9171  finsschain  9330  dffi2  9397  dffi3  9405  hartogslem1  9518  inf3lema  9607  cantnflem1  9672  dfttrcl2  9707  tz9.1  9712  tz9.1c  9713  tctr  9721  tcmin  9722  tcrank  9870  scottex  9876  scottexOLD  9877  cardlim  9981  infxpenlem  10020  infxpenc2  10029  isinfcard  10099  alephinit  10102  alephval3  10117  dfac3  10128  cflem  10251  cfval  10252  cflecard  10258  cfsuc  10263  cff1  10264  cfflb  10265  cflim2  10269  isf32lem2  10360  fin1a2lem13  10418  ac7g  10480  ttukeylem5  10519  ttukeylem7  10521  pwcfsdom  10596  pwfseqlem5  10676  pwfseq  10677  gch2  10688  winalim  10708  wunex  10752  wuncss  10758  eltskg  10763  eltsk2g  10764  gruina  10831  grur1a  10832  axgroth6  10841  swrdnd2  14729  trcleq2lem  15068  dfrtrcl2  15139  fprodss  16041  mrcflem  17700  mrcval  17704  isacs2  17747  acsfiel  17748  ipoval  18624  fpwipodrs  18634  ipodrsima  18635  mreclatBAD  18657  slwispgp  19744  pgpssslw  19747  lsmss1b  19799  lsmss2b  19801  cntzcmnss  19974  gsumzres  20042  rgspnval  20780  rgspncl  20781  rgspnmin  20783  lspf  21164  lspval  21165  lbsextlem1  21351  lbsextlem3  21353  lbsextlem4  21354  unichnlidl  21431  rspprop  21439  isprmidl  21532  ssdifidllem  21553  ssdifidl  21554  ssdifidlprm  21555  aspval  22093  mplsubglem  22219  mpllsslem  22220  basis2  23182  eltg2  23189  clsval  23268  clscld  23278  clsval2  23281  ntrcls0  23307  isnei  23334  neiint  23335  neips  23344  opnneissb  23345  opnssneib  23346  neindisj2  23354  innei  23356  neiptoptop  23362  neiptopnei  23363  neitr  23411  restcls  23412  cnpimaex  23487  cnprest2  23521  regsep  23565  nrmsep3  23586  nrmsep  23588  regsep2  23607  tgcmp  23632  uncmp  23634  bwth  23641  1stcfb  23676  1stcrest  23684  2ndcctbss  23687  1stcelcls  23693  lly1stc  23728  ssref  23744  refref  23745  comppfsc  23764  xkoopn  23821  neitx  23839  txcnp  23852  txcmplem1  23873  kqnrmlem1  23975  kqnrmlem2  23976  nrmhmph  24026  fbssfi  24069  opnfbas  24074  fbasfip  24100  fbunfip  24101  fgss2  24106  fgcl  24110  supfil  24127  isufil2  24140  filssufilg  24143  ssufl  24150  ufileu  24151  elfm3  24182  fmfnfm  24190  ufldom  24194  fbflim2  24209  flfneii  24224  flftg  24228  txflf  24238  supnfcls  24252  fclscf  24257  fclsfnflim  24259  flimfnfcls  24260  alexsubALTlem2  24280  alexsubALTlem3  24281  alexsubALTlem4  24282  alexsubALT  24283  tsmsfbas  24360  tsmsres  24376  tsmsf1o  24377  tsmsxplem1  24385  tsmsxp  24387  ustssel  24438  ustincl  24440  ustdiag  24441  ustinvel  24442  ustexhalf  24443  ust0  24452  elutop  24465  ustuqtop4  24476  cfiluexsm  24521  cfiluweak  24526  blssps  24656  blss  24657  metss  24740  metrest  24756  metcnp3  24772  metnrmlem3  25094  lebnumlem3  25197  lebnum  25198  ellimc3  26113  lhop1lem  26247  dchrelbas  27480  eqcuts2  28059  cutsun12  28063  madebdayim  28161  madebday  28173  oniso  28544  bdayn0p1  28642  prlngd  29304  dfprlng2  29312  upgredgpr  29607  dfnbgr3  29806  nbupgr  29812  nbumgrvtx  29814  nbgr2vtx1edg  29818  nbuhgr2vtx1edgb  29820  cusgrexilem2  29910  wlkvtxiedg  30092  wlkres  30136  upgr1wlkdlem2  30624  1pthon2v  30641  1pthon2ve  30642  cusconngr  30679  isfrgr  30748  avril1  30951  spanval  31822  spancl  31825  shsval2i  31876  omlsi  31893  ococin  31897  chsupsn  31902  pjoml  31925  shs00i  31939  chj00i  31976  chsscon3  31989  chlejb1  32001  chnle  32003  pjoml2  32100  pjoml3  32101  lecm  32106  stcltr1i  32763  mdbr  32783  dmdmd  32789  dmdi  32791  dmdbr3  32794  dmdbr4  32795  mdsl1i  32810  mdslmd1lem3  32816  mdslmd1lem4  32817  csmdsymi  32823  hatomic  32849  chrelat2  32859  atord  32877  atcvat4i  32886  fz1nntr  33281  elrgspnlem4  33693  fldgenval  33761  fldgensdrg  33763  fldgenssv  33764  fldgenssp  33767  nsgmgc  33849  nsgqusf1olem2  33851  mxidlmax  33876  ssmxidllem  33884  ssmxidl  33885  dflringlem  33912  1arithufdlem4  33965  reff  34357  cmpcref  34368  zarcls1  34387  zarclsiin  34389  zarclssn  34391  zart0  34397  zarmxt1  34398  zarcmp  34400  rhmpreimacnlem  34402  sigagenval  34659  dmsigagen  34663  sigagenss  34668  ldsysgenld  34679  ldgenpisyslem1  34682  ldgenpisyslem2  34683  dynkin  34686  carsgmon  34833  carsgclctunlem2  34838  bnj1286  35536  bnj1452  35569  fineqvac  35650  tz9.1regs  35668  onvf1odlem4  35711  vonf1wev  35713  vonf1owevOLD  35715  kur14lem9  35801  mclsssvlem  36149  mclsind  36157  imagesset  36540  altopthsn  36549  fnessref  36984  refssfne  36985  topjoin  36992  neifg  36998  tz9.1tco  37110  ttc00  37135  dfttc3gw  37150  bj-snglex  37725  bj-imdirvallem  37940  relowlssretop  38125  relowlpssretop  38126  exrecfnlem  38141  finxpreclem3  38155  pibt2  38179  poimirlem29  38406  poimir  38410  mblfinlem3  38416  totbndss  38535  heibor1lem  38567  unichnidl  38789  ispridl  38792  maxidlmax  38801  igenval  38819  igenidl  38821  igenmin  38822  igenval2  38824  dfsuccl4  39230  brssr  39337  suceldisj  39574  lsatcmp  39884  lcvexchlem4  39918  lcvexchlem5  39919  pclvalN  40771  pclclN  40772  elpcliN  40774  docaclN  42005  dihglb2  42223  doch2val2  42245  dochocss  42247  dochexmidlem7  42347  lpolconN  42368  mapdval  42509  nacsfix  43565  mzpcompact2  43605  superficl  44415  superuncl  44416  cleq2lem  44456  clcnvlem  44471  dfrtrcl3  44581  clsk1indlem2  44890  neik0pk1imk0  44895  isotone1  44896  isotone2  44897  ntrclsiso  44915  gneispacess2  44994  mnuunid  45109  mnurndlem2  45114  ssrecnpr  45140  founiiun  46019  founiiun0  46030  islptre  46457  salgenval  47157  salgenn0  47167  salgencl  47168  sssalgen  47171  salgenss  47172  salgenuni  47173  issalgend  47174  dfsalgen2  47177  salgencntex  47179  dfclnbgr3  48750  predgclnbgrel  48763  clnbgredg  48764  clnbgrgrimlem  48857  clnbgrgrim  48858  opndisj  49837  opnneilem  49840  sepfsepc  49862  iscnrm3rlem8  49881  iscnrm3llem2  49884  intubeu  49918  ipolubdm  49921  ipoglbdm  49924  setrec1lem1  50621  setrec1lem3  50623  setrec2fun  50626