Theorem sseq2 3964

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 3953	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3944	. . . 4 ⊢ (𝐶 ⊆ 𝐴 → (𝐴 ⊆ 𝐵 → 𝐶 ⊆ 𝐵))
3	2	com12 32	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵))
4		sstr2 3944	. . . 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 1540   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3922

This theorem is referenced by:  sseq12  3965  sseq2i  3967  sseq2d  3970  nssne1  4000  psseq2  4044  sseq0  4356  un00  4398  disjpss  4414  pweqALT  4568  ssintab  4918  ssintub  4919  intmin  4921  treq  5209  al0ssb  5250  sseliALT  5251  ssexg  5265  intabs  5291  iunopeqop  5468  onelssex  6360  ordunidif  6361  ordssun  6415  fununi  6561  feq3  6636  ssimaexg  6913  fnssintima  7303  iunpw  7711  tfindsg  7801  limomss  7811  findsg  7837  funcnvuni  7872  frxp  8066  frrlem1  8226  frrlem13  8238  onfununi  8271  oawordeu  8480  oawordexr  8481  nnawordex  8562  eldifsucnn  8589  coflton  8596  cofon1  8597  cofon2  8598  cofonr  8599  naddcllem  8601  naddunif  8618  ereq1  8639  xpider  8722  domeng  8895  sbthlem4  9014  sbthlem5  9015  domssex  9062  ssfi  9097  finsschain  9268  dffi2  9332  dffi3  9340  hartogslem1  9453  inf3lema  9539  cantnflem1  9604  dfttrcl2  9639  tz9.1  9644  tz9.1c  9645  tctr  9655  tcmin  9656  tcrank  9799  scottex  9800  cardlim  9887  infxpenlem  9926  infxpenc2  9935  isinfcard  10005  alephinit  10008  alephval3  10023  dfac3  10034  cflem  10158  cflemOLD  10159  cfval  10160  cflecard  10166  cfsuc  10170  cff1  10171  cfflb  10172  cflim2  10176  isf32lem2  10267  fin1a2lem13  10325  ac7g  10387  ttukeylem5  10426  ttukeylem7  10428  pwcfsdom  10496  pwfseqlem5  10576  pwfseq  10577  gch2  10588  winalim  10608  wunex  10652  wuncss  10658  eltskg  10663  eltsk2g  10664  gruina  10731  grur1a  10732  axgroth6  10741  swrdnd2  14580  trcleq2lem  14916  dfrtrcl2  14987  fprodss  15873  mrcflem  17530  mrcval  17534  isacs2  17577  acsfiel  17578  ipoval  18454  fpwipodrs  18464  ipodrsima  18465  mreclatBAD  18487  slwispgp  19508  pgpssslw  19511  lsmss1b  19563  lsmss2b  19565  cntzcmnss  19738  gsumzres  19806  rgspnval  20515  rgspncl  20516  rgspnmin  20518  lspf  20895  lspval  20896  lbsextlem1  21083  lbsextlem3  21085  lbsextlem4  21086  aspval  21798  mplsubglem  21924  mpllsslem  21925  basis2  22854  eltg2  22861  clsval  22940  clscld  22950  clsval2  22953  ntrcls0  22979  isnei  23006  neiint  23007  neips  23016  opnneissb  23017  opnssneib  23018  neindisj2  23026  innei  23028  neiptoptop  23034  neiptopnei  23035  neitr  23083  restcls  23084  cnpimaex  23159  cnprest2  23193  regsep  23237  nrmsep3  23258  nrmsep  23260  regsep2  23279  tgcmp  23304  uncmp  23306  bwth  23313  1stcfb  23348  1stcrest  23356  2ndcctbss  23358  1stcelcls  23364  lly1stc  23399  ssref  23415  refref  23416  comppfsc  23435  xkoopn  23492  neitx  23510  txcnp  23523  txcmplem1  23544  kqnrmlem1  23646  kqnrmlem2  23647  nrmhmph  23697  fbssfi  23740  opnfbas  23745  fbasfip  23771  fbunfip  23772  fgss2  23777  fgcl  23781  supfil  23798  isufil2  23811  filssufilg  23814  ssufl  23821  ufileu  23822  elfm3  23853  fmfnfm  23861  ufldom  23865  fbflim2  23880  flfneii  23895  flftg  23899  txflf  23909  supnfcls  23923  fclscf  23928  fclsfnflim  23930  flimfnfcls  23931  alexsubALTlem2  23951  alexsubALTlem3  23952  alexsubALTlem4  23953  alexsubALT  23954  tsmsfbas  24031  tsmsres  24047  tsmsf1o  24048  tsmsxplem1  24056  tsmsxp  24058  ustssel  24109  ustincl  24111  ustdiag  24112  ustinvel  24113  ustexhalf  24114  ust0  24123  elutop  24137  ustuqtop4  24148  cfiluexsm  24193  cfiluweak  24198  blssps  24328  blss  24329  metss  24412  metrest  24428  metcnp3  24444  metnrmlem3  24766  lebnumlem3  24878  lebnum  24879  ellimc3  25796  lhop1lem  25934  dchrelbas  27163  eqscut2  27735  scutun12  27739  madebdayim  27820  madebday  27832  onsiso  28192  bdayn0p1  28281  upgredgpr  29105  dfnbgr3  29301  nbupgr  29307  nbumgrvtx  29309  nbgr2vtx1edg  29313  nbuhgr2vtx1edgb  29315  cusgrexilem2  29405  wlkvtxiedg  29588  wlkres  29632  upgr1wlkdlem2  30108  1pthon2v  30115  1pthon2ve  30116  cusconngr  30153  isfrgr  30222  avril1  30425  spanval  31295  spancl  31298  shsval2i  31349  omlsi  31366  ococin  31370  chsupsn  31375  pjoml  31398  shs00i  31412  chj00i  31449  chsscon3  31462  chlejb1  31474  chnle  31476  pjoml2  31573  pjoml3  31574  lecm  31579  stcltr1i  32236  mdbr  32256  dmdmd  32262  dmdi  32264  dmdbr3  32267  dmdbr4  32268  mdsl1i  32283  mdslmd1lem3  32289  mdslmd1lem4  32290  csmdsymi  32296  hatomic  32322  chrelat2  32332  atord  32350  atcvat4i  32359  fz1nntr  32760  elrgspnlem4  33198  fldgenval  33264  fldgensdrg  33266  fldgenssv  33267  fldgenssp  33270  nsgmgc  33362  nsgqusf1olem2  33364  isprmidl  33388  ssdifidllem  33406  ssdifidl  33407  ssdifidlprm  33408  mxidlmax  33415  ssmxidllem  33423  ssmxidl  33424  1arithufdlem4  33497  reff  33808  cmpcref  33819  zarcls1  33838  zarclsiin  33840  zarclssn  33842  zart0  33848  zarmxt1  33849  zarcmp  33851  rhmpreimacnlem  33853  sigagenval  34109  dmsigagen  34113  sigagenss  34118  ldsysgenld  34129  ldgenpisyslem1  34132  ldgenpisyslem2  34133  dynkin  34136  carsgmon  34284  carsgclctunlem2  34289  bnj1286  34988  bnj1452  35021  tz9.1regs  35069  fineqvac  35074  onvf1odlem4  35081  vonf1owev  35083  kur14lem9  35189  mclsssvlem  35537  mclsind  35545  imagesset  35929  altopthsn  35937  fnessref  36333  refssfne  36334  topjoin  36341  neifg  36347  bj-snglex  36949  bj-imdirvallem  37156  relowlssretop  37339  relowlpssretop  37340  exrecfnlem  37355  finxpreclem3  37369  pibt2  37393  poimirlem29  37631  poimir  37635  mblfinlem3  37641  totbndss  37759  heibor1lem  37791  unichnidl  38013  ispridl  38016  maxidlmax  38025  igenval  38043  igenidl  38045  igenmin  38046  igenval2  38048  brssr  38480  lsatcmp  38984  lcvexchlem4  39018  lcvexchlem5  39019  pclvalN  39872  pclclN  39873  elpcliN  39875  docaclN  41106  dihglb2  41324  doch2val2  41346  dochocss  41348  dochexmidlem7  41448  lpolconN  41469  mapdval  41610  nacsfix  42688  mzpcompact2  42728  superficl  43543  superuncl  43544  cleq2lem  43584  clcnvlem  43599  dfrtrcl3  43709  clsk1indlem2  44018  neik0pk1imk0  44023  isotone1  44024  isotone2  44025  ntrclsiso  44043  gneispacess2  44122  mnuunid  44253  mnurndlem2  44258  ssrecnpr  44284  founiiun  45160  founiiun0  45171  islptre  45604  salgenval  46306  salgenn0  46316  salgencl  46317  sssalgen  46320  salgenss  46321  salgenuni  46322  issalgend  46323  dfsalgen2  46326  salgencntex  46328  dfclnbgr3  47814  predgclnbgrel  47827  clnbgredg  47828  clnbgrgrimlem  47921  clnbgrgrim  47922  opndisj  48891  opnneilem  48894  sepfsepc  48916  iscnrm3rlem8  48935  iscnrm3llem2  48938  intubeu  48972  ipolubdm  48975  ipoglbdm  48978  setrec1lem1  49676  setrec1lem3  49678  setrec2fun  49681