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

Theorem dfss3 3953
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 3952 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
2 df-ral 3140 . 2 (∀𝑥𝐴 𝑥𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
31, 2bitr4i 279 1 (𝐴𝐵 ↔ ∀𝑥𝐴 𝑥𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wal 1526  wcel 2105  wral 3135  wss 3933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-ral 3140  df-in 3940  df-ss 3949
This theorem is referenced by:  ssrab  4046  dfss5  4238  elpwunsn  4613  eqsn  4754  uni0b  4855  uni0c  4856  ssint  4883  ssiinf  4969  sspwuni  5013  dftr3  5167  wefrc  5542  rninxp  6029  wfisg  6176  ordunisssuc  6286  fnres  6467  eqfnfv3  6796  funimass3  6816  ffvresb  6880  tfis  7558  smogt  7993  unifi  8801  unifi2  8802  fissuni  8817  fipreima  8818  cantnf  9144  tz9.12lem3  9206  r1elss  9223  rankval3b  9243  rankonidlem  9245  bndrank  9258  iscard  9392  cfub  9659  cflm  9660  fin1a2s  9824  dcomex  9857  ttukeylem6  9924  unirnfdomd  9977  alephreg  9992  tskord  10190  gruuni  10210  intgru  10224  grudomon  10227  axgroth3  10241  suplem1pr  10462  supexpr  10464  supsr  10522  hashfun  13786  4sqlem19  16287  imasaddfnlem  16789  imasvscafn  16798  setcepi  17336  acsfiindd  17775  sylow2blem3  18676  sylow3lem6  18686  efgval2  18779  iscyggen2  18929  iscyg3  18934  issubdrg  19489  isdomn2  20000  ishil2  20791  rintopn  21445  isbasis2g  21484  tgval2  21492  eltg2b  21495  tgss2  21523  basgen2  21525  bastop1  21529  intcld  21576  unicld  21582  isclo  21623  isclo2  21624  neips  21649  opnnei  21656  neiptopnei  21668  isperf3  21689  ssidcn  21791  ist1-3  21885  cmpcov2  21926  cmpsub  21936  2ndcdisj2  21993  txkgen  22188  xkoinjcn  22223  tgqtop  22248  flimopn  22511  flfnei  22527  tmdcn2  22625  qustgplem  22656  cfil3i  23799  cmetcaulem  23818  ovolfioo  23995  ovolficc  23996  ovolicc2lem4  24048  opnmblALT  24131  xrlimcnp  25473  uvtxnbgrss  27101  iscplgr  27124  vdiscusgrb  27239  ubthlem1  28574  prmidl2  30877  hasheuni  31243  dmvlsiga  31287  ispisys2  31311  omssubadd  31457  eulerpartlemr  31531  eulerpartlemn  31538  cvmlift2lem1  32446  cvmlift2lem12  32458  mclsax  32713  setinds  32920  tfisg  32952  frpoinsg  32978  frinsg  32984  isfne4  33585  isfne2  33587  isfne3  33588  neibastop2lem  33605  filnetlem4  33626  fvineqsneq  34575  fin2so  34760  poimirlem24  34797  poimirlem27  34800  nninfnub  34907  unichnidl  35190  ispridl2  35197  n0elqs  35464  pmapglb  36786  hdmapoc  38947  isnacs2  39181  setindtrs  39500  dford3lem2  39502  dford3  39503  ntrneicls00  40317  ntrneixb  40323  ntrneik3  40324  ntrneix3  40325  ntrneik13  40326  ntrneix13  40327  pwssfi  41184  ssdf  41216  ballss3  41236  iunincfi  41237  restuni3  41261  disjf1o  41328  mapss2  41344  difmap  41346  unirnmap  41347  inmap  41348  difmapsn  41351  uzfissfz  41470  iuneqfzuzlem  41478  ssuzfz  41493  iccdificc  41691  iooiinicc  41694  ressiocsup  41706  ressioosup  41707  iooiinioc  41708  ressiooinf  41709  fsumiunss  41732  limciccioolb  41778  limcicciooub  41794  limcresiooub  41799  limsupresxr  41923  liminfresxr  41924  icccncfext  42046  dmvolss  42147  stoweidlem31  42193  stoweidlem39  42201  fourierdlem8  42277  fourierdlem27  42296  fourierdlem38  42307  fourierdlem40  42309  fourierdlem41  42310  fourierdlem46  42314  fourierdlem48  42316  fourierdlem49  42317  fourierdlem51  42319  fourierdlem53  42321  fourierdlem64  42332  fourierdlem70  42338  fourierdlem71  42339  fourierdlem76  42344  fourierdlem78  42346  fourierdlem79  42347  fourierdlem80  42348  fourierdlem93  42361  fourierdlem97  42365  fourierdlem103  42371  fourierdlem104  42372  salexct  42494  salgencntex  42503  gsumge0cl  42530  sge0fodjrnlem  42575  sge0reuz  42606  iundjiun  42619  icoresmbl  42702  hoicvr  42707  hoidmv1le  42753  hoidmvlelem1  42754  hoidmvlelem3  42756  hoiqssbllem2  42782  hspmbllem2  42786  opnvonmbllem2  42792  iinhoiicc  42833  smfpimbor1lem2  42951  setrec1lem2  44719  setrec1lem3  44720
  Copyright terms: Public domain W3C validator