Theorem sseq2 3920

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 3901	. . . 4 ⊢ (𝐶 ⊆ 𝐴 → (𝐴 ⊆ 𝐵 → 𝐶 ⊆ 𝐵))
2	1	com12 32	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵))
3		sstr2 3901	. . . 4 ⊢ (𝐶 ⊆ 𝐵 → (𝐵 ⊆ 𝐴 → 𝐶 ⊆ 𝐴))
4	3	com12 32	. . 3 ⊢ (𝐵 ⊆ 𝐴 → (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴))
5	2, 4	anim12i 615	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → ((𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵) ∧ (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴)))
6		eqss 3909	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
7		dfbi2 478	. 2 ⊢ ((𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵) ↔ ((𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵) ∧ (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴)))
8	5, 6, 7	3imtr4i 295	1 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ⊆ wss 3860

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3867  df-ss 3877

This theorem is referenced by:  sseq12  3921  sseq2i  3923  sseq2d  3926  sseqtrid  3946  nssne1  3954  psseq2  3996  sseq0  4298  un00  4342  disjpss  4360  pweqALT  4514  ssintab  4858  ssintub  4859  intmin  4861  treq  5148  al0ssb  5182  sseliALT  5183  ssexg  5197  intabs  5216  iunopeqop  5384  ordunidif  6222  ordssun  6273  fununi  6415  feq3  6486  ssimaexg  6743  iunpw  7498  tfindsg  7580  limomss  7590  findsg  7615  funcnvuni  7647  frxp  7831  wrecseq123  7964  wfrlem1  7970  wfrlem4  7974  wfrlem15  7985  onfununi  7994  oawordeu  8197  oawordexr  8198  nnawordex  8279  ereq1  8312  xpider  8384  domeng  8554  sbthlem4  8665  sbthlem5  8666  domssex  8713  ssfi  8755  finsschain  8877  dffi2  8933  dffi3  8941  hartogslem1  9052  inf3lema  9133  cantnflem1  9198  tz9.1  9217  tz9.1c  9218  tctr  9228  tcmin  9229  tcrank  9359  scottex  9360  cardlim  9447  infxpenlem  9486  infxpenc2  9495  isinfcard  9565  alephinit  9568  alephval3  9583  dfac3  9594  cflem  9719  cfval  9720  cflecard  9726  cfsuc  9730  cff1  9731  cfflb  9732  cflim2  9736  isf32lem2  9827  fin1a2lem13  9885  ac7g  9947  ttukeylem5  9986  ttukeylem7  9988  pwcfsdom  10056  pwfseqlem5  10136  pwfseq  10137  gch2  10148  winalim  10168  wunex  10212  wuncss  10218  eltskg  10223  eltsk2g  10224  gruina  10291  grur1a  10292  axgroth6  10301  swrdnd2  14077  trcleq2lem  14411  dfrtrcl2  14482  fprodss  15363  mrcflem  16948  mrcval  16952  isacs2  16995  acsfiel  16996  ipoval  17843  fpwipodrs  17853  ipodrsima  17854  mreclatBAD  17876  slwispgp  18816  pgpssslw  18819  lsmss1b  18872  lsmss2b  18874  cntzcmnss  19042  gsumzres  19110  lspf  19827  lspval  19828  lbsextlem1  20011  lbsextlem3  20013  lbsextlem4  20014  aspval  20648  mplsubglem  20777  mpllsslem  20778  basis2  21664  eltg2  21671  clsval  21750  clscld  21760  clsval2  21763  ntrcls0  21789  isnei  21816  neiint  21817  neips  21826  opnneissb  21827  opnssneib  21828  neindisj2  21836  innei  21838  neiptoptop  21844  neiptopnei  21845  neitr  21893  restcls  21894  cnpimaex  21969  cnprest2  22003  regsep  22047  nrmsep3  22068  nrmsep  22070  regsep2  22089  tgcmp  22114  uncmp  22116  bwth  22123  1stcfb  22158  1stcrest  22166  2ndcctbss  22168  1stcelcls  22174  lly1stc  22209  ssref  22225  refref  22226  comppfsc  22245  xkoopn  22302  neitx  22320  txcnp  22333  txcmplem1  22354  kqnrmlem1  22456  kqnrmlem2  22457  nrmhmph  22507  fbssfi  22550  opnfbas  22555  fbasfip  22581  fbunfip  22582  fgss2  22587  fgcl  22591  supfil  22608  isufil2  22621  filssufilg  22624  ssufl  22631  ufileu  22632  elfm3  22663  fmfnfm  22671  ufldom  22675  fbflim2  22690  flfneii  22705  flftg  22709  txflf  22719  supnfcls  22733  fclscf  22738  fclsfnflim  22740  flimfnfcls  22741  alexsubALTlem2  22761  alexsubALTlem3  22762  alexsubALTlem4  22763  alexsubALT  22764  tsmsfbas  22841  tsmsres  22857  tsmsf1o  22858  tsmsxplem1  22866  tsmsxp  22868  ustssel  22919  ustincl  22921  ustdiag  22922  ustinvel  22923  ustexhalf  22924  ust0  22933  elutop  22947  ustuqtop4  22958  cfiluexsm  23004  cfiluweak  23009  blssps  23139  blss  23140  metss  23223  metrest  23239  metcnp3  23255  metnrmlem3  23575  lebnumlem3  23677  lebnum  23678  ellimc3  24591  lhop1lem  24725  dchrelbas  25932  upgredgpr  27047  dfnbgr3  27240  nbupgr  27246  nbumgrvtx  27248  nbgr2vtx1edg  27252  nbuhgr2vtx1edgb  27254  cusgrexilem2  27344  wlkvtxiedg  27526  wlkres  27572  upgr1wlkdlem2  28043  1pthon2v  28050  1pthon2ve  28051  cusconngr  28088  isfrgr  28157  avril1  28360  spanval  29228  spancl  29231  shsval2i  29282  omlsi  29299  ococin  29303  chsupsn  29308  pjoml  29331  shs00i  29345  chj00i  29382  chsscon3  29395  chlejb1  29407  chnle  29409  pjoml2  29506  pjoml3  29507  lecm  29512  stcltr1i  30169  mdbr  30189  dmdmd  30195  dmdi  30197  dmdbr3  30200  dmdbr4  30201  mdsl1i  30216  mdslmd1lem3  30222  mdslmd1lem4  30223  csmdsymi  30229  hatomic  30255  chrelat2  30265  atord  30283  atcvat4i  30292  fz1nntr  30661  nsgmgc  31130  nsgqusf1olem2  31132  isprmidl  31146  mxidlmax  31170  ssmxidllem  31174  ssmxidl  31175  reff  31322  cmpcref  31333  zarcls1  31352  zarclsiin  31354  zarclssn  31356  zart0  31362  zarmxt1  31363  zarcmp  31365  rhmpreimacnlem  31367  sigagenval  31639  dmsigagen  31643  sigagenss  31648  ldsysgenld  31659  ldgenpisyslem1  31662  ldgenpisyslem2  31663  dynkin  31666  carsgmon  31812  carsgclctunlem2  31817  bnj1286  32531  bnj1452  32564  kur14lem9  32704  mclsssvlem  33052  mclsind  33060  onelssex  33191  fnssintima  33206  frrlem1  33397  frrlem13  33409  naddcllem  33428  eqscut2  33595  scutun12  33599  madebdayim  33661  madebday  33671  imagesset  33838  altopthsn  33846  fnessref  34129  refssfne  34130  topjoin  34137  neifg  34143  bj-snglex  34724  bj-imdirvallem  34909  relowlssretop  35094  relowlpssretop  35095  exrecfnlem  35110  finxpreclem3  35124  pibt2  35148  poimirlem29  35400  poimir  35404  mblfinlem3  35410  totbndss  35529  heibor1lem  35561  unichnidl  35783  ispridl  35786  maxidlmax  35795  igenval  35813  igenidl  35815  igenmin  35816  igenval2  35818  brssr  36215  lsatcmp  36613  lcvexchlem4  36647  lcvexchlem5  36648  pclvalN  37500  pclclN  37501  elpcliN  37503  docaclN  38734  dihglb2  38952  doch2val2  38974  dochocss  38976  dochexmidlem7  39076  lpolconN  39097  mapdval  39238  nacsfix  40061  mzpcompact2  40101  rgspnval  40520  rgspncl  40521  rgspnmin  40523  superficl  40674  superuncl  40675  cleq2lem  40716  clcnvlem  40731  dfrtrcl3  40842  clsk1indlem2  41153  neik0pk1imk0  41158  isotone1  41159  isotone2  41160  ntrclsiso  41178  gneispacess2  41257  mnuunid  41393  mnurndlem2  41398  ssrecnpr  41420  founiiun  42209  founiiun0  42222  islptre  42662  salgenval  43364  salgenn0  43372  salgencl  43373  sssalgen  43376  salgenss  43377  salgenuni  43378  issalgend  43379  dfsalgen2  43382  salgencntex  43384  isomgreqve  44759  opndisj  45636  opnneilem  45638  sepfsepc  45660  iscnrm3rlem8  45680  iscnrm3llem2  45683  setrec1lem1  45702  setrec1lem3  45704  setrec2fun  45707