Theorem sseq2 3956

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 3945	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3936	. . . 4 ⊢ (𝐶 ⊆ 𝐴 → (𝐴 ⊆ 𝐵 → 𝐶 ⊆ 𝐵))
3	2	com12 32	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵))
4		sstr2 3936	. . . 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 1541   ⊆ wss 3897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ss 3914

This theorem is referenced by:  sseq12  3957  sseq2i  3959  sseq2d  3962  nssne1  3992  psseq2  4040  sseq0  4352  un00  4394  disjpss  4410  pweqALT  4564  ssintab  4915  ssintub  4916  intmin  4918  treq  5207  al0ssb  5248  sseliALT  5249  ssexg  5263  intabs  5289  iunopeqop  5464  onelssex  6361  ordunidif  6362  ordssun  6416  fununi  6562  feq3  6637  ssimaexg  6914  fnssintima  7302  iunpw  7710  tfindsg  7797  limomss  7807  findsg  7833  funcnvuni  7868  frxp  8062  frrlem1  8222  frrlem13  8234  onfununi  8267  oawordeu  8476  oawordexr  8477  nnawordex  8558  eldifsucnn  8585  coflton  8592  cofon1  8593  cofon2  8594  cofonr  8595  naddcllem  8597  naddunif  8614  ereq1  8635  xpider  8718  domeng  8891  sbthlem4  9009  sbthlem5  9010  domssex  9057  ssfi  9088  finsschain  9249  dffi2  9313  dffi3  9321  hartogslem1  9434  inf3lema  9520  cantnflem1  9585  dfttrcl2  9620  tz9.1  9625  tz9.1c  9626  tctr  9634  tcmin  9635  tcrank  9783  scottex  9784  cardlim  9871  infxpenlem  9910  infxpenc2  9919  isinfcard  9989  alephinit  9992  alephval3  10007  dfac3  10018  cflem  10142  cflemOLD  10143  cfval  10144  cflecard  10150  cfsuc  10154  cff1  10155  cfflb  10156  cflim2  10160  isf32lem2  10251  fin1a2lem13  10309  ac7g  10371  ttukeylem5  10410  ttukeylem7  10412  pwcfsdom  10480  pwfseqlem5  10560  pwfseq  10561  gch2  10572  winalim  10592  wunex  10636  wuncss  10642  eltskg  10647  eltsk2g  10648  gruina  10715  grur1a  10716  axgroth6  10725  swrdnd2  14569  trcleq2lem  14904  dfrtrcl2  14975  fprodss  15861  mrcflem  17518  mrcval  17522  isacs2  17565  acsfiel  17566  ipoval  18442  fpwipodrs  18452  ipodrsima  18453  mreclatBAD  18475  slwispgp  19529  pgpssslw  19532  lsmss1b  19584  lsmss2b  19586  cntzcmnss  19759  gsumzres  19827  rgspnval  20533  rgspncl  20534  rgspnmin  20536  lspf  20913  lspval  20914  lbsextlem1  21101  lbsextlem3  21103  lbsextlem4  21104  aspval  21816  mplsubglem  21942  mpllsslem  21943  basis2  22872  eltg2  22879  clsval  22958  clscld  22968  clsval2  22971  ntrcls0  22997  isnei  23024  neiint  23025  neips  23034  opnneissb  23035  opnssneib  23036  neindisj2  23044  innei  23046  neiptoptop  23052  neiptopnei  23053  neitr  23101  restcls  23102  cnpimaex  23177  cnprest2  23211  regsep  23255  nrmsep3  23276  nrmsep  23278  regsep2  23297  tgcmp  23322  uncmp  23324  bwth  23331  1stcfb  23366  1stcrest  23374  2ndcctbss  23376  1stcelcls  23382  lly1stc  23417  ssref  23433  refref  23434  comppfsc  23453  xkoopn  23510  neitx  23528  txcnp  23541  txcmplem1  23562  kqnrmlem1  23664  kqnrmlem2  23665  nrmhmph  23715  fbssfi  23758  opnfbas  23763  fbasfip  23789  fbunfip  23790  fgss2  23795  fgcl  23799  supfil  23816  isufil2  23829  filssufilg  23832  ssufl  23839  ufileu  23840  elfm3  23871  fmfnfm  23879  ufldom  23883  fbflim2  23898  flfneii  23913  flftg  23917  txflf  23927  supnfcls  23941  fclscf  23946  fclsfnflim  23948  flimfnfcls  23949  alexsubALTlem2  23969  alexsubALTlem3  23970  alexsubALTlem4  23971  alexsubALT  23972  tsmsfbas  24049  tsmsres  24065  tsmsf1o  24066  tsmsxplem1  24074  tsmsxp  24076  ustssel  24127  ustincl  24129  ustdiag  24130  ustinvel  24131  ustexhalf  24132  ust0  24141  elutop  24154  ustuqtop4  24165  cfiluexsm  24210  cfiluweak  24215  blssps  24345  blss  24346  metss  24429  metrest  24445  metcnp3  24461  metnrmlem3  24783  lebnumlem3  24895  lebnum  24896  ellimc3  25813  lhop1lem  25951  dchrelbas  27180  eqscut2  27753  scutun12  27757  madebdayim  27839  madebday  27851  onsiso  28211  bdayn0p1  28300  upgredgpr  29127  dfnbgr3  29323  nbupgr  29329  nbumgrvtx  29331  nbgr2vtx1edg  29335  nbuhgr2vtx1edgb  29337  cusgrexilem2  29427  wlkvtxiedg  29610  wlkres  29654  upgr1wlkdlem2  30133  1pthon2v  30140  1pthon2ve  30141  cusconngr  30178  isfrgr  30247  avril1  30450  spanval  31320  spancl  31323  shsval2i  31374  omlsi  31391  ococin  31395  chsupsn  31400  pjoml  31423  shs00i  31437  chj00i  31474  chsscon3  31487  chlejb1  31499  chnle  31501  pjoml2  31598  pjoml3  31599  lecm  31604  stcltr1i  32261  mdbr  32281  dmdmd  32287  dmdi  32289  dmdbr3  32292  dmdbr4  32293  mdsl1i  32308  mdslmd1lem3  32314  mdslmd1lem4  32315  csmdsymi  32321  hatomic  32347  chrelat2  32357  atord  32375  atcvat4i  32384  fz1nntr  32791  elrgspnlem4  33219  fldgenval  33285  fldgensdrg  33287  fldgenssv  33288  fldgenssp  33291  nsgmgc  33384  nsgqusf1olem2  33386  isprmidl  33410  ssdifidllem  33428  ssdifidl  33429  ssdifidlprm  33430  mxidlmax  33437  ssmxidllem  33445  ssmxidl  33446  1arithufdlem4  33519  reff  33859  cmpcref  33870  zarcls1  33889  zarclsiin  33891  zarclssn  33893  zart0  33899  zarmxt1  33900  zarcmp  33902  rhmpreimacnlem  33904  sigagenval  34160  dmsigagen  34164  sigagenss  34169  ldsysgenld  34180  ldgenpisyslem1  34183  ldgenpisyslem2  34184  dynkin  34187  carsgmon  34334  carsgclctunlem2  34339  bnj1286  35038  bnj1452  35071  tz9.1regs  35137  fineqvac  35146  onvf1odlem4  35157  vonf1owev  35159  kur14lem9  35265  mclsssvlem  35613  mclsind  35621  imagesset  36004  altopthsn  36012  fnessref  36408  refssfne  36409  topjoin  36416  neifg  36422  bj-snglex  37024  bj-imdirvallem  37231  relowlssretop  37414  relowlpssretop  37415  exrecfnlem  37430  finxpreclem3  37444  pibt2  37468  poimirlem29  37695  poimir  37699  mblfinlem3  37705  totbndss  37823  heibor1lem  37855  unichnidl  38077  ispridl  38080  maxidlmax  38089  igenval  38107  igenidl  38109  igenmin  38110  igenval2  38112  dfsuccl4  38493  brssr  38599  lsatcmp  39108  lcvexchlem4  39142  lcvexchlem5  39143  pclvalN  39995  pclclN  39996  elpcliN  39998  docaclN  41229  dihglb2  41447  doch2val2  41469  dochocss  41471  dochexmidlem7  41571  lpolconN  41592  mapdval  41733  nacsfix  42810  mzpcompact2  42850  superficl  43665  superuncl  43666  cleq2lem  43706  clcnvlem  43721  dfrtrcl3  43831  clsk1indlem2  44140  neik0pk1imk0  44145  isotone1  44146  isotone2  44147  ntrclsiso  44165  gneispacess2  44244  mnuunid  44375  mnurndlem2  44380  ssrecnpr  44406  founiiun  45281  founiiun0  45292  islptre  45724  salgenval  46424  salgenn0  46434  salgencl  46435  sssalgen  46438  salgenss  46439  salgenuni  46440  issalgend  46441  dfsalgen2  46444  salgencntex  46446  dfclnbgr3  47931  predgclnbgrel  47944  clnbgredg  47945  clnbgrgrimlem  48038  clnbgrgrim  48039  opndisj  49008  opnneilem  49011  sepfsepc  49033  iscnrm3rlem8  49052  iscnrm3llem2  49055  intubeu  49089  ipolubdm  49092  ipoglbdm  49095  setrec1lem1  49793  setrec1lem3  49795  setrec2fun  49798