Theorem sseq2 3952

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 3933	. . . 4 ⊢ (𝐶 ⊆ 𝐴 → (𝐴 ⊆ 𝐵 → 𝐶 ⊆ 𝐵))
2	1	com12 32	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵))
3		sstr2 3933	. . . 4 ⊢ (𝐶 ⊆ 𝐵 → (𝐵 ⊆ 𝐴 → 𝐶 ⊆ 𝐴))
4	3	com12 32	. . 3 ⊢ (𝐵 ⊆ 𝐴 → (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴))
5	2, 4	anim12i 614	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → ((𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵) ∧ (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴)))
6		eqss 3941	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
7		dfbi2 476	. 2 ⊢ ((𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵) ↔ ((𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵) ∧ (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴)))
8	5, 6, 7	3imtr4i 292	1 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1539   ⊆ wss 3892

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3439  df-in 3899  df-ss 3909

This theorem is referenced by:  sseq12  3953  sseq2i  3955  sseq2d  3958  sseqtrid  3978  nssne1  3986  psseq2  4029  sseq0  4339  un00  4382  disjpss  4400  pweqALT  4554  ssintab  4903  ssintub  4904  intmin  4906  treq  5206  al0ssb  5241  sseliALT  5242  ssexg  5256  intabs  5275  iunopeqop  5448  ordunidif  6329  ordssun  6382  fununi  6538  feq3  6613  ssimaexg  6886  iunpw  7653  tfindsg  7739  limomss  7749  findsg  7778  funcnvuni  7810  frxp  7998  frrlem1  8133  frrlem13  8145  wrecseq123OLD  8162  wfrlem1OLD  8170  wfrlem4OLD  8174  wfrlem15OLD  8185  onfununi  8203  oawordeu  8417  oawordexr  8418  nnawordex  8499  eldifsucnn  8525  ereq1  8536  xpider  8608  domeng  8783  sbthlem4  8911  sbthlem5  8912  domssex  8963  ssfi  8994  finsschain  9170  dffi2  9226  dffi3  9234  hartogslem1  9345  inf3lema  9426  cantnflem1  9491  dfttrcl2  9526  tz9.1  9531  tz9.1c  9532  tctr  9542  tcmin  9543  tcrank  9686  scottex  9687  cardlim  9774  infxpenlem  9815  infxpenc2  9824  isinfcard  9894  alephinit  9897  alephval3  9912  dfac3  9923  cflem  10048  cfval  10049  cflecard  10055  cfsuc  10059  cff1  10060  cfflb  10061  cflim2  10065  isf32lem2  10156  fin1a2lem13  10214  ac7g  10276  ttukeylem5  10315  ttukeylem7  10317  pwcfsdom  10385  pwfseqlem5  10465  pwfseq  10466  gch2  10477  winalim  10497  wunex  10541  wuncss  10547  eltskg  10552  eltsk2g  10553  gruina  10620  grur1a  10621  axgroth6  10630  swrdnd2  14413  trcleq2lem  14747  dfrtrcl2  14818  fprodss  15703  mrcflem  17360  mrcval  17364  isacs2  17407  acsfiel  17408  ipoval  18293  fpwipodrs  18303  ipodrsima  18304  mreclatBAD  18326  slwispgp  19261  pgpssslw  19264  lsmss1b  19317  lsmss2b  19319  cntzcmnss  19487  gsumzres  19555  lspf  20281  lspval  20282  lbsextlem1  20465  lbsextlem3  20467  lbsextlem4  20468  aspval  21122  mplsubglem  21250  mpllsslem  21251  basis2  22146  eltg2  22153  clsval  22233  clscld  22243  clsval2  22246  ntrcls0  22272  isnei  22299  neiint  22300  neips  22309  opnneissb  22310  opnssneib  22311  neindisj2  22319  innei  22321  neiptoptop  22327  neiptopnei  22328  neitr  22376  restcls  22377  cnpimaex  22452  cnprest2  22486  regsep  22530  nrmsep3  22551  nrmsep  22553  regsep2  22572  tgcmp  22597  uncmp  22599  bwth  22606  1stcfb  22641  1stcrest  22649  2ndcctbss  22651  1stcelcls  22657  lly1stc  22692  ssref  22708  refref  22709  comppfsc  22728  xkoopn  22785  neitx  22803  txcnp  22816  txcmplem1  22837  kqnrmlem1  22939  kqnrmlem2  22940  nrmhmph  22990  fbssfi  23033  opnfbas  23038  fbasfip  23064  fbunfip  23065  fgss2  23070  fgcl  23074  supfil  23091  isufil2  23104  filssufilg  23107  ssufl  23114  ufileu  23115  elfm3  23146  fmfnfm  23154  ufldom  23158  fbflim2  23173  flfneii  23188  flftg  23192  txflf  23202  supnfcls  23216  fclscf  23221  fclsfnflim  23223  flimfnfcls  23224  alexsubALTlem2  23244  alexsubALTlem3  23245  alexsubALTlem4  23246  alexsubALT  23247  tsmsfbas  23324  tsmsres  23340  tsmsf1o  23341  tsmsxplem1  23349  tsmsxp  23351  ustssel  23402  ustincl  23404  ustdiag  23405  ustinvel  23406  ustexhalf  23407  ust0  23416  elutop  23430  ustuqtop4  23441  cfiluexsm  23487  cfiluweak  23492  blssps  23622  blss  23623  metss  23709  metrest  23725  metcnp3  23741  metnrmlem3  24069  lebnumlem3  24171  lebnum  24172  ellimc3  25088  lhop1lem  25222  dchrelbas  26429  upgredgpr  27557  dfnbgr3  27750  nbupgr  27756  nbumgrvtx  27758  nbgr2vtx1edg  27762  nbuhgr2vtx1edgb  27764  cusgrexilem2  27854  wlkvtxiedg  28037  wlkres  28083  upgr1wlkdlem2  28555  1pthon2v  28562  1pthon2ve  28563  cusconngr  28600  isfrgr  28669  avril1  28872  spanval  29740  spancl  29743  shsval2i  29794  omlsi  29811  ococin  29815  chsupsn  29820  pjoml  29843  shs00i  29857  chj00i  29894  chsscon3  29907  chlejb1  29919  chnle  29921  pjoml2  30018  pjoml3  30019  lecm  30024  stcltr1i  30681  mdbr  30701  dmdmd  30707  dmdi  30709  dmdbr3  30712  dmdbr4  30713  mdsl1i  30728  mdslmd1lem3  30734  mdslmd1lem4  30735  csmdsymi  30741  hatomic  30767  chrelat2  30777  atord  30795  atcvat4i  30804  fz1nntr  31170  nsgmgc  31642  nsgqusf1olem2  31644  isprmidl  31658  mxidlmax  31682  ssmxidllem  31686  ssmxidl  31687  reff  31834  cmpcref  31845  zarcls1  31864  zarclsiin  31866  zarclssn  31868  zart0  31874  zarmxt1  31875  zarcmp  31877  rhmpreimacnlem  31879  sigagenval  32153  dmsigagen  32157  sigagenss  32162  ldsysgenld  32173  ldgenpisyslem1  32176  ldgenpisyslem2  32177  dynkin  32180  carsgmon  32326  carsgclctunlem2  32331  bnj1286  33044  bnj1452  33077  fineqvac  33111  kur14lem9  33221  mclsssvlem  33569  mclsind  33577  onelssex  33706  fnssintima  33721  naddcllem  33876  eqscut2  34045  scutun12  34049  madebdayim  34115  madebday  34125  imagesset  34300  altopthsn  34308  fnessref  34591  refssfne  34592  topjoin  34599  neifg  34605  bj-snglex  35207  bj-imdirvallem  35395  relowlssretop  35578  relowlpssretop  35579  exrecfnlem  35594  finxpreclem3  35608  pibt2  35632  poimirlem29  35850  poimir  35854  mblfinlem3  35860  totbndss  35979  heibor1lem  36011  unichnidl  36233  ispridl  36236  maxidlmax  36245  igenval  36263  igenidl  36265  igenmin  36266  igenval2  36268  brssr  36661  lsatcmp  37059  lcvexchlem4  37093  lcvexchlem5  37094  pclvalN  37946  pclclN  37947  elpcliN  37949  docaclN  39180  dihglb2  39398  doch2val2  39420  dochocss  39422  dochexmidlem7  39522  lpolconN  39543  mapdval  39684  nacsfix  40571  mzpcompact2  40611  rgspnval  41031  rgspncl  41032  rgspnmin  41034  superficl  41212  superuncl  41213  cleq2lem  41254  clcnvlem  41269  dfrtrcl3  41379  clsk1indlem2  41690  neik0pk1imk0  41695  isotone1  41696  isotone2  41697  ntrclsiso  41715  gneispacess2  41794  mnuunid  41933  mnurndlem2  41938  ssrecnpr  41964  founiiun  42759  founiiun0  42772  islptre  43209  salgenval  43911  salgenn0  43919  salgencl  43920  sssalgen  43923  salgenss  43924  salgenuni  43925  issalgend  43926  dfsalgen2  43929  salgencntex  43931  isomgreqve  45335  opndisj  46254  opnneilem  46257  sepfsepc  46279  iscnrm3rlem8  46299  iscnrm3llem2  46302  intubeu  46328  ipolubdm  46331  ipoglbdm  46334  setrec1lem1  46451  setrec1lem3  46453  setrec2fun  46456