Theorem sseq2 3590

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		sstr2 3575	. . . 4 ⊢ (𝐶 ⊆ 𝐴 → (𝐴 ⊆ 𝐵 → 𝐶 ⊆ 𝐵))
2	1	com12 32	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵))
3		sstr2 3575	. . . 4 ⊢ (𝐶 ⊆ 𝐵 → (𝐵 ⊆ 𝐴 → 𝐶 ⊆ 𝐴))
4	3	com12 32	. . 3 ⊢ (𝐵 ⊆ 𝐴 → (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴))
5	2, 4	anim12i 588	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → ((𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵) ∧ (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴)))
6		eqss 3583	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
7		dfbi2 658	. 2 ⊢ ((𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵) ↔ ((𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵) ∧ (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴)))
8	5, 6, 7	3imtr4i 280	1 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554

This theorem is referenced by:  sseq12  3591  sseq2i  3593  sseq2d  3596  syl5sseq  3616  nssne1  3624  psseq2  3657  sseq0  3927  un00  3963  disjpss  3980  pweq  4111  ssintab  4429  ssintub  4430  intmin  4432  treq  4686  sseliALT  4719  ssexg  4732  intabs  4752  iunopeqop  4906  ordunidif  5690  ordssun  5744  fununi  5878  feq3  5941  ssimaexg  6174  iunpw  6870  tfindsg  6952  limomss  6962  findsg  6985  funcnvuni  7012  frxp  7174  wrecseq123  7295  wfrlem1  7301  wfrlem4  7305  wfrlem15  7316  onfununi  7325  oawordeu  7522  oawordexr  7523  nnawordex  7604  ereq1  7636  xpider  7705  domeng  7855  sbthlem4  7958  sbthlem5  7959  domssex  8006  finsschain  8156  dffi2  8212  dffi3  8220  hartogslem1  8330  inf3lema  8404  cantnflem1  8469  tz9.1  8488  tz9.1c  8489  tctr  8499  tcmin  8500  tcrank  8630  scottex  8631  cardlim  8681  infxpenlem  8719  infxpenc2  8728  isinfcard  8798  alephinit  8801  alephval3  8816  dfac3  8827  cflem  8951  cfval  8952  cflecard  8958  cfsuc  8962  cff1  8963  cfflb  8964  cflim2  8968  isf32lem2  9059  fin1a2lem13  9117  ac7g  9179  ttukeylem5  9218  ttukeylem7  9220  pwcfsdom  9284  pwfseqlem5  9364  pwfseq  9365  gch2  9376  winalim  9396  wunex  9440  wuncss  9446  eltskg  9451  eltsk2g  9452  gruina  9519  grur1a  9520  axgroth6  9529  swrdnd2  13285  trcleq2lem  13578  dfrtrcl2  13650  fprodss  14517  mrcflem  16089  mrcval  16093  isacs2  16137  acsfiel  16138  ipoval  16977  fpwipodrs  16987  ipodrsima  16988  mreclatBAD  17010  slwispgp  17849  pgpssslw  17852  lsmss1b  17903  lsmss2b  17905  cntzcmnss  18069  gsumzres  18133  lspf  18795  lspval  18796  lbsextlem1  18979  lbsextlem3  18981  lbsextlem4  18982  aspval  19149  mplsubglem  19255  mpllsslem  19256  basis2  20566  eltg2  20573  clsval  20651  clscld  20661  clsval2  20664  ntrcls0  20690  isnei  20717  neiint  20718  neips  20727  opnneissb  20728  opnssneib  20729  neindisj2  20737  innei  20739  neiptoptop  20745  neiptopnei  20746  neitr  20794  restcls  20795  cnpimaex  20870  cnprest2  20904  regsep  20948  nrmsep3  20969  nrmsep  20971  regsep2  20990  tgcmp  21014  uncmp  21016  bwth  21023  1stcfb  21058  1stcrest  21066  2ndcctbss  21068  1stcelcls  21074  lly1stc  21109  ssref  21125  refref  21126  comppfsc  21145  xkoopn  21202  neitx  21220  txcnp  21233  txcmplem1  21254  kqnrmlem1  21356  kqnrmlem2  21357  nrmhmph  21407  fbssfi  21451  opnfbas  21456  fbasfip  21482  fbunfip  21483  fgss2  21488  fgcl  21492  supfil  21509  isufil2  21522  filssufilg  21525  ssufl  21532  ufileu  21533  elfm3  21564  fmfnfm  21572  ufldom  21576  fbflim2  21591  flfneii  21606  flftg  21610  txflf  21620  supnfcls  21634  fclscf  21639  fclsfnflim  21641  flimfnfcls  21642  alexsubALTlem2  21662  alexsubALTlem3  21663  alexsubALTlem4  21664  alexsubALT  21665  tsmsfbas  21741  tsmsres  21757  tsmsf1o  21758  tsmsxplem1  21766  tsmsxp  21768  ustssel  21819  ustincl  21821  ustdiag  21822  ustinvel  21823  ustexhalf  21824  ust0  21833  elutop  21847  ustuqtop4  21858  cfiluexsm  21904  cfiluweak  21909  blssps  22039  blss  22040  metss  22123  metrest  22139  metcnp3  22155  metnrmlem3  22472  lebnumlem3  22570  lebnum  22571  ellimc3  23449  lhop1lem  23580  dchrelbas  24761  upgredgpr  25815  avril1  26711  spanval  27576  spancl  27579  shsval2i  27630  omlsi  27647  ococin  27651  chsupsn  27656  pjoml  27679  shs00i  27693  chj00i  27730  chsscon3  27743  chlejb1  27755  chnle  27757  pjoml2  27854  pjoml3  27855  lecm  27860  stcltr1i  28517  mdbr  28537  dmdmd  28543  dmdi  28545  dmdbr3  28548  dmdbr4  28549  mdsl1i  28564  mdslmd1lem3  28570  mdslmd1lem4  28571  csmdsymi  28577  hatomic  28603  chrelat2  28613  atord  28631  atcvat4i  28640  fz1nntr  28948  reff  29234  cmpcref  29245  sigagenval  29530  dmsigagen  29534  sigagenss  29539  ldsysgenld  29550  ldgenpisyslem1  29553  ldgenpisyslem2  29554  dynkin  29557  carsgmon  29703  carsgclctunlem2  29708  bnj1286  30341  bnj1452  30374  kur14lem9  30450  mclsssvlem  30713  mclsind  30721  frrlem1  31024  frrlem4  31027  frrlem5e  31032  frrlem11  31036  imagesset  31230  altopthsn  31238  fnessref  31522  refssfne  31523  topjoin  31530  neifg  31536  bj-snglex  32154  relowlssretop  32387  relowlpssretop  32388  finxpreclem3  32406  poimirlem29  32608  poimir  32612  mblfinlem3  32618  totbndss  32746  heibor1lem  32778  unichnidl  33000  ispridl  33003  maxidlmax  33012  igenval  33030  igenidl  33032  igenmin  33033  igenval2  33035  lsatcmp  33308  lcvexchlem4  33342  lcvexchlem5  33343  pclvalN  34194  pclclN  34195  elpcliN  34197  docaclN  35431  dihglb2  35649  doch2val2  35671  dochocss  35673  dochexmidlem7  35773  lpolconN  35794  mapdval  35935  nacsfix  36293  mzpcompact2  36333  rgspnval  36757  rgspncl  36758  rgspnmin  36760  superficl  36891  superuncl  36892  cleq2lem  36933  clcnvlem  36949  dfrtrcl3  37044  clsk1indlem2  37360  neik0pk1imk0  37365  isotone1  37366  isotone2  37367  ntrclsiso  37385  gneispacess2  37464  ssrecnpr  37529  founiiun  38355  founiiun0  38372  islptre  38686  salgenval  39217  salgenn0  39225  salgencl  39226  sssalgen  39229  salgenss  39230  salgenuni  39231  issalgend  39232  dfsalgen2  39235  salgencntex  39237  dfnbgr3  40562  nbupgr  40566  nbumgrvtx  40568  nbgr2vtx1edg  40572  nbuhgr2vtx1edgb  40574  cusgrexi  40662  1wlkvtxiedg  40829  1wlkres  40879  upgr11wlkdlem2  41313  1pthon2v-av  41320  1pthon2ve  41321  cusconngr  41358  setrec1lem1  42233  setrec1lem3  42235  setrec2fun  42238