Theorem sseq2 3962

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 3951	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3942	. . . 4 ⊢ (𝐶 ⊆ 𝐴 → (𝐴 ⊆ 𝐵 → 𝐶 ⊆ 𝐵))
3	2	com12 32	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵))
4		sstr2 3942	. . . 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 3903

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 2709

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

This theorem is referenced by:  sseq12  3963  sseq2i  3965  sseq2d  3968  nssne1  3998  psseq2  4045  sseq0  4357  un00  4399  disjpss  4415  pweqALT  4571  ssintab  4922  ssintub  4923  intmin  4925  treq  5214  al0ssb  5255  sseliALT  5256  ssexg  5270  intabs  5296  iunopeqop  5477  onelssex  6374  ordunidif  6375  ordssun  6429  fununi  6575  feq3  6650  ssimaexg  6928  fnssintima  7318  iunpw  7726  tfindsg  7813  limomss  7823  findsg  7849  funcnvuni  7884  frxp  8078  frrlem1  8238  frrlem13  8250  onfununi  8283  oawordeu  8492  oawordexr  8493  nnawordex  8575  eldifsucnn  8602  coflton  8609  cofon1  8610  cofon2  8611  cofonr  8612  naddcllem  8614  naddunif  8631  ereq1  8653  xpider  8737  domeng  8911  sbthlem4  9030  sbthlem5  9031  domssex  9078  ssfi  9109  finsschain  9271  dffi2  9338  dffi3  9346  hartogslem1  9459  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  14591  trcleq2lem  14926  dfrtrcl2  14997  fprodss  15883  mrcflem  17541  mrcval  17545  isacs2  17588  acsfiel  17589  ipoval  18465  fpwipodrs  18475  ipodrsima  18476  mreclatBAD  18498  slwispgp  19552  pgpssslw  19555  lsmss1b  19607  lsmss2b  19609  cntzcmnss  19782  gsumzres  19850  rgspnval  20557  rgspncl  20558  rgspnmin  20560  lspf  20937  lspval  20938  lbsextlem1  21125  lbsextlem3  21127  lbsextlem4  21128  aspval  21840  mplsubglem  21966  mpllsslem  21967  basis2  22907  eltg2  22914  clsval  22993  clscld  23003  clsval2  23006  ntrcls0  23032  isnei  23059  neiint  23060  neips  23069  opnneissb  23070  opnssneib  23071  neindisj2  23079  innei  23081  neiptoptop  23087  neiptopnei  23088  neitr  23136  restcls  23137  cnpimaex  23212  cnprest2  23246  regsep  23290  nrmsep3  23311  nrmsep  23313  regsep2  23332  tgcmp  23357  uncmp  23359  bwth  23366  1stcfb  23401  1stcrest  23409  2ndcctbss  23411  1stcelcls  23417  lly1stc  23452  ssref  23468  refref  23469  comppfsc  23488  xkoopn  23545  neitx  23563  txcnp  23576  txcmplem1  23597  kqnrmlem1  23699  kqnrmlem2  23700  nrmhmph  23750  fbssfi  23793  opnfbas  23798  fbasfip  23824  fbunfip  23825  fgss2  23830  fgcl  23834  supfil  23851  isufil2  23864  filssufilg  23867  ssufl  23874  ufileu  23875  elfm3  23906  fmfnfm  23914  ufldom  23918  fbflim2  23933  flfneii  23948  flftg  23952  txflf  23962  supnfcls  23976  fclscf  23981  fclsfnflim  23983  flimfnfcls  23984  alexsubALTlem2  24004  alexsubALTlem3  24005  alexsubALTlem4  24006  alexsubALT  24007  tsmsfbas  24084  tsmsres  24100  tsmsf1o  24101  tsmsxplem1  24109  tsmsxp  24111  ustssel  24162  ustincl  24164  ustdiag  24165  ustinvel  24166  ustexhalf  24167  ust0  24176  elutop  24189  ustuqtop4  24200  cfiluexsm  24245  cfiluweak  24250  blssps  24380  blss  24381  metss  24464  metrest  24480  metcnp3  24496  metnrmlem3  24818  lebnumlem3  24930  lebnum  24931  ellimc3  25848  lhop1lem  25986  dchrelbas  27215  eqcuts2  27794  cutsun12  27798  madebdayim  27896  madebday  27908  oniso  28279  bdayn0p1  28377  upgredgpr  29227  dfnbgr3  29423  nbupgr  29429  nbumgrvtx  29431  nbgr2vtx1edg  29435  nbuhgr2vtx1edgb  29437  cusgrexilem2  29527  wlkvtxiedg  29710  wlkres  29754  upgr1wlkdlem2  30233  1pthon2v  30240  1pthon2ve  30241  cusconngr  30278  isfrgr  30347  avril1  30550  spanval  31420  spancl  31423  shsval2i  31474  omlsi  31491  ococin  31495  chsupsn  31500  pjoml  31523  shs00i  31537  chj00i  31574  chsscon3  31587  chlejb1  31599  chnle  31601  pjoml2  31698  pjoml3  31699  lecm  31704  stcltr1i  32361  mdbr  32381  dmdmd  32387  dmdi  32389  dmdbr3  32392  dmdbr4  32393  mdsl1i  32408  mdslmd1lem3  32414  mdslmd1lem4  32415  csmdsymi  32421  hatomic  32447  chrelat2  32457  atord  32475  atcvat4i  32484  fz1nntr  32892  elrgspnlem4  33338  fldgenval  33405  fldgensdrg  33407  fldgenssv  33408  fldgenssp  33411  nsgmgc  33504  nsgqusf1olem2  33506  isprmidl  33530  ssdifidllem  33548  ssdifidl  33549  ssdifidlprm  33550  mxidlmax  33557  ssmxidllem  33565  ssmxidl  33566  1arithufdlem4  33639  reff  34016  cmpcref  34027  zarcls1  34046  zarclsiin  34048  zarclssn  34050  zart0  34056  zarmxt1  34057  zarcmp  34059  rhmpreimacnlem  34061  sigagenval  34317  dmsigagen  34321  sigagenss  34326  ldsysgenld  34337  ldgenpisyslem1  34340  ldgenpisyslem2  34341  dynkin  34344  carsgmon  34491  carsgclctunlem2  34496  bnj1286  35194  bnj1452  35227  fineqvac  35291  tz9.1regs  35309  onvf1odlem4  35319  vonf1owev  35321  kur14lem9  35427  mclsssvlem  35775  mclsind  35783  imagesset  36166  altopthsn  36174  fnessref  36570  refssfne  36571  topjoin  36578  neifg  36584  bj-snglex  37218  bj-imdirvallem  37432  relowlssretop  37615  relowlpssretop  37616  exrecfnlem  37631  finxpreclem3  37645  pibt2  37669  poimirlem29  37897  poimir  37901  mblfinlem3  37907  totbndss  38025  heibor1lem  38057  unichnidl  38279  ispridl  38282  maxidlmax  38291  igenval  38309  igenidl  38311  igenmin  38312  igenval2  38314  dfsuccl4  38722  brssr  38829  suceldisj  39066  lsatcmp  39376  lcvexchlem4  39410  lcvexchlem5  39411  pclvalN  40263  pclclN  40264  elpcliN  40266  docaclN  41497  dihglb2  41715  doch2val2  41737  dochocss  41739  dochexmidlem7  41839  lpolconN  41860  mapdval  42001  nacsfix  43066  mzpcompact2  43106  superficl  43920  superuncl  43921  cleq2lem  43961  clcnvlem  43976  dfrtrcl3  44086  clsk1indlem2  44395  neik0pk1imk0  44400  isotone1  44401  isotone2  44402  ntrclsiso  44420  gneispacess2  44499  mnuunid  44630  mnurndlem2  44635  ssrecnpr  44661  founiiun  45535  founiiun0  45546  islptre  45976  salgenval  46676  salgenn0  46686  salgencl  46687  sssalgen  46690  salgenss  46691  salgenuni  46692  issalgend  46693  dfsalgen2  46696  salgencntex  46698  dfclnbgr3  48183  predgclnbgrel  48196  clnbgredg  48197  clnbgrgrimlem  48290  clnbgrgrim  48291  opndisj  49259  opnneilem  49262  sepfsepc  49284  iscnrm3rlem8  49303  iscnrm3llem2  49306  intubeu  49340  ipolubdm  49343  ipoglbdm  49346  setrec1lem1  50043  setrec1lem3  50045  setrec2fun  50048