MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sseqin2 Structured version   Visualization version   GIF version

Theorem sseqin2 3850
Description: A relationship between subclass and intersection. Similar to Exercise 9 of [TakeutiZaring] p. 18. (Contributed by NM, 17-May-1994.)
Assertion
Ref Expression
sseqin2 (𝐴𝐵 ↔ (𝐵𝐴) = 𝐴)

Proof of Theorem sseqin2
StepHypRef Expression
1 df-ss 3621 . 2 (𝐴𝐵 ↔ (𝐴𝐵) = 𝐴)
2 incom 3838 . . 3 (𝐴𝐵) = (𝐵𝐴)
32eqeq1i 2656 . 2 ((𝐴𝐵) = 𝐴 ↔ (𝐵𝐴) = 𝐴)
41, 3bitri 264 1 (𝐴𝐵 ↔ (𝐵𝐴) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1523  cin 3606  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-in 3614  df-ss 3621
This theorem is referenced by:  dfss5OLD  3852  sseqin2OLD  3865  dfss4  3891  rintn0  4651  resabs1  5462  resima2  5467  xpssres  5469  rescnvcnv  5632  sspred  5726  onfr  5801  ordtri2or3  5862  fndmdif  6361  fimacnvinrn2  6389  fveqressseq  6395  sorpssin  6987  predon  7033  omsinds  7126  cnvoprab  7274  frnsuppeq  7352  wfrlem4  7463  fiint  8278  infxpenlem  8874  acndom2  8915  ackbij1lem2  9081  isf34lem5  9238  fpwwe2  9503  uzin  11758  iooval2  12246  fzval2  12367  leiso  13281  fz1isolem  13283  isercolllem3  14441  incexc  14613  bitsinv1  15211  bitsinvp1  15218  bitsshft  15244  dfphi2  15526  ressbas  15977  ressress  15985  ressabs  15986  psssdm  17263  sylow3lem2  18089  gsumxp  18421  dprdsn  18481  ablfac1eu  18518  pgpfac1lem5  18524  ablfaclem3  18532  ocv1  20071  resttopon  21013  restabs  21017  restopnb  21027  restperf  21036  ordtbas  21044  ordtrest2lem  21055  ordtrest2  21056  leordtvallem1  21062  leordtvallem2  21063  cnclsi  21124  ordtt1  21231  cmpsub  21251  connsub  21272  cnconn  21273  nconnsubb  21274  connsubclo  21275  1stcfb  21296  kgentopon  21389  ptbasfi  21432  ptclsg  21466  dfac14lem  21468  xkoccn  21470  txcnmpt  21475  txtube  21491  xkoptsub  21505  xkopt  21506  kqsat  21582  kqcldsat  21584  ordthmeolem  21652  fbasrn  21735  trfil1  21737  trfil2  21738  trufil  21761  qustgphaus  21973  trust  22080  metustfbas  22409  cfilucfil  22411  xrsmopn  22662  lebnumii  22812  iscmet3  23137  resscdrg  23200  cmmbl  23348  voliunlem3  23366  uniioombllem4  23400  mbflimsup  23478  0plef  23484  0pledm  23485  itg1ge0  23498  mbfi1fseqlem5  23531  itg2addlem  23570  dvcmulf  23753  lhop1  23822  lhop2  23823  efopn  24449  wilthlem2  24840  ex-in  27412  cmcmlem  28578  pjvec  28683  pjocvec  28684  ssmd2  29299  mdslmd4i  29320  chirredlem2  29378  chirredlem3  29379  dmdbr7ati  29411  difuncomp  29495  xppreima  29577  gtiso  29606  resf1o  29633  prsss  30090  ordtrestNEW  30095  ordtrest2NEWlem  30096  ordtrest2NEW  30097  lmxrge0  30126  carsggect  30508  probdsb  30612  totprobd  30616  cndprobtot  30626  orvcelval  30658  ballotlemfmpn  30684  signsplypnf  30755  signsply0  30756  dfon2lem4  31815  frrlem4  31908  neibastop3  32482  bj-restsnss  33161  bj-ismoored2  33188  bj-ismooredr2  33190  topdifinfeq  33328  poimirlem3  33542  poimirlem9  33548  mblfinlem3  33578  mblfinlem4  33579  itg2addnclem2  33592  blssp  33682  sstotbnd2  33703  lcvexchlem1  34639  lcvexchlem4  34642  glbconN  34981  pmapglb2N  35375  pmapglb2xN  35376  2polssN  35519  polatN  35535  osumcllem1N  35560  osumcllem9N  35568  pexmidlem6N  35579  diarnN  36735  dihmeetlem11N  36923  dochexmidlem6  37071  lclkrlem2r  37130  mapdunirnN  37256  rfovcnvf1od  38615  fsovcnvlem  38624  ntrneifv3  38697  ntrneifv4  38700  clsneifv3  38725  clsneifv4  38726  neicvgfv  38736  k0004lem2  38763  wnefimgd  38777  inabs3  39538  mptima2  39771  stoweidlem50  40585  sge0iunmptlemre  40950  caratheodorylem1  41061  smfconst  41279
  Copyright terms: Public domain W3C validator