Theorem sseq2 3909

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1520   ⊆ wss 3854

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-ext 2767

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-clab 2774  df-cleq 2786  df-clel 2861  df-in 3861  df-ss 3869

This theorem is referenced by:  sseq12  3910  sseq2i  3912  sseq2d  3915  sseqtrid  3935  nssne1  3943  psseq2  3981  sseq0  4267  un00  4302  disjpss  4318  pweq  4450  ssintab  4793  ssintub  4794  intmin  4796  treq  5063  al0ssb  5097  sseliALT  5098  ssexg  5111  intabs  5129  iunopeqop  5295  ordunidif  6106  ordssun  6157  fununi  6291  feq3  6357  ssimaexg  6608  iunpw  7340  tfindsg  7422  limomss  7432  findsg  7456  funcnvuni  7483  frxp  7664  wrecseq123  7790  wfrlem1  7796  wfrlem4  7800  wfrlem4OLD  7801  wfrlem15  7812  onfununi  7821  oawordeu  8022  oawordexr  8023  nnawordex  8104  ereq1  8137  xpider  8209  domeng  8361  sbthlem4  8467  sbthlem5  8468  domssex  8515  finsschain  8667  dffi2  8723  dffi3  8731  hartogslem1  8842  inf3lema  8922  cantnflem1  8987  tz9.1  9006  tz9.1c  9007  tctr  9017  tcmin  9018  tcrank  9148  scottex  9149  cardlim  9236  infxpenlem  9274  infxpenc2  9283  isinfcard  9353  alephinit  9356  alephval3  9371  dfac3  9382  cflem  9503  cfval  9504  cflecard  9510  cfsuc  9514  cff1  9515  cfflb  9516  cflim2  9520  isf32lem2  9611  fin1a2lem13  9669  ac7g  9731  ttukeylem5  9770  ttukeylem7  9772  pwcfsdom  9840  pwfseqlem5  9920  pwfseq  9921  gch2  9932  winalim  9952  wunex  9996  wuncss  10002  eltskg  10007  eltsk2g  10008  gruina  10075  grur1a  10076  axgroth6  10085  swrdnd2  13841  trcleq2lem  14173  dfrtrcl2  14243  fprodss  15123  mrcflem  16694  mrcval  16698  isacs2  16741  acsfiel  16742  ipoval  17581  fpwipodrs  17591  ipodrsima  17592  mreclatBAD  17614  slwispgp  18454  pgpssslw  18457  lsmss1b  18508  lsmss2b  18510  cntzcmnss  18674  gsumzres  18738  lspf  19424  lspval  19425  lbsextlem1  19608  lbsextlem3  19610  lbsextlem4  19611  aspval  19778  mplsubglem  19890  mpllsslem  19891  basis2  21231  eltg2  21238  clsval  21317  clscld  21327  clsval2  21330  ntrcls0  21356  isnei  21383  neiint  21384  neips  21393  opnneissb  21394  opnssneib  21395  neindisj2  21403  innei  21405  neiptoptop  21411  neiptopnei  21412  neitr  21460  restcls  21461  cnpimaex  21536  cnprest2  21570  regsep  21614  nrmsep3  21635  nrmsep  21637  regsep2  21656  tgcmp  21681  uncmp  21683  bwth  21690  1stcfb  21725  1stcrest  21733  2ndcctbss  21735  1stcelcls  21741  lly1stc  21776  ssref  21792  refref  21793  comppfsc  21812  xkoopn  21869  neitx  21887  txcnp  21900  txcmplem1  21921  kqnrmlem1  22023  kqnrmlem2  22024  nrmhmph  22074  fbssfi  22117  opnfbas  22122  fbasfip  22148  fbunfip  22149  fgss2  22154  fgcl  22158  supfil  22175  isufil2  22188  filssufilg  22191  ssufl  22198  ufileu  22199  elfm3  22230  fmfnfm  22238  ufldom  22242  fbflim2  22257  flfneii  22272  flftg  22276  txflf  22286  supnfcls  22300  fclscf  22305  fclsfnflim  22307  flimfnfcls  22308  alexsubALTlem2  22328  alexsubALTlem3  22329  alexsubALTlem4  22330  alexsubALT  22331  tsmsfbas  22407  tsmsres  22423  tsmsf1o  22424  tsmsxplem1  22432  tsmsxp  22434  ustssel  22485  ustincl  22487  ustdiag  22488  ustinvel  22489  ustexhalf  22490  ust0  22499  elutop  22513  ustuqtop4  22524  cfiluexsm  22570  cfiluweak  22575  blssps  22705  blss  22706  metss  22789  metrest  22805  metcnp3  22821  metnrmlem3  23140  lebnumlem3  23238  lebnum  23239  ellimc3  24148  lhop1lem  24281  dchrelbas  25482  upgredgpr  26598  dfnbgr3  26791  nbupgr  26797  nbumgrvtx  26799  nbgr2vtx1edg  26803  nbuhgr2vtx1edgb  26805  cusgrexilem2  26895  wlkvtxiedg  27077  wlkres  27123  wlkresOLD  27125  upgr1wlkdlem2  27600  1pthon2v  27607  1pthon2ve  27608  cusconngr  27645  avril1  27921  spanval  28789  spancl  28792  shsval2i  28843  omlsi  28860  ococin  28864  chsupsn  28869  pjoml  28892  shs00i  28906  chj00i  28943  chsscon3  28956  chlejb1  28968  chnle  28970  pjoml2  29067  pjoml3  29068  lecm  29073  stcltr1i  29730  mdbr  29750  dmdmd  29756  dmdi  29758  dmdbr3  29761  dmdbr4  29762  mdsl1i  29777  mdslmd1lem3  29783  mdslmd1lem4  29784  csmdsymi  29790  hatomic  29816  chrelat2  29826  atord  29844  atcvat4i  29853  fz1nntr  30183  reff  30676  cmpcref  30687  sigagenval  30972  dmsigagen  30976  sigagenss  30981  ldsysgenld  30992  ldgenpisyslem1  30995  ldgenpisyslem2  30996  dynkin  30999  carsgmon  31145  carsgclctunlem2  31150  bnj1286  31861  bnj1452  31894  kur14lem9  32025  mclsssvlem  32362  mclsind  32370  frrlem1  32677  frrlem13  32689  scutun12  32825  imagesset  32968  altopthsn  32976  fnessref  33259  refssfne  33260  topjoin  33267  neifg  33273  bj-snglex  33836  relowlssretop  34121  relowlpssretop  34122  exrecfnlem  34137  finxpreclem3  34151  pibt2  34175  poimirlem29  34398  poimir  34402  mblfinlem3  34408  totbndss  34533  heibor1lem  34565  unichnidl  34787  ispridl  34790  maxidlmax  34799  igenval  34817  igenidl  34819  igenmin  34820  igenval2  34822  brssr  35222  lsatcmp  35620  lcvexchlem4  35654  lcvexchlem5  35655  pclvalN  36507  pclclN  36508  elpcliN  36510  docaclN  37741  dihglb2  37959  doch2val2  37981  dochocss  37983  dochexmidlem7  38083  lpolconN  38104  mapdval  38245  nacsfix  38744  mzpcompact2  38784  rgspnval  39204  rgspncl  39205  rgspnmin  39207  superficl  39362  superuncl  39363  cleq2lem  39404  clcnvlem  39419  dfrtrcl3  39514  clsk1indlem2  39828  neik0pk1imk0  39833  isotone1  39834  isotone2  39835  ntrclsiso  39853  gneispacess2  39932  mnuunid  40062  mnurndlem2  40067  ssrecnpr  40130  founiiun  40928  founiiun0  40944  islptre  41396  salgenval  42102  salgenn0  42110  salgencl  42111  sssalgen  42114  salgenss  42115  salgenuni  42116  issalgend  42117  dfsalgen2  42120  salgencntex  42122  isomgreqve  43426  setrec1lem1  44224  setrec1lem3  44226  setrec2fun  44229