Theorem sseq2 3951

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 3932	. . . 4 ⊢ (𝐶 ⊆ 𝐴 → (𝐴 ⊆ 𝐵 → 𝐶 ⊆ 𝐵))
2	1	com12 32	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵))
3		sstr2 3932	. . . 4 ⊢ (𝐶 ⊆ 𝐵 → (𝐵 ⊆ 𝐴 → 𝐶 ⊆ 𝐴))
4	3	com12 32	. . 3 ⊢ (𝐵 ⊆ 𝐴 → (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴))
5	2, 4	anim12i 612	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → ((𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵) ∧ (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴)))
6		eqss 3940	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
7		dfbi2 474	. 2 ⊢ ((𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵) ↔ ((𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵) ∧ (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴)))
8	5, 6, 7	3imtr4i 291	1 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1541   ⊆ wss 3891

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3432  df-in 3898  df-ss 3908

This theorem is referenced by:  sseq12  3952  sseq2i  3954  sseq2d  3957  sseqtrid  3977  nssne1  3985  psseq2  4027  sseq0  4338  un00  4381  disjpss  4399  pweqALT  4555  ssintab  4901  ssintub  4902  intmin  4904  treq  5201  al0ssb  5235  sseliALT  5236  ssexg  5250  intabs  5269  iunopeqop  5437  ordunidif  6311  ordssun  6362  fununi  6505  feq3  6579  ssimaexg  6848  iunpw  7612  tfindsg  7695  limomss  7705  findsg  7733  funcnvuni  7765  frxp  7951  frrlem1  8086  frrlem13  8098  wrecseq123OLD  8115  wfrlem1OLD  8123  wfrlem4OLD  8127  wfrlem15OLD  8138  onfununi  8156  oawordeu  8362  oawordexr  8363  nnawordex  8444  eldifsucnn  8468  ereq1  8479  xpider  8551  domeng  8723  sbthlem4  8842  sbthlem5  8843  domssex  8890  ssfi  8921  finsschain  9087  dffi2  9143  dffi3  9151  hartogslem1  9262  inf3lema  9343  cantnflem1  9408  dfttrcl2  9443  tz9.1  9470  tz9.1c  9471  tctr  9481  tcmin  9482  tcrank  9626  scottex  9627  cardlim  9714  infxpenlem  9753  infxpenc2  9762  isinfcard  9832  alephinit  9835  alephval3  9850  dfac3  9861  cflem  9986  cfval  9987  cflecard  9993  cfsuc  9997  cff1  9998  cfflb  9999  cflim2  10003  isf32lem2  10094  fin1a2lem13  10152  ac7g  10214  ttukeylem5  10253  ttukeylem7  10255  pwcfsdom  10323  pwfseqlem5  10403  pwfseq  10404  gch2  10415  winalim  10435  wunex  10479  wuncss  10485  eltskg  10490  eltsk2g  10491  gruina  10558  grur1a  10559  axgroth6  10568  swrdnd2  14349  trcleq2lem  14683  dfrtrcl2  14754  fprodss  15639  mrcflem  17296  mrcval  17300  isacs2  17343  acsfiel  17344  ipoval  18229  fpwipodrs  18239  ipodrsima  18240  mreclatBAD  18262  slwispgp  19197  pgpssslw  19200  lsmss1b  19253  lsmss2b  19255  cntzcmnss  19423  gsumzres  19491  lspf  20217  lspval  20218  lbsextlem1  20401  lbsextlem3  20403  lbsextlem4  20404  aspval  21058  mplsubglem  21186  mpllsslem  21187  basis2  22082  eltg2  22089  clsval  22169  clscld  22179  clsval2  22182  ntrcls0  22208  isnei  22235  neiint  22236  neips  22245  opnneissb  22246  opnssneib  22247  neindisj2  22255  innei  22257  neiptoptop  22263  neiptopnei  22264  neitr  22312  restcls  22313  cnpimaex  22388  cnprest2  22422  regsep  22466  nrmsep3  22487  nrmsep  22489  regsep2  22508  tgcmp  22533  uncmp  22535  bwth  22542  1stcfb  22577  1stcrest  22585  2ndcctbss  22587  1stcelcls  22593  lly1stc  22628  ssref  22644  refref  22645  comppfsc  22664  xkoopn  22721  neitx  22739  txcnp  22752  txcmplem1  22773  kqnrmlem1  22875  kqnrmlem2  22876  nrmhmph  22926  fbssfi  22969  opnfbas  22974  fbasfip  23000  fbunfip  23001  fgss2  23006  fgcl  23010  supfil  23027  isufil2  23040  filssufilg  23043  ssufl  23050  ufileu  23051  elfm3  23082  fmfnfm  23090  ufldom  23094  fbflim2  23109  flfneii  23124  flftg  23128  txflf  23138  supnfcls  23152  fclscf  23157  fclsfnflim  23159  flimfnfcls  23160  alexsubALTlem2  23180  alexsubALTlem3  23181  alexsubALTlem4  23182  alexsubALT  23183  tsmsfbas  23260  tsmsres  23276  tsmsf1o  23277  tsmsxplem1  23285  tsmsxp  23287  ustssel  23338  ustincl  23340  ustdiag  23341  ustinvel  23342  ustexhalf  23343  ust0  23352  elutop  23366  ustuqtop4  23377  cfiluexsm  23423  cfiluweak  23428  blssps  23558  blss  23559  metss  23645  metrest  23661  metcnp3  23677  metnrmlem3  24005  lebnumlem3  24107  lebnum  24108  ellimc3  25024  lhop1lem  25158  dchrelbas  26365  upgredgpr  27493  dfnbgr3  27686  nbupgr  27692  nbumgrvtx  27694  nbgr2vtx1edg  27698  nbuhgr2vtx1edgb  27700  cusgrexilem2  27790  wlkvtxiedg  27972  wlkres  28018  upgr1wlkdlem2  28489  1pthon2v  28496  1pthon2ve  28497  cusconngr  28534  isfrgr  28603  avril1  28806  spanval  29674  spancl  29677  shsval2i  29728  omlsi  29745  ococin  29749  chsupsn  29754  pjoml  29777  shs00i  29791  chj00i  29828  chsscon3  29841  chlejb1  29853  chnle  29855  pjoml2  29952  pjoml3  29953  lecm  29958  stcltr1i  30615  mdbr  30635  dmdmd  30641  dmdi  30643  dmdbr3  30646  dmdbr4  30647  mdsl1i  30662  mdslmd1lem3  30668  mdslmd1lem4  30669  csmdsymi  30675  hatomic  30701  chrelat2  30711  atord  30729  atcvat4i  30738  fz1nntr  31104  nsgmgc  31576  nsgqusf1olem2  31578  isprmidl  31592  mxidlmax  31616  ssmxidllem  31620  ssmxidl  31621  reff  31768  cmpcref  31779  zarcls1  31798  zarclsiin  31800  zarclssn  31802  zart0  31808  zarmxt1  31809  zarcmp  31811  rhmpreimacnlem  31813  sigagenval  32087  dmsigagen  32091  sigagenss  32096  ldsysgenld  32107  ldgenpisyslem1  32110  ldgenpisyslem2  32111  dynkin  32114  carsgmon  32260  carsgclctunlem2  32265  bnj1286  32978  bnj1452  33011  fineqvac  33045  kur14lem9  33155  mclsssvlem  33503  mclsind  33511  onelssex  33640  fnssintima  33655  naddcllem  33810  eqscut2  33979  scutun12  33983  madebdayim  34049  madebday  34059  imagesset  34234  altopthsn  34242  fnessref  34525  refssfne  34526  topjoin  34533  neifg  34539  bj-snglex  35142  bj-imdirvallem  35330  relowlssretop  35513  relowlpssretop  35514  exrecfnlem  35529  finxpreclem3  35543  pibt2  35567  poimirlem29  35785  poimir  35789  mblfinlem3  35795  totbndss  35914  heibor1lem  35946  unichnidl  36168  ispridl  36171  maxidlmax  36180  igenval  36198  igenidl  36200  igenmin  36201  igenval2  36203  brssr  36598  lsatcmp  36996  lcvexchlem4  37030  lcvexchlem5  37031  pclvalN  37883  pclclN  37884  elpcliN  37886  docaclN  39117  dihglb2  39335  doch2val2  39357  dochocss  39359  dochexmidlem7  39459  lpolconN  39480  mapdval  39621  nacsfix  40514  mzpcompact2  40554  rgspnval  40973  rgspncl  40974  rgspnmin  40976  superficl  41127  superuncl  41128  cleq2lem  41169  clcnvlem  41184  dfrtrcl3  41294  clsk1indlem2  41605  neik0pk1imk0  41610  isotone1  41611  isotone2  41612  ntrclsiso  41630  gneispacess2  41709  mnuunid  41848  mnurndlem2  41853  ssrecnpr  41879  founiiun  42668  founiiun0  42681  islptre  43114  salgenval  43816  salgenn0  43824  salgencl  43825  sssalgen  43828  salgenss  43829  salgenuni  43830  issalgend  43831  dfsalgen2  43834  salgencntex  43836  isomgreqve  45229  opndisj  46148  opnneilem  46151  sepfsepc  46173  iscnrm3rlem8  46193  iscnrm3llem2  46196  intubeu  46222  ipolubdm  46225  ipoglbdm  46228  setrec1lem1  46345  setrec1lem3  46347  setrec2fun  46350