Theorem sseq2 3992

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1533   ⊆ wss 3935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3942  df-ss 3951

This theorem is referenced by:  sseq12  3993  sseq2i  3995  sseq2d  3998  sseqtrid  4018  nssne1  4026  psseq2  4064  sseq0  4352  un00  4393  disjpss  4409  pweq  4541  ssintab  4885  ssintub  4886  intmin  4888  treq  5170  al0ssb  5204  sseliALT  5205  ssexg  5219  intabs  5237  iunopeqop  5403  ordunidif  6233  ordssun  6284  fununi  6423  feq3  6491  ssimaexg  6743  iunpw  7487  tfindsg  7569  limomss  7579  findsg  7603  funcnvuni  7630  frxp  7814  wrecseq123  7942  wfrlem1  7948  wfrlem4  7952  wfrlem15  7963  onfununi  7972  oawordeu  8175  oawordexr  8176  nnawordex  8257  ereq1  8290  xpider  8362  domeng  8517  sbthlem4  8624  sbthlem5  8625  domssex  8672  finsschain  8825  dffi2  8881  dffi3  8889  hartogslem1  9000  inf3lema  9081  cantnflem1  9146  tz9.1  9165  tz9.1c  9166  tctr  9176  tcmin  9177  tcrank  9307  scottex  9308  cardlim  9395  infxpenlem  9433  infxpenc2  9442  isinfcard  9512  alephinit  9515  alephval3  9530  dfac3  9541  cflem  9662  cfval  9663  cflecard  9669  cfsuc  9673  cff1  9674  cfflb  9675  cflim2  9679  isf32lem2  9770  fin1a2lem13  9828  ac7g  9890  ttukeylem5  9929  ttukeylem7  9931  pwcfsdom  9999  pwfseqlem5  10079  pwfseq  10080  gch2  10091  winalim  10111  wunex  10155  wuncss  10161  eltskg  10166  eltsk2g  10167  gruina  10234  grur1a  10235  axgroth6  10244  swrdnd2  14011  trcleq2lem  14345  dfrtrcl2  14415  fprodss  15296  mrcflem  16871  mrcval  16875  isacs2  16918  acsfiel  16919  ipoval  17758  fpwipodrs  17768  ipodrsima  17769  mreclatBAD  17791  slwispgp  18730  pgpssslw  18733  lsmss1b  18786  lsmss2b  18788  cntzcmnss  18955  gsumzres  19023  lspf  19740  lspval  19741  lbsextlem1  19924  lbsextlem3  19926  lbsextlem4  19927  aspval  20096  mplsubglem  20208  mpllsslem  20209  basis2  21553  eltg2  21560  clsval  21639  clscld  21649  clsval2  21652  ntrcls0  21678  isnei  21705  neiint  21706  neips  21715  opnneissb  21716  opnssneib  21717  neindisj2  21725  innei  21727  neiptoptop  21733  neiptopnei  21734  neitr  21782  restcls  21783  cnpimaex  21858  cnprest2  21892  regsep  21936  nrmsep3  21957  nrmsep  21959  regsep2  21978  tgcmp  22003  uncmp  22005  bwth  22012  1stcfb  22047  1stcrest  22055  2ndcctbss  22057  1stcelcls  22063  lly1stc  22098  ssref  22114  refref  22115  comppfsc  22134  xkoopn  22191  neitx  22209  txcnp  22222  txcmplem1  22243  kqnrmlem1  22345  kqnrmlem2  22346  nrmhmph  22396  fbssfi  22439  opnfbas  22444  fbasfip  22470  fbunfip  22471  fgss2  22476  fgcl  22480  supfil  22497  isufil2  22510  filssufilg  22513  ssufl  22520  ufileu  22521  elfm3  22552  fmfnfm  22560  ufldom  22564  fbflim2  22579  flfneii  22594  flftg  22598  txflf  22608  supnfcls  22622  fclscf  22627  fclsfnflim  22629  flimfnfcls  22630  alexsubALTlem2  22650  alexsubALTlem3  22651  alexsubALTlem4  22652  alexsubALT  22653  tsmsfbas  22730  tsmsres  22746  tsmsf1o  22747  tsmsxplem1  22755  tsmsxp  22757  ustssel  22808  ustincl  22810  ustdiag  22811  ustinvel  22812  ustexhalf  22813  ust0  22822  elutop  22836  ustuqtop4  22847  cfiluexsm  22893  cfiluweak  22898  blssps  23028  blss  23029  metss  23112  metrest  23128  metcnp3  23144  metnrmlem3  23463  lebnumlem3  23561  lebnum  23562  ellimc3  24471  lhop1lem  24604  dchrelbas  25806  upgredgpr  26921  dfnbgr3  27114  nbupgr  27120  nbumgrvtx  27122  nbgr2vtx1edg  27126  nbuhgr2vtx1edgb  27128  cusgrexilem2  27218  wlkvtxiedg  27400  wlkres  27446  upgr1wlkdlem2  27919  1pthon2v  27926  1pthon2ve  27927  cusconngr  27964  isfrgr  28033  avril1  28236  spanval  29104  spancl  29107  shsval2i  29158  omlsi  29175  ococin  29179  chsupsn  29184  pjoml  29207  shs00i  29221  chj00i  29258  chsscon3  29271  chlejb1  29283  chnle  29285  pjoml2  29382  pjoml3  29383  lecm  29388  stcltr1i  30045  mdbr  30065  dmdmd  30071  dmdi  30073  dmdbr3  30076  dmdbr4  30077  mdsl1i  30092  mdslmd1lem3  30098  mdslmd1lem4  30099  csmdsymi  30105  hatomic  30131  chrelat2  30141  atord  30159  atcvat4i  30168  fz1nntr  30521  isprmidl  30950  mxidlmax  30969  ssmxidllem  30973  ssmxidl  30974  reff  31098  cmpcref  31109  sigagenval  31394  dmsigagen  31398  sigagenss  31403  ldsysgenld  31414  ldgenpisyslem1  31417  ldgenpisyslem2  31418  dynkin  31421  carsgmon  31567  carsgclctunlem2  31572  bnj1286  32286  bnj1452  32319  kur14lem9  32456  mclsssvlem  32804  mclsind  32812  frrlem1  33118  frrlem13  33130  scutun12  33266  imagesset  33409  altopthsn  33417  fnessref  33700  refssfne  33701  topjoin  33708  neifg  33714  bj-snglex  34280  bj-imdirval  34466  relowlssretop  34638  relowlpssretop  34639  exrecfnlem  34654  finxpreclem3  34668  pibt2  34692  poimirlem29  34915  poimir  34919  mblfinlem3  34925  totbndss  35049  heibor1lem  35081  unichnidl  35303  ispridl  35306  maxidlmax  35315  igenval  35333  igenidl  35335  igenmin  35336  igenval2  35338  brssr  35735  lsatcmp  36133  lcvexchlem4  36167  lcvexchlem5  36168  pclvalN  37020  pclclN  37021  elpcliN  37023  docaclN  38254  dihglb2  38472  doch2val2  38494  dochocss  38496  dochexmidlem7  38596  lpolconN  38617  mapdval  38758  nacsfix  39302  mzpcompact2  39342  rgspnval  39761  rgspncl  39762  rgspnmin  39764  superficl  39919  superuncl  39920  cleq2lem  39961  clcnvlem  39976  dfrtrcl3  40071  clsk1indlem2  40385  neik0pk1imk0  40390  isotone1  40391  isotone2  40392  ntrclsiso  40410  gneispacess2  40489  mnuunid  40606  mnurndlem2  40611  ssrecnpr  40633  founiiun  41428  founiiun0  41444  islptre  41893  salgenval  42600  salgenn0  42608  salgencl  42609  sssalgen  42612  salgenss  42613  salgenuni  42614  issalgend  42615  dfsalgen2  42618  salgencntex  42620  isomgreqve  43984  setrec1lem1  44784  setrec1lem3  44786  setrec2fun  44789