Theorem sseq2 3948

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

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

This theorem is referenced by:  sseq12  3949  sseq2i  3951  sseq2d  3954  nssne1  3984  psseq2  4031  sseq0  4343  un00  4385  disjpss  4401  pweqALT  4556  ssintab  4907  ssintub  4908  intmin  4910  treq  5199  al0ssb  5243  sseliALT  5244  ssexg  5264  intabs  5290  iunopeqop  5475  iunopeqopOLD  5476  onelssex  6372  ordunidif  6373  ordssun  6427  fununi  6573  feq3  6648  ssimaexg  6926  fnssintima  7317  iunpw  7725  tfindsg  7812  limomss  7822  findsg  7848  funcnvuni  7883  frxp  8076  frrlem1  8236  frrlem13  8248  onfununi  8281  oawordeu  8490  oawordexr  8491  nnawordex  8573  eldifsucnn  8600  coflton  8607  cofon1  8608  cofon2  8609  cofonr  8610  naddcllem  8612  naddunif  8629  ereq1  8651  xpider  8735  domeng  8909  sbthlem4  9028  sbthlem5  9029  domssex  9076  ssfi  9107  finsschain  9269  dffi2  9336  dffi3  9344  hartogslem1  9457  inf3lema  9545  cantnflem1  9610  dfttrcl2  9645  tz9.1  9650  tz9.1c  9651  tctr  9659  tcmin  9660  tcrank  9808  scottex  9809  cardlim  9896  infxpenlem  9935  infxpenc2  9944  isinfcard  10014  alephinit  10017  alephval3  10032  dfac3  10043  cflem  10167  cflemOLD  10168  cfval  10169  cflecard  10175  cfsuc  10179  cff1  10180  cfflb  10181  cflim2  10185  isf32lem2  10276  fin1a2lem13  10334  ac7g  10396  ttukeylem5  10435  ttukeylem7  10437  pwcfsdom  10506  pwfseqlem5  10586  pwfseq  10587  gch2  10598  winalim  10618  wunex  10662  wuncss  10668  eltskg  10673  eltsk2g  10674  gruina  10741  grur1a  10742  axgroth6  10751  swrdnd2  14618  trcleq2lem  14953  dfrtrcl2  15024  fprodss  15913  mrcflem  17572  mrcval  17576  isacs2  17619  acsfiel  17620  ipoval  18496  fpwipodrs  18506  ipodrsima  18507  mreclatBAD  18529  slwispgp  19586  pgpssslw  19589  lsmss1b  19641  lsmss2b  19643  cntzcmnss  19816  gsumzres  19884  rgspnval  20589  rgspncl  20590  rgspnmin  20592  lspf  20969  lspval  20970  lbsextlem1  21156  lbsextlem3  21158  lbsextlem4  21159  aspval  21852  mplsubglem  21977  mpllsslem  21978  basis2  22916  eltg2  22923  clsval  23002  clscld  23012  clsval2  23015  ntrcls0  23041  isnei  23068  neiint  23069  neips  23078  opnneissb  23079  opnssneib  23080  neindisj2  23088  innei  23090  neiptoptop  23096  neiptopnei  23097  neitr  23145  restcls  23146  cnpimaex  23221  cnprest2  23255  regsep  23299  nrmsep3  23320  nrmsep  23322  regsep2  23341  tgcmp  23366  uncmp  23368  bwth  23375  1stcfb  23410  1stcrest  23418  2ndcctbss  23420  1stcelcls  23426  lly1stc  23461  ssref  23477  refref  23478  comppfsc  23497  xkoopn  23554  neitx  23572  txcnp  23585  txcmplem1  23606  kqnrmlem1  23708  kqnrmlem2  23709  nrmhmph  23759  fbssfi  23802  opnfbas  23807  fbasfip  23833  fbunfip  23834  fgss2  23839  fgcl  23843  supfil  23860  isufil2  23873  filssufilg  23876  ssufl  23883  ufileu  23884  elfm3  23915  fmfnfm  23923  ufldom  23927  fbflim2  23942  flfneii  23957  flftg  23961  txflf  23971  supnfcls  23985  fclscf  23990  fclsfnflim  23992  flimfnfcls  23993  alexsubALTlem2  24013  alexsubALTlem3  24014  alexsubALTlem4  24015  alexsubALT  24016  tsmsfbas  24093  tsmsres  24109  tsmsf1o  24110  tsmsxplem1  24118  tsmsxp  24120  ustssel  24171  ustincl  24173  ustdiag  24174  ustinvel  24175  ustexhalf  24176  ust0  24185  elutop  24198  ustuqtop4  24209  cfiluexsm  24254  cfiluweak  24259  blssps  24389  blss  24390  metss  24473  metrest  24489  metcnp3  24505  metnrmlem3  24827  lebnumlem3  24930  lebnum  24931  ellimc3  25846  lhop1lem  25980  dchrelbas  27199  eqcuts2  27778  cutsun12  27782  madebdayim  27880  madebday  27892  oniso  28263  bdayn0p1  28361  upgredgpr  29211  dfnbgr3  29407  nbupgr  29413  nbumgrvtx  29415  nbgr2vtx1edg  29419  nbuhgr2vtx1edgb  29421  cusgrexilem2  29511  wlkvtxiedg  29693  wlkres  29737  upgr1wlkdlem2  30216  1pthon2v  30223  1pthon2ve  30224  cusconngr  30261  isfrgr  30330  avril1  30533  spanval  31404  spancl  31407  shsval2i  31458  omlsi  31475  ococin  31479  chsupsn  31484  pjoml  31507  shs00i  31521  chj00i  31558  chsscon3  31571  chlejb1  31583  chnle  31585  pjoml2  31682  pjoml3  31683  lecm  31688  stcltr1i  32345  mdbr  32365  dmdmd  32371  dmdi  32373  dmdbr3  32376  dmdbr4  32377  mdsl1i  32392  mdslmd1lem3  32398  mdslmd1lem4  32399  csmdsymi  32405  hatomic  32431  chrelat2  32441  atord  32459  atcvat4i  32468  fz1nntr  32875  elrgspnlem4  33306  fldgenval  33373  fldgensdrg  33375  fldgenssv  33376  fldgenssp  33379  nsgmgc  33472  nsgqusf1olem2  33474  isprmidl  33498  ssdifidllem  33516  ssdifidl  33517  ssdifidlprm  33518  mxidlmax  33525  ssmxidllem  33533  ssmxidl  33534  1arithufdlem4  33607  reff  33983  cmpcref  33994  zarcls1  34013  zarclsiin  34015  zarclssn  34017  zart0  34023  zarmxt1  34024  zarcmp  34026  rhmpreimacnlem  34028  sigagenval  34284  dmsigagen  34288  sigagenss  34293  ldsysgenld  34304  ldgenpisyslem1  34307  ldgenpisyslem2  34308  dynkin  34311  carsgmon  34458  carsgclctunlem2  34463  bnj1286  35161  bnj1452  35194  fineqvac  35260  tz9.1regs  35278  onvf1odlem4  35288  vonf1owev  35290  kur14lem9  35396  mclsssvlem  35744  mclsind  35752  imagesset  36135  altopthsn  36143  fnessref  36539  refssfne  36540  topjoin  36547  neifg  36553  tz9.1tco  36665  ttc00  36690  dfttc3gw  36705  bj-snglex  37280  bj-imdirvallem  37494  relowlssretop  37679  relowlpssretop  37680  exrecfnlem  37695  finxpreclem3  37709  pibt2  37733  poimirlem29  37970  poimir  37974  mblfinlem3  37980  totbndss  38098  heibor1lem  38130  unichnidl  38352  ispridl  38355  maxidlmax  38364  igenval  38382  igenidl  38384  igenmin  38385  igenval2  38387  dfsuccl4  38795  brssr  38902  suceldisj  39139  lsatcmp  39449  lcvexchlem4  39483  lcvexchlem5  39484  pclvalN  40336  pclclN  40337  elpcliN  40339  docaclN  41570  dihglb2  41788  doch2val2  41810  dochocss  41812  dochexmidlem7  41912  lpolconN  41933  mapdval  42074  nacsfix  43144  mzpcompact2  43184  superficl  43994  superuncl  43995  cleq2lem  44035  clcnvlem  44050  dfrtrcl3  44160  clsk1indlem2  44469  neik0pk1imk0  44474  isotone1  44475  isotone2  44476  ntrclsiso  44494  gneispacess2  44573  mnuunid  44704  mnurndlem2  44709  ssrecnpr  44735  founiiun  45609  founiiun0  45620  islptre  46049  salgenval  46749  salgenn0  46759  salgencl  46760  sssalgen  46763  salgenss  46764  salgenuni  46765  issalgend  46766  dfsalgen2  46769  salgencntex  46771  dfclnbgr3  48302  predgclnbgrel  48315  clnbgredg  48316  clnbgrgrimlem  48409  clnbgrgrim  48410  opndisj  49378  opnneilem  49381  sepfsepc  49403  iscnrm3rlem8  49422  iscnrm3llem2  49425  intubeu  49459  ipolubdm  49462  ipoglbdm  49465  setrec1lem1  50162  setrec1lem3  50164  setrec2fun  50167