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

Theorem dfss3 3787
Description: Alternate definition of subclass relationship. (Contributed by NM, 14-Oct-1999.)
Assertion
Ref Expression
dfss3 (𝐴𝐵 ↔ ∀𝑥𝐴 𝑥𝐵)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem dfss3
StepHypRef Expression
1 dfss2 3786 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
2 df-ral 3101 . 2 (∀𝑥𝐴 𝑥𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
31, 2bitr4i 269 1 (𝐴𝐵 ↔ ∀𝑥𝐴 𝑥𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wal 1635  wcel 2156  wral 3096  wss 3769
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-ral 3101  df-in 3776  df-ss 3783
This theorem is referenced by:  ssrab  3877  dfss5  4066  elpwunsn  4417  ssdifsnOLD  4510  eqsn  4550  uni0b  4657  uni0c  4658  ssint  4685  ssiinf  4761  sspwuni  4803  dftr3  4950  wefrc  5305  rninxp  5784  wfisg  5928  ordunisssuc  6039  fnres  6214  eqfnfv3  6531  funimass3  6551  ffvresb  6612  tfis  7280  smogt  7696  unifi  8490  unifi2  8491  fissuni  8506  fipreima  8507  cantnf  8833  tz9.12lem3  8895  r1elss  8912  rankval3b  8932  rankonidlem  8934  bndrank  8947  iscard  9080  cfub  9352  cflm  9353  fin1a2s  9517  dcomex  9550  ttukeylem6  9617  unirnfdomd  9670  alephreg  9685  tskord  9883  gruuni  9903  intgru  9917  grudomon  9920  axgroth3  9934  suplem1pr  10155  supexpr  10157  supsr  10214  hashfun  13437  4sqlem19  15880  imasaddfnlem  16389  imasvscafn  16398  setcepi  16938  acsfiindd  17378  sylow2blem3  18234  sylow3lem6  18244  efgval2  18334  iscyggen2  18480  iscyg3  18485  issubdrg  19005  isdomn2  19504  ishil2  20270  rintopn  20924  isbasis2g  20963  tgval2  20971  eltg2b  20974  tgss2  21002  basgen2  21004  bastop1  21008  intcld  21055  unicld  21061  isclo  21102  isclo2  21103  neips  21128  opnnei  21135  neiptopnei  21147  isperf3  21168  ssidcn  21270  ist1-3  21364  cmpcov2  21404  cmpsub  21414  2ndcdisj2  21471  txkgen  21666  xkoinjcn  21701  tgqtop  21726  flimopn  21989  flfnei  22005  tmdcn2  22103  qustgplem  22134  cfil3i  23277  cmetcaulem  23296  ovolfioo  23447  ovolficc  23448  ovolicc2lem4  23500  opnmblALT  23583  xrlimcnp  24908  uvtxnbgrss  26511  iscplgr  26537  cplgruvtxbOLD  26538  vdiscusgrb  26653  ubthlem1  28053  hasheuni  30471  dmvlsiga  30516  ispisys2  30540  omssubadd  30686  eulerpartlemr  30760  eulerpartlemn  30767  cvmlift2lem1  31605  cvmlift2lem12  31617  mclsax  31787  setinds  32001  tfisg  32034  frpoinsg  32060  frinsg  32064  isfne4  32654  isfne2  32656  isfne3  32657  neibastop2lem  32674  filnetlem4  32695  fin2so  33707  poimirlem24  33744  poimirlem27  33747  nninfnub  33856  unichnidl  34139  ispridl2  34146  n0elqs  34411  pmapglb  35548  hdmapoc  37709  isnacs2  37768  setindtrs  38090  dford3lem2  38092  dford3  38093  ntrneicls00  38884  ntrneixb  38890  ntrneik3  38891  ntrneix3  38892  ntrneik13  38893  ntrneix13  38894  pwssfi  39701  ssdf  39737  ballss3  39760  iunincfi  39762  restuni3  39790  iinssiin  39800  disjf1o  39864  mapss2  39881  difmap  39883  unirnmap  39884  inmap  39885  difmapsn  39888  uzfissfz  40019  iuneqfzuzlem  40027  ssuzfz  40042  iccdificc  40243  iooiinicc  40246  ressiocsup  40258  ressioosup  40259  iooiinioc  40260  ressiooinf  40261  fsumiunss  40284  limciccioolb  40330  limcicciooub  40346  limcresiooub  40351  limsupresxr  40475  liminfresxr  40476  icccncfext  40577  dmvolss  40678  stoweidlem31  40724  stoweidlem39  40732  fourierdlem8  40808  fourierdlem27  40827  fourierdlem38  40838  fourierdlem40  40840  fourierdlem41  40841  fourierdlem46  40845  fourierdlem48  40847  fourierdlem49  40848  fourierdlem51  40850  fourierdlem53  40852  fourierdlem64  40863  fourierdlem70  40869  fourierdlem71  40870  fourierdlem76  40875  fourierdlem78  40877  fourierdlem79  40878  fourierdlem80  40879  fourierdlem93  40892  fourierdlem97  40896  fourierdlem103  40902  fourierdlem104  40903  salexct  41028  salgencntex  41037  gsumge0cl  41064  sge0fodjrnlem  41109  sge0reuz  41140  iundjiun  41153  icoresmbl  41236  hoicvr  41241  hoidmv1le  41287  hoidmvlelem1  41288  hoidmvlelem3  41290  hoiqssbllem2  41316  hspmbllem2  41320  opnvonmbllem2  41326  iinhoiicc  41367  smfpimbor1lem2  41485  setrec1lem2  43000  setrec1lem3  43001
  Copyright terms: Public domain W3C validator