Theorem sseq2 3949

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

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 3907

This theorem is referenced by:  sseq12  3950  sseq2i  3952  sseq2d  3955  nssne1  3985  psseq2  4032  sseq0  4344  un00  4386  disjpss  4402  pweqALT  4557  ssintab  4908  ssintub  4909  intmin  4911  treq  5200  al0ssb  5243  sseliALT  5244  ssexg  5260  intabs  5286  iunopeqop  5469  onelssex  6366  ordunidif  6367  ordssun  6421  fununi  6567  feq3  6642  ssimaexg  6920  fnssintima  7310  iunpw  7718  tfindsg  7805  limomss  7815  findsg  7841  funcnvuni  7876  frxp  8069  frrlem1  8229  frrlem13  8241  onfununi  8274  oawordeu  8483  oawordexr  8484  nnawordex  8566  eldifsucnn  8593  coflton  8600  cofon1  8601  cofon2  8602  cofonr  8603  naddcllem  8605  naddunif  8622  ereq1  8644  xpider  8728  domeng  8902  sbthlem4  9021  sbthlem5  9022  domssex  9069  ssfi  9100  finsschain  9262  dffi2  9329  dffi3  9337  hartogslem1  9450  inf3lema  9536  cantnflem1  9601  dfttrcl2  9636  tz9.1  9641  tz9.1c  9642  tctr  9650  tcmin  9651  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  10497  pwfseqlem5  10577  pwfseq  10578  gch2  10589  winalim  10609  wunex  10653  wuncss  10659  eltskg  10664  eltsk2g  10665  gruina  10732  grur1a  10733  axgroth6  10742  swrdnd2  14609  trcleq2lem  14944  dfrtrcl2  15015  fprodss  15904  mrcflem  17563  mrcval  17567  isacs2  17610  acsfiel  17611  ipoval  18487  fpwipodrs  18497  ipodrsima  18498  mreclatBAD  18520  slwispgp  19577  pgpssslw  19580  lsmss1b  19632  lsmss2b  19634  cntzcmnss  19807  gsumzres  19875  rgspnval  20580  rgspncl  20581  rgspnmin  20583  lspf  20960  lspval  20961  lbsextlem1  21148  lbsextlem3  21150  lbsextlem4  21151  aspval  21862  mplsubglem  21987  mpllsslem  21988  basis2  22926  eltg2  22933  clsval  23012  clscld  23022  clsval2  23025  ntrcls0  23051  isnei  23078  neiint  23079  neips  23088  opnneissb  23089  opnssneib  23090  neindisj2  23098  innei  23100  neiptoptop  23106  neiptopnei  23107  neitr  23155  restcls  23156  cnpimaex  23231  cnprest2  23265  regsep  23309  nrmsep3  23330  nrmsep  23332  regsep2  23351  tgcmp  23376  uncmp  23378  bwth  23385  1stcfb  23420  1stcrest  23428  2ndcctbss  23430  1stcelcls  23436  lly1stc  23471  ssref  23487  refref  23488  comppfsc  23507  xkoopn  23564  neitx  23582  txcnp  23595  txcmplem1  23616  kqnrmlem1  23718  kqnrmlem2  23719  nrmhmph  23769  fbssfi  23812  opnfbas  23817  fbasfip  23843  fbunfip  23844  fgss2  23849  fgcl  23853  supfil  23870  isufil2  23883  filssufilg  23886  ssufl  23893  ufileu  23894  elfm3  23925  fmfnfm  23933  ufldom  23937  fbflim2  23952  flfneii  23967  flftg  23971  txflf  23981  supnfcls  23995  fclscf  24000  fclsfnflim  24002  flimfnfcls  24003  alexsubALTlem2  24023  alexsubALTlem3  24024  alexsubALTlem4  24025  alexsubALT  24026  tsmsfbas  24103  tsmsres  24119  tsmsf1o  24120  tsmsxplem1  24128  tsmsxp  24130  ustssel  24181  ustincl  24183  ustdiag  24184  ustinvel  24185  ustexhalf  24186  ust0  24195  elutop  24208  ustuqtop4  24219  cfiluexsm  24264  cfiluweak  24269  blssps  24399  blss  24400  metss  24483  metrest  24499  metcnp3  24515  metnrmlem3  24837  lebnumlem3  24940  lebnum  24941  ellimc3  25856  lhop1lem  25990  dchrelbas  27213  eqcuts2  27792  cutsun12  27796  madebdayim  27894  madebday  27906  oniso  28277  bdayn0p1  28375  upgredgpr  29225  dfnbgr3  29421  nbupgr  29427  nbumgrvtx  29429  nbgr2vtx1edg  29433  nbuhgr2vtx1edgb  29435  cusgrexilem2  29525  wlkvtxiedg  29708  wlkres  29752  upgr1wlkdlem2  30231  1pthon2v  30238  1pthon2ve  30239  cusconngr  30276  isfrgr  30345  avril1  30548  spanval  31419  spancl  31422  shsval2i  31473  omlsi  31490  ococin  31494  chsupsn  31499  pjoml  31522  shs00i  31536  chj00i  31573  chsscon3  31586  chlejb1  31598  chnle  31600  pjoml2  31697  pjoml3  31698  lecm  31703  stcltr1i  32360  mdbr  32380  dmdmd  32386  dmdi  32388  dmdbr3  32391  dmdbr4  32392  mdsl1i  32407  mdslmd1lem3  32413  mdslmd1lem4  32414  csmdsymi  32420  hatomic  32446  chrelat2  32456  atord  32474  atcvat4i  32483  fz1nntr  32890  elrgspnlem4  33321  fldgenval  33388  fldgensdrg  33390  fldgenssv  33391  fldgenssp  33394  nsgmgc  33487  nsgqusf1olem2  33489  isprmidl  33513  ssdifidllem  33531  ssdifidl  33532  ssdifidlprm  33533  mxidlmax  33540  ssmxidllem  33548  ssmxidl  33549  1arithufdlem4  33622  reff  33999  cmpcref  34010  zarcls1  34029  zarclsiin  34031  zarclssn  34033  zart0  34039  zarmxt1  34040  zarcmp  34042  rhmpreimacnlem  34044  sigagenval  34300  dmsigagen  34304  sigagenss  34309  ldsysgenld  34320  ldgenpisyslem1  34323  ldgenpisyslem2  34324  dynkin  34327  carsgmon  34474  carsgclctunlem2  34479  bnj1286  35177  bnj1452  35210  fineqvac  35276  tz9.1regs  35294  onvf1odlem4  35304  vonf1owev  35306  kur14lem9  35412  mclsssvlem  35760  mclsind  35768  imagesset  36151  altopthsn  36159  fnessref  36555  refssfne  36556  topjoin  36563  neifg  36569  tz9.1tco  36681  ttc00  36706  dfttc3gw  36721  bj-snglex  37296  bj-imdirvallem  37510  relowlssretop  37693  relowlpssretop  37694  exrecfnlem  37709  finxpreclem3  37723  pibt2  37747  poimirlem29  37984  poimir  37988  mblfinlem3  37994  totbndss  38112  heibor1lem  38144  unichnidl  38366  ispridl  38369  maxidlmax  38378  igenval  38396  igenidl  38398  igenmin  38399  igenval2  38401  dfsuccl4  38809  brssr  38916  suceldisj  39153  lsatcmp  39463  lcvexchlem4  39497  lcvexchlem5  39498  pclvalN  40350  pclclN  40351  elpcliN  40353  docaclN  41584  dihglb2  41802  doch2val2  41824  dochocss  41826  dochexmidlem7  41926  lpolconN  41947  mapdval  42088  nacsfix  43158  mzpcompact2  43198  superficl  44012  superuncl  44013  cleq2lem  44053  clcnvlem  44068  dfrtrcl3  44178  clsk1indlem2  44487  neik0pk1imk0  44492  isotone1  44493  isotone2  44494  ntrclsiso  44512  gneispacess2  44591  mnuunid  44722  mnurndlem2  44727  ssrecnpr  44753  founiiun  45627  founiiun0  45638  islptre  46067  salgenval  46767  salgenn0  46777  salgencl  46778  sssalgen  46781  salgenss  46782  salgenuni  46783  issalgend  46784  dfsalgen2  46787  salgencntex  46789  dfclnbgr3  48314  predgclnbgrel  48327  clnbgredg  48328  clnbgrgrimlem  48421  clnbgrgrim  48422  opndisj  49390  opnneilem  49393  sepfsepc  49415  iscnrm3rlem8  49434  iscnrm3llem2  49437  intubeu  49471  ipolubdm  49474  ipoglbdm  49477  setrec1lem1  50174  setrec1lem3  50176  setrec2fun  50179