Theorem sseq2 3962

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		eqss 3951	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3943	. . . 4 ⊢ (𝐶 ⊆ 𝐴 → (𝐴 ⊆ 𝐵 → 𝐶 ⊆ 𝐵))
3	2	com12 33	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵))
4		sstr2 3943	. . . 4 ⊢ (𝐶 ⊆ 𝐵 → (𝐵 ⊆ 𝐴 → 𝐶 ⊆ 𝐴))
5	4	com12 33	. . 3 ⊢ (𝐵 ⊆ 𝐴 → (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴))
6	3, 5	anbiim 652	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))
7	1, 6	sylbi 220	1 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1569   ⊆ wss 3904

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-cleq 2754  df-ss 3921

This theorem is used by:  sseq12  3963  sseq2i  3965  sseq2d  3968  nssne1  3998  psseq2  4044  sseq0b  4359  un00  4363  disjpss  4420  pweqALT  4576  ssintab  4929  ssintub  4930  intmin  4932  treq  5224  al0ssb  5270  sseliALT  5271  ssexgOLD  5293  intabs  5318  iunopeqop  5503  iunopeqopOLD  5504  onelssex  6410  ordunidif  6411  ordssun  6465  fununi  6611  feq3  6685  ssimaexg  6967  fnssintima  7362  iunpw  7768  tfindsg  7855  limomss  7865  findsg  7892  funcnvuni  7927  frxp  8120  frrlem1  8281  frrlem13  8293  onfununi  8326  oawordeu  8538  oawordexr  8539  nnawordex  8621  eldifsucnn  8648  coflton  8655  cofon1  8656  cofon2  8657  cofonr  8658  naddcllem  8660  naddunif  8678  ereq1  8700  xpider  8784  domeng  8957  sbthlem4  9076  sbthlem5  9077  domssex  9124  ssfi  9155  finsschain  9314  dffi2  9381  dffi3  9389  hartogslem1  9502  inf3lema  9591  cantnflem1  9656  dfttrcl2  9691  tz9.1  9696  tz9.1c  9697  tctr  9705  tcmin  9706  tcrank  9854  scottex  9860  scottexOLD  9861  cardlim  9965  infxpenlem  10004  infxpenc2  10013  isinfcard  10083  alephinit  10086  alephval3  10101  dfac3  10112  cflem  10235  cfval  10236  cflecard  10242  cfsuc  10247  cff1  10248  cfflb  10249  cflim2  10253  isf32lem2  10344  fin1a2lem13  10402  ac7g  10464  ttukeylem5  10503  ttukeylem7  10505  pwcfsdom  10574  pwfseqlem5  10654  pwfseq  10655  gch2  10666  winalim  10686  wunex  10730  wuncss  10736  eltskg  10741  eltsk2g  10742  gruina  10809  grur1a  10810  axgroth6  10819  swrdnd2  14700  trcleq2lem  15035  dfrtrcl2  15106  fprodss  16009  mrcflem  17668  mrcval  17672  isacs2  17715  acsfiel  17716  ipoval  18592  fpwipodrs  18602  ipodrsima  18603  mreclatBAD  18625  slwispgp  19687  pgpssslw  19690  lsmss1b  19742  lsmss2b  19744  cntzcmnss  19917  gsumzres  19985  rgspnval  20722  rgspncl  20723  rgspnmin  20725  lspf  21106  lspval  21107  lbsextlem1  21293  lbsextlem3  21295  lbsextlem4  21296  unichnlidl  21373  rspprop  21381  isprmidl  21474  ssdifidllem  21495  ssdifidl  21496  ssdifidlprm  21497  aspval  22033  mplsubglem  22159  mpllsslem  22160  basis2  23119  eltg2  23126  clsval  23205  clscld  23215  clsval2  23218  ntrcls0  23244  isnei  23271  neiint  23272  neips  23281  opnneissb  23282  opnssneib  23283  neindisj2  23291  innei  23293  neiptoptop  23299  neiptopnei  23300  neitr  23348  restcls  23349  cnpimaex  23424  cnprest2  23458  regsep  23502  nrmsep3  23523  nrmsep  23525  regsep2  23544  tgcmp  23569  uncmp  23571  bwth  23578  1stcfb  23613  1stcrest  23621  2ndcctbss  23623  1stcelcls  23629  lly1stc  23664  ssref  23680  refref  23681  comppfsc  23700  xkoopn  23757  neitx  23775  txcnp  23788  txcmplem1  23809  kqnrmlem1  23911  kqnrmlem2  23912  nrmhmph  23962  fbssfi  24005  opnfbas  24010  fbasfip  24036  fbunfip  24037  fgss2  24042  fgcl  24046  supfil  24063  isufil2  24076  filssufilg  24079  ssufl  24086  ufileu  24087  elfm3  24118  fmfnfm  24126  ufldom  24130  fbflim2  24145  flfneii  24160  flftg  24164  txflf  24174  supnfcls  24188  fclscf  24193  fclsfnflim  24195  flimfnfcls  24196  alexsubALTlem2  24216  alexsubALTlem3  24217  alexsubALTlem4  24218  alexsubALT  24219  tsmsfbas  24296  tsmsres  24312  tsmsf1o  24313  tsmsxplem1  24321  tsmsxp  24323  ustssel  24374  ustincl  24376  ustdiag  24377  ustinvel  24378  ustexhalf  24379  ust0  24388  elutop  24401  ustuqtop4  24412  cfiluexsm  24457  cfiluweak  24462  blssps  24592  blss  24593  metss  24676  metrest  24692  metcnp3  24708  metnrmlem3  25030  lebnumlem3  25133  lebnum  25134  ellimc3  26049  lhop1lem  26183  dchrelbas  27411  eqcuts2  27990  cutsun12  27994  madebdayim  28092  madebday  28104  oniso  28475  bdayn0p1  28573  prlngd  29200  dfprlng2  29208  upgredgpr  29503  dfnbgr3  29699  nbupgr  29705  nbumgrvtx  29707  nbgr2vtx1edg  29711  nbuhgr2vtx1edgb  29713  cusgrexilem2  29803  wlkvtxiedg  29985  wlkres  30029  upgr1wlkdlem2  30508  1pthon2v  30515  1pthon2ve  30516  cusconngr  30553  isfrgr  30622  avril1  30825  spanval  31696  spancl  31699  shsval2i  31750  omlsi  31767  ococin  31771  chsupsn  31776  pjoml  31799  shs00i  31813  chj00i  31850  chsscon3  31863  chlejb1  31875  chnle  31877  pjoml2  31974  pjoml3  31975  lecm  31980  stcltr1i  32637  mdbr  32657  dmdmd  32663  dmdi  32665  dmdbr3  32668  dmdbr4  32669  mdsl1i  32684  mdslmd1lem3  32690  mdslmd1lem4  32691  csmdsymi  32697  hatomic  32723  chrelat2  32733  atord  32751  atcvat4i  32760  fz1nntr  33158  elrgspnlem4  33574  fldgenval  33642  fldgensdrg  33644  fldgenssv  33645  fldgenssp  33648  nsgmgc  33730  nsgqusf1olem2  33732  mxidlmax  33757  ssmxidllem  33765  ssmxidl  33766  dflringlem  33793  1arithufdlem4  33846  reff  34238  cmpcref  34249  zarcls1  34268  zarclsiin  34270  zarclssn  34272  zart0  34278  zarmxt1  34279  zarcmp  34281  rhmpreimacnlem  34283  sigagenval  34539  dmsigagen  34543  sigagenss  34548  ldsysgenld  34559  ldgenpisyslem1  34562  ldgenpisyslem2  34563  dynkin  34566  carsgmon  34713  carsgclctunlem2  34718  bnj1286  35416  bnj1452  35449  fineqvac  35537  tz9.1regs  35555  onvf1odlem4  35598  vonf1wev  35600  vonf1owevOLD  35602  kur14lem9  35714  mclsssvlem  36062  mclsind  36070  imagesset  36453  altopthsn  36461  fnessref  36896  refssfne  36897  topjoin  36904  neifg  36910  tz9.1tco  37022  ttc00  37047  dfttc3gw  37062  bj-snglex  37637  bj-imdirvallem  37852  relowlssretop  38037  relowlpssretop  38038  exrecfnlem  38053  finxpreclem3  38067  pibt2  38091  poimirlem29  38328  poimir  38332  mblfinlem3  38338  totbndss  38456  heibor1lem  38488  unichnidl  38710  ispridl  38713  maxidlmax  38722  igenval  38740  igenidl  38742  igenmin  38743  igenval2  38745  dfsuccl4  39151  brssr  39258  suceldisj  39495  lsatcmp  39805  lcvexchlem4  39839  lcvexchlem5  39840  pclvalN  40692  pclclN  40693  elpcliN  40695  docaclN  41926  dihglb2  42144  doch2val2  42166  dochocss  42168  dochexmidlem7  42268  lpolconN  42289  mapdval  42430  nacsfix  43471  mzpcompact2  43511  superficl  44321  superuncl  44322  cleq2lem  44362  clcnvlem  44377  dfrtrcl3  44487  clsk1indlem2  44796  neik0pk1imk0  44801  isotone1  44802  isotone2  44803  ntrclsiso  44821  gneispacess2  44900  mnuunid  45015  mnurndlem2  45020  ssrecnpr  45046  founiiun  45925  founiiun0  45936  islptre  46363  salgenval  47063  salgenn0  47073  salgencl  47074  sssalgen  47077  salgenss  47078  salgenuni  47079  issalgend  47080  dfsalgen2  47083  salgencntex  47085  dfclnbgr3  48619  predgclnbgrel  48632  clnbgredg  48633  clnbgrgrimlem  48726  clnbgrgrim  48727  opndisj  49709  opnneilem  49712  sepfsepc  49734  iscnrm3rlem8  49753  iscnrm3llem2  49756  intubeu  49790  ipolubdm  49793  ipoglbdm  49796  setrec1lem1  50493  setrec1lem3  50495  setrec2fun  50498