Theorem sseq2 3627

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 3610	. . . 4 ⊢ (𝐶 ⊆ 𝐴 → (𝐴 ⊆ 𝐵 → 𝐶 ⊆ 𝐵))
2	1	com12 32	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵))
3		sstr2 3610	. . . 4 ⊢ (𝐶 ⊆ 𝐵 → (𝐵 ⊆ 𝐴 → 𝐶 ⊆ 𝐴))
4	3	com12 32	. . 3 ⊢ (𝐵 ⊆ 𝐴 → (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴))
5	2, 4	anim12i 590	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → ((𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵) ∧ (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴)))
6		eqss 3618	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
7		dfbi2 660	. 2 ⊢ ((𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵) ↔ ((𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵) ∧ (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴)))
8	5, 6, 7	3imtr4i 281	1 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1483   ⊆ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  sseq12  3628  sseq2i  3630  sseq2d  3633  syl5sseq  3653  nssne1  3661  psseq2  3695  sseq0  3975  un00  4011  disjpss  4028  pweq  4161  ssintab  4494  ssintub  4495  intmin  4497  treq  4758  sseliALT  4791  ssexg  4804  intabs  4825  iunopeqop  4981  ordunidif  5773  ordssun  5827  fununi  5964  feq3  6028  ssimaexg  6264  iunpw  6978  tfindsg  7060  limomss  7070  findsg  7093  funcnvuni  7119  frxp  7287  wrecseq123  7408  wfrlem1  7414  wfrlem4  7418  wfrlem15  7429  onfununi  7438  oawordeu  7635  oawordexr  7636  nnawordex  7717  ereq1  7749  xpider  7818  domeng  7969  sbthlem4  8073  sbthlem5  8074  domssex  8121  finsschain  8273  dffi2  8329  dffi3  8337  hartogslem1  8447  inf3lema  8521  cantnflem1  8586  tz9.1  8605  tz9.1c  8606  tctr  8616  tcmin  8617  tcrank  8747  scottex  8748  cardlim  8798  infxpenlem  8836  infxpenc2  8845  isinfcard  8915  alephinit  8918  alephval3  8933  dfac3  8944  cflem  9068  cfval  9069  cflecard  9075  cfsuc  9079  cff1  9080  cfflb  9081  cflim2  9085  isf32lem2  9176  fin1a2lem13  9234  ac7g  9296  ttukeylem5  9335  ttukeylem7  9337  pwcfsdom  9405  pwfseqlem5  9485  pwfseq  9486  gch2  9497  winalim  9517  wunex  9561  wuncss  9567  eltskg  9572  eltsk2g  9573  gruina  9640  grur1a  9641  axgroth6  9650  swrdnd2  13433  trcleq2lem  13730  dfrtrcl2  13802  fprodss  14678  mrcflem  16266  mrcval  16270  isacs2  16314  acsfiel  16315  ipoval  17154  fpwipodrs  17164  ipodrsima  17165  mreclatBAD  17187  slwispgp  18026  pgpssslw  18029  lsmss1b  18080  lsmss2b  18082  cntzcmnss  18246  gsumzres  18310  lspf  18974  lspval  18975  lbsextlem1  19158  lbsextlem3  19160  lbsextlem4  19161  aspval  19328  mplsubglem  19434  mpllsslem  19435  basis2  20755  eltg2  20762  clsval  20841  clscld  20851  clsval2  20854  ntrcls0  20880  isnei  20907  neiint  20908  neips  20917  opnneissb  20918  opnssneib  20919  neindisj2  20927  innei  20929  neiptoptop  20935  neiptopnei  20936  neitr  20984  restcls  20985  cnpimaex  21060  cnprest2  21094  regsep  21138  nrmsep3  21159  nrmsep  21161  regsep2  21180  tgcmp  21204  uncmp  21206  bwth  21213  1stcfb  21248  1stcrest  21256  2ndcctbss  21258  1stcelcls  21264  lly1stc  21299  ssref  21315  refref  21316  comppfsc  21335  xkoopn  21392  neitx  21410  txcnp  21423  txcmplem1  21444  kqnrmlem1  21546  kqnrmlem2  21547  nrmhmph  21597  fbssfi  21641  opnfbas  21646  fbasfip  21672  fbunfip  21673  fgss2  21678  fgcl  21682  supfil  21699  isufil2  21712  filssufilg  21715  ssufl  21722  ufileu  21723  elfm3  21754  fmfnfm  21762  ufldom  21766  fbflim2  21781  flfneii  21796  flftg  21800  txflf  21810  supnfcls  21824  fclscf  21829  fclsfnflim  21831  flimfnfcls  21832  alexsubALTlem2  21852  alexsubALTlem3  21853  alexsubALTlem4  21854  alexsubALT  21855  tsmsfbas  21931  tsmsres  21947  tsmsf1o  21948  tsmsxplem1  21956  tsmsxp  21958  ustssel  22009  ustincl  22011  ustdiag  22012  ustinvel  22013  ustexhalf  22014  ust0  22023  elutop  22037  ustuqtop4  22048  cfiluexsm  22094  cfiluweak  22099  blssps  22229  blss  22230  metss  22313  metrest  22329  metcnp3  22345  metnrmlem3  22664  lebnumlem3  22762  lebnum  22763  ellimc3  23643  lhop1lem  23776  dchrelbas  24961  upgredgpr  26037  dfnbgr3  26236  nbupgr  26240  nbumgrvtx  26242  nbgr2vtx1edg  26246  nbuhgr2vtx1edgb  26248  cusgrexilem2  26338  wlkvtxiedg  26520  wlkres  26567  upgr1wlkdlem2  27006  1pthon2v  27013  1pthon2ve  27014  cusconngr  27051  avril1  27319  spanval  28192  spancl  28195  shsval2i  28246  omlsi  28263  ococin  28267  chsupsn  28272  pjoml  28295  shs00i  28309  chj00i  28346  chsscon3  28359  chlejb1  28371  chnle  28373  pjoml2  28470  pjoml3  28471  lecm  28476  stcltr1i  29133  mdbr  29153  dmdmd  29159  dmdi  29161  dmdbr3  29164  dmdbr4  29165  mdsl1i  29180  mdslmd1lem3  29186  mdslmd1lem4  29187  csmdsymi  29193  hatomic  29219  chrelat2  29229  atord  29247  atcvat4i  29256  fz1nntr  29561  reff  29906  cmpcref  29917  sigagenval  30203  dmsigagen  30207  sigagenss  30212  ldsysgenld  30223  ldgenpisyslem1  30226  ldgenpisyslem2  30227  dynkin  30230  carsgmon  30376  carsgclctunlem2  30381  bnj1286  31087  bnj1452  31120  kur14lem9  31196  mclsssvlem  31459  mclsind  31467  frrlem1  31780  frrlem4  31783  frrlem5e  31788  frrlem11  31792  scutun12  31917  imagesset  32060  altopthsn  32068  fnessref  32352  refssfne  32353  topjoin  32360  neifg  32366  bj-snglex  32961  relowlssretop  33211  relowlpssretop  33212  finxpreclem3  33230  poimirlem29  33438  poimir  33442  mblfinlem3  33448  totbndss  33576  heibor1lem  33608  unichnidl  33830  ispridl  33833  maxidlmax  33842  igenval  33860  igenidl  33862  igenmin  33863  igenval2  33865  lsatcmp  34290  lcvexchlem4  34324  lcvexchlem5  34325  pclvalN  35176  pclclN  35177  elpcliN  35179  docaclN  36413  dihglb2  36631  doch2val2  36653  dochocss  36655  dochexmidlem7  36755  lpolconN  36776  mapdval  36917  nacsfix  37275  mzpcompact2  37315  rgspnval  37738  rgspncl  37739  rgspnmin  37741  superficl  37872  superuncl  37873  cleq2lem  37914  clcnvlem  37930  dfrtrcl3  38025  clsk1indlem2  38340  neik0pk1imk0  38345  isotone1  38346  isotone2  38347  ntrclsiso  38365  gneispacess2  38444  ssrecnpr  38507  founiiun  39360  founiiun0  39377  islptre  39851  salgenval  40541  salgenn0  40549  salgencl  40550  sssalgen  40553  salgenss  40554  salgenuni  40555  issalgend  40556  dfsalgen2  40559  salgencntex  40561  setrec1lem1  42434  setrec1lem3  42436  setrec2fun  42439