Theorem sseq2 4021

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-ss 3979

This theorem is referenced by:  sseq12  4022  sseq2i  4024  sseq2d  4027  nssne1  4057  psseq2  4100  sseq0  4408  un00  4450  disjpss  4466  pweqALT  4619  ssintab  4969  ssintub  4970  intmin  4972  treq  5272  al0ssb  5313  sseliALT  5314  ssexg  5328  intabs  5354  iunopeqop  5530  onelssex  6433  ordunidif  6434  ordssun  6487  fununi  6642  feq3  6718  ssimaexg  6994  fnssintima  7381  iunpw  7789  tfindsg  7881  limomss  7891  findsg  7919  funcnvuni  7954  frxp  8149  frrlem1  8309  frrlem13  8321  wrecseq123OLD  8338  wfrlem1OLD  8346  wfrlem4OLD  8350  wfrlem15OLD  8361  onfununi  8379  oawordeu  8591  oawordexr  8592  nnawordex  8673  eldifsucnn  8700  coflton  8707  cofon1  8708  cofon2  8709  cofonr  8710  naddcllem  8712  naddunif  8729  ereq1  8750  xpider  8826  domeng  9001  sbthlem4  9124  sbthlem5  9125  domssex  9176  ssfi  9211  finsschain  9396  dffi2  9460  dffi3  9468  hartogslem1  9579  inf3lema  9661  cantnflem1  9726  dfttrcl2  9761  tz9.1  9766  tz9.1c  9767  tctr  9777  tcmin  9778  tcrank  9921  scottex  9922  cardlim  10009  infxpenlem  10050  infxpenc2  10059  isinfcard  10129  alephinit  10132  alephval3  10147  dfac3  10158  cflem  10282  cflemOLD  10283  cfval  10284  cflecard  10290  cfsuc  10294  cff1  10295  cfflb  10296  cflim2  10300  isf32lem2  10391  fin1a2lem13  10449  ac7g  10511  ttukeylem5  10550  ttukeylem7  10552  pwcfsdom  10620  pwfseqlem5  10700  pwfseq  10701  gch2  10712  winalim  10732  wunex  10776  wuncss  10782  eltskg  10787  eltsk2g  10788  gruina  10855  grur1a  10856  axgroth6  10865  swrdnd2  14689  trcleq2lem  15026  dfrtrcl2  15097  fprodss  15980  mrcflem  17650  mrcval  17654  isacs2  17697  acsfiel  17698  ipoval  18587  fpwipodrs  18597  ipodrsima  18598  mreclatBAD  18620  slwispgp  19643  pgpssslw  19646  lsmss1b  19698  lsmss2b  19700  cntzcmnss  19873  gsumzres  19941  rgspnval  20628  rgspncl  20629  rgspnmin  20631  lspf  20989  lspval  20990  lbsextlem1  21177  lbsextlem3  21179  lbsextlem4  21180  aspval  21910  mplsubglem  22036  mpllsslem  22037  basis2  22973  eltg2  22980  clsval  23060  clscld  23070  clsval2  23073  ntrcls0  23099  isnei  23126  neiint  23127  neips  23136  opnneissb  23137  opnssneib  23138  neindisj2  23146  innei  23148  neiptoptop  23154  neiptopnei  23155  neitr  23203  restcls  23204  cnpimaex  23279  cnprest2  23313  regsep  23357  nrmsep3  23378  nrmsep  23380  regsep2  23399  tgcmp  23424  uncmp  23426  bwth  23433  1stcfb  23468  1stcrest  23476  2ndcctbss  23478  1stcelcls  23484  lly1stc  23519  ssref  23535  refref  23536  comppfsc  23555  xkoopn  23612  neitx  23630  txcnp  23643  txcmplem1  23664  kqnrmlem1  23766  kqnrmlem2  23767  nrmhmph  23817  fbssfi  23860  opnfbas  23865  fbasfip  23891  fbunfip  23892  fgss2  23897  fgcl  23901  supfil  23918  isufil2  23931  filssufilg  23934  ssufl  23941  ufileu  23942  elfm3  23973  fmfnfm  23981  ufldom  23985  fbflim2  24000  flfneii  24015  flftg  24019  txflf  24029  supnfcls  24043  fclscf  24048  fclsfnflim  24050  flimfnfcls  24051  alexsubALTlem2  24071  alexsubALTlem3  24072  alexsubALTlem4  24073  alexsubALT  24074  tsmsfbas  24151  tsmsres  24167  tsmsf1o  24168  tsmsxplem1  24176  tsmsxp  24178  ustssel  24229  ustincl  24231  ustdiag  24232  ustinvel  24233  ustexhalf  24234  ust0  24243  elutop  24257  ustuqtop4  24268  cfiluexsm  24314  cfiluweak  24319  blssps  24449  blss  24450  metss  24536  metrest  24552  metcnp3  24568  metnrmlem3  24896  lebnumlem3  25008  lebnum  25009  ellimc3  25928  lhop1lem  26066  dchrelbas  27294  eqscut2  27865  scutun12  27869  madebdayim  27940  madebday  27952  upgredgpr  29173  dfnbgr3  29369  nbupgr  29375  nbumgrvtx  29377  nbgr2vtx1edg  29381  nbuhgr2vtx1edgb  29383  cusgrexilem2  29473  wlkvtxiedg  29657  wlkres  29702  upgr1wlkdlem2  30174  1pthon2v  30181  1pthon2ve  30182  cusconngr  30219  isfrgr  30288  avril1  30491  spanval  31361  spancl  31364  shsval2i  31415  omlsi  31432  ococin  31436  chsupsn  31441  pjoml  31464  shs00i  31478  chj00i  31515  chsscon3  31528  chlejb1  31540  chnle  31542  pjoml2  31639  pjoml3  31640  lecm  31645  stcltr1i  32302  mdbr  32322  dmdmd  32328  dmdi  32330  dmdbr3  32333  dmdbr4  32334  mdsl1i  32349  mdslmd1lem3  32355  mdslmd1lem4  32356  csmdsymi  32362  hatomic  32388  chrelat2  32398  atord  32416  atcvat4i  32425  fz1nntr  32811  elrgspnlem4  33234  fldgenval  33293  fldgensdrg  33295  fldgenssv  33296  fldgenssp  33299  nsgmgc  33419  nsgqusf1olem2  33421  isprmidl  33445  ssdifidllem  33463  ssdifidl  33464  ssdifidlprm  33465  mxidlmax  33472  ssmxidllem  33480  ssmxidl  33481  1arithufdlem4  33554  reff  33799  cmpcref  33810  zarcls1  33829  zarclsiin  33831  zarclssn  33833  zart0  33839  zarmxt1  33840  zarcmp  33842  rhmpreimacnlem  33844  sigagenval  34120  dmsigagen  34124  sigagenss  34129  ldsysgenld  34140  ldgenpisyslem1  34143  ldgenpisyslem2  34144  dynkin  34147  carsgmon  34295  carsgclctunlem2  34300  bnj1286  35011  bnj1452  35044  fineqvac  35089  kur14lem9  35198  mclsssvlem  35546  mclsind  35554  imagesset  35934  altopthsn  35942  fnessref  36339  refssfne  36340  topjoin  36347  neifg  36353  bj-snglex  36955  bj-imdirvallem  37162  relowlssretop  37345  relowlpssretop  37346  exrecfnlem  37361  finxpreclem3  37375  pibt2  37399  poimirlem29  37635  poimir  37639  mblfinlem3  37645  totbndss  37763  heibor1lem  37795  unichnidl  38017  ispridl  38020  maxidlmax  38029  igenval  38047  igenidl  38049  igenmin  38050  igenval2  38052  brssr  38482  lsatcmp  38984  lcvexchlem4  39018  lcvexchlem5  39019  pclvalN  39872  pclclN  39873  elpcliN  39875  docaclN  41106  dihglb2  41324  doch2val2  41346  dochocss  41348  dochexmidlem7  41448  lpolconN  41469  mapdval  41610  nacsfix  42699  mzpcompact2  42739  superficl  43556  superuncl  43557  cleq2lem  43597  clcnvlem  43612  dfrtrcl3  43722  clsk1indlem2  44031  neik0pk1imk0  44036  isotone1  44037  isotone2  44038  ntrclsiso  44056  gneispacess2  44135  mnuunid  44272  mnurndlem2  44277  ssrecnpr  44303  founiiun  45121  founiiun0  45132  islptre  45574  salgenval  46276  salgenn0  46286  salgencl  46287  sssalgen  46290  salgenss  46291  salgenuni  46292  issalgend  46293  dfsalgen2  46296  salgencntex  46298  dfclnbgr3  47750  predgclnbgrel  47762  clnbgredg  47763  clnbgrgrimlem  47838  clnbgrgrim  47839  opndisj  48698  opnneilem  48701  sepfsepc  48723  iscnrm3rlem8  48743  iscnrm3llem2  48746  intubeu  48772  ipolubdm  48775  ipoglbdm  48778  setrec1lem1  48917  setrec1lem3  48919  setrec2fun  48922