Theorem sseq2 4035

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ss 3993

This theorem is referenced by:  sseq12  4036  sseq2i  4038  sseq2d  4041  nssne1  4071  psseq2  4114  sseq0  4426  un00  4468  disjpss  4484  pweqALT  4637  ssintab  4989  ssintub  4990  intmin  4992  treq  5291  al0ssb  5326  sseliALT  5327  ssexg  5341  intabs  5367  iunopeqop  5540  onelssex  6443  ordunidif  6444  ordssun  6497  fununi  6653  feq3  6730  ssimaexg  7008  fnssintima  7398  iunpw  7806  tfindsg  7898  limomss  7908  findsg  7937  funcnvuni  7972  frxp  8167  frrlem1  8327  frrlem13  8339  wrecseq123OLD  8356  wfrlem1OLD  8364  wfrlem4OLD  8368  wfrlem15OLD  8379  onfununi  8397  oawordeu  8611  oawordexr  8612  nnawordex  8693  eldifsucnn  8720  coflton  8727  cofon1  8728  cofon2  8729  cofonr  8730  naddcllem  8732  naddunif  8749  ereq1  8770  xpider  8846  domeng  9022  sbthlem4  9152  sbthlem5  9153  domssex  9204  ssfi  9240  finsschain  9429  dffi2  9492  dffi3  9500  hartogslem1  9611  inf3lema  9693  cantnflem1  9758  dfttrcl2  9793  tz9.1  9798  tz9.1c  9799  tctr  9809  tcmin  9810  tcrank  9953  scottex  9954  cardlim  10041  infxpenlem  10082  infxpenc2  10091  isinfcard  10161  alephinit  10164  alephval3  10179  dfac3  10190  cflem  10314  cflemOLD  10315  cfval  10316  cflecard  10322  cfsuc  10326  cff1  10327  cfflb  10328  cflim2  10332  isf32lem2  10423  fin1a2lem13  10481  ac7g  10543  ttukeylem5  10582  ttukeylem7  10584  pwcfsdom  10652  pwfseqlem5  10732  pwfseq  10733  gch2  10744  winalim  10764  wunex  10808  wuncss  10814  eltskg  10819  eltsk2g  10820  gruina  10887  grur1a  10888  axgroth6  10897  swrdnd2  14703  trcleq2lem  15040  dfrtrcl2  15111  fprodss  15996  mrcflem  17664  mrcval  17668  isacs2  17711  acsfiel  17712  ipoval  18600  fpwipodrs  18610  ipodrsima  18611  mreclatBAD  18633  slwispgp  19653  pgpssslw  19656  lsmss1b  19708  lsmss2b  19710  cntzcmnss  19883  gsumzres  19951  lspf  20995  lspval  20996  lbsextlem1  21183  lbsextlem3  21185  lbsextlem4  21186  aspval  21916  mplsubglem  22042  mpllsslem  22043  basis2  22979  eltg2  22986  clsval  23066  clscld  23076  clsval2  23079  ntrcls0  23105  isnei  23132  neiint  23133  neips  23142  opnneissb  23143  opnssneib  23144  neindisj2  23152  innei  23154  neiptoptop  23160  neiptopnei  23161  neitr  23209  restcls  23210  cnpimaex  23285  cnprest2  23319  regsep  23363  nrmsep3  23384  nrmsep  23386  regsep2  23405  tgcmp  23430  uncmp  23432  bwth  23439  1stcfb  23474  1stcrest  23482  2ndcctbss  23484  1stcelcls  23490  lly1stc  23525  ssref  23541  refref  23542  comppfsc  23561  xkoopn  23618  neitx  23636  txcnp  23649  txcmplem1  23670  kqnrmlem1  23772  kqnrmlem2  23773  nrmhmph  23823  fbssfi  23866  opnfbas  23871  fbasfip  23897  fbunfip  23898  fgss2  23903  fgcl  23907  supfil  23924  isufil2  23937  filssufilg  23940  ssufl  23947  ufileu  23948  elfm3  23979  fmfnfm  23987  ufldom  23991  fbflim2  24006  flfneii  24021  flftg  24025  txflf  24035  supnfcls  24049  fclscf  24054  fclsfnflim  24056  flimfnfcls  24057  alexsubALTlem2  24077  alexsubALTlem3  24078  alexsubALTlem4  24079  alexsubALT  24080  tsmsfbas  24157  tsmsres  24173  tsmsf1o  24174  tsmsxplem1  24182  tsmsxp  24184  ustssel  24235  ustincl  24237  ustdiag  24238  ustinvel  24239  ustexhalf  24240  ust0  24249  elutop  24263  ustuqtop4  24274  cfiluexsm  24320  cfiluweak  24325  blssps  24455  blss  24456  metss  24542  metrest  24558  metcnp3  24574  metnrmlem3  24902  lebnumlem3  25014  lebnum  25015  ellimc3  25934  lhop1lem  26072  dchrelbas  27298  eqscut2  27869  scutun12  27873  madebdayim  27944  madebday  27956  upgredgpr  29177  dfnbgr3  29373  nbupgr  29379  nbumgrvtx  29381  nbgr2vtx1edg  29385  nbuhgr2vtx1edgb  29387  cusgrexilem2  29477  wlkvtxiedg  29661  wlkres  29706  upgr1wlkdlem2  30178  1pthon2v  30185  1pthon2ve  30186  cusconngr  30223  isfrgr  30292  avril1  30495  spanval  31365  spancl  31368  shsval2i  31419  omlsi  31436  ococin  31440  chsupsn  31445  pjoml  31468  shs00i  31482  chj00i  31519  chsscon3  31532  chlejb1  31544  chnle  31546  pjoml2  31643  pjoml3  31644  lecm  31649  stcltr1i  32306  mdbr  32326  dmdmd  32332  dmdi  32334  dmdbr3  32337  dmdbr4  32338  mdsl1i  32353  mdslmd1lem3  32359  mdslmd1lem4  32360  csmdsymi  32366  hatomic  32392  chrelat2  32402  atord  32420  atcvat4i  32429  fz1nntr  32809  fldgenval  33279  fldgensdrg  33281  fldgenssv  33282  fldgenssp  33285  nsgmgc  33405  nsgqusf1olem2  33407  isprmidl  33431  ssdifidllem  33449  ssdifidl  33450  ssdifidlprm  33451  mxidlmax  33458  ssmxidllem  33466  ssmxidl  33467  1arithufdlem4  33540  reff  33785  cmpcref  33796  zarcls1  33815  zarclsiin  33817  zarclssn  33819  zart0  33825  zarmxt1  33826  zarcmp  33828  rhmpreimacnlem  33830  sigagenval  34104  dmsigagen  34108  sigagenss  34113  ldsysgenld  34124  ldgenpisyslem1  34127  ldgenpisyslem2  34128  dynkin  34131  carsgmon  34279  carsgclctunlem2  34284  bnj1286  34995  bnj1452  35028  fineqvac  35073  kur14lem9  35182  mclsssvlem  35530  mclsind  35538  imagesset  35917  altopthsn  35925  fnessref  36323  refssfne  36324  topjoin  36331  neifg  36337  bj-snglex  36939  bj-imdirvallem  37146  relowlssretop  37329  relowlpssretop  37330  exrecfnlem  37345  finxpreclem3  37359  pibt2  37383  poimirlem29  37609  poimir  37613  mblfinlem3  37619  totbndss  37737  heibor1lem  37769  unichnidl  37991  ispridl  37994  maxidlmax  38003  igenval  38021  igenidl  38023  igenmin  38024  igenval2  38026  brssr  38457  lsatcmp  38959  lcvexchlem4  38993  lcvexchlem5  38994  pclvalN  39847  pclclN  39848  elpcliN  39850  docaclN  41081  dihglb2  41299  doch2val2  41321  dochocss  41323  dochexmidlem7  41423  lpolconN  41444  mapdval  41585  nacsfix  42668  mzpcompact2  42708  rgspnval  43125  rgspncl  43126  rgspnmin  43128  superficl  43529  superuncl  43530  cleq2lem  43570  clcnvlem  43585  dfrtrcl3  43695  clsk1indlem2  44004  neik0pk1imk0  44009  isotone1  44010  isotone2  44011  ntrclsiso  44029  gneispacess2  44108  mnuunid  44246  mnurndlem2  44251  ssrecnpr  44277  founiiun  45086  founiiun0  45097  islptre  45540  salgenval  46242  salgenn0  46252  salgencl  46253  sssalgen  46256  salgenss  46257  salgenuni  46258  issalgend  46259  dfsalgen2  46262  salgencntex  46264  dfclnbgr3  47699  predgclnbgrel  47711  clnbgredg  47712  clnbgrgrimlem  47785  clnbgrgrim  47786  opndisj  48582  opnneilem  48585  sepfsepc  48607  iscnrm3rlem8  48627  iscnrm3llem2  48630  intubeu  48656  ipolubdm  48659  ipoglbdm  48662  setrec1lem1  48779  setrec1lem3  48781  setrec2fun  48784