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

Theorem dfss3 3625
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 3624 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
2 df-ral 2946 . 2 (∀𝑥𝐴 𝑥𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
31, 2bitr4i 267 1 (𝐴𝐵 ↔ ∀𝑥𝐴 𝑥𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wal 1521  wcel 2030  wral 2941  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-ral 2946  df-in 3614  df-ss 3621
This theorem is referenced by:  ssrab  3713  dfss5  3897  elpwunsn  4256  ssdifsn  4351  eqsn  4393  eqsnOLD  4394  uni0b  4495  uni0c  4496  ssint  4525  ssiinf  4601  sspwuni  4643  dftr3  4789  wefrc  5137  rninxp  5608  wfisg  5753  ordunisssuc  5868  fnres  6045  eqfnfv3  6353  funimass3  6373  ffvresb  6434  tfis  7096  smogt  7509  unifi  8296  unifi2  8297  fissuni  8312  fipreima  8313  cantnf  8628  tz9.12lem3  8690  r1elss  8707  rankval3b  8727  rankonidlem  8729  bndrank  8742  iscard  8839  cfub  9109  cflm  9110  fin1a2s  9274  dcomex  9307  ttukeylem6  9374  unirnfdomd  9427  alephreg  9442  tskord  9640  gruuni  9660  intgru  9674  grudomon  9677  axgroth3  9691  suplem1pr  9912  supexpr  9914  supsr  9971  hashfun  13262  4sqlem19  15714  imasaddfnlem  16235  imasvscafn  16244  setcepi  16785  acsfiindd  17224  sylow2blem3  18083  sylow3lem6  18093  efgval2  18183  iscyggen2  18329  iscyg3  18334  issubdrg  18853  isdomn2  19347  ishil2  20111  rintopn  20762  isbasis2g  20800  tgval2  20808  eltg2b  20811  tgss2  20839  basgen2  20841  bastop1  20845  intcld  20892  unicld  20898  isclo  20939  isclo2  20940  neips  20965  opnnei  20972  neiptopnei  20984  isperf3  21005  ssidcn  21107  ist1-3  21201  cmpcov2  21241  cmpsub  21251  2ndcdisj2  21308  txkgen  21503  xkoinjcn  21538  tgqtop  21563  flimopn  21826  flfnei  21842  tmdcn2  21940  qustgplem  21971  cfil3i  23113  cmetcaulem  23132  ovolfioo  23282  ovolficc  23283  ovolicc2lem4  23334  opnmblALT  23417  xrlimcnp  24740  uvtxnbgrss  26340  nbupgruvtxres  26358  iscplgr  26366  cplgruvtxbOLD  26367  vdiscusgrb  26482  ubthlem1  27854  hasheuni  30275  dmvlsiga  30320  ispisys2  30344  omssubadd  30490  eulerpartlemr  30564  eulerpartlemn  30571  cvmlift2lem1  31410  cvmlift2lem12  31422  mclsax  31592  setinds  31807  tfisg  31840  frpoinsg  31866  frinsg  31870  isfne4  32460  isfne2  32462  isfne3  32463  neibastop2lem  32480  filnetlem4  32501  fin2so  33526  poimirlem24  33563  poimirlem27  33566  nninfnub  33677  unichnidl  33960  ispridl2  33967  n0elqs  34239  pmapglb  35374  hdmapoc  37540  isnacs2  37586  setindtrs  37909  dford3lem2  37911  dford3  37912  ntrneicls00  38704  ntrneixb  38710  ntrneik3  38711  ntrneix3  38712  ntrneik13  38713  ntrneix13  38714  pwssfi  39525  ssdf  39561  ballss3  39584  iunincfi  39586  restuni3  39615  iinssiin  39626  disjf1o  39692  mapss2  39711  difmap  39713  unirnmap  39714  inmap  39715  difmapsn  39718  unirnmapsn  39720  iunmapsn  39723  uzfissfz  39855  iuneqfzuzlem  39863  ssuzfz  39878  iccdificc  40084  iooiinicc  40087  ressiocsup  40099  ressioosup  40100  iooiinioc  40101  ressiooinf  40102  fsumiunss  40125  limciccioolb  40171  limcicciooub  40187  limcresiooub  40192  limsupresxr  40316  liminfresxr  40317  icccncfext  40418  dmvolss  40520  stoweidlem31  40566  stoweidlem39  40574  fourierdlem8  40650  fourierdlem27  40669  fourierdlem38  40680  fourierdlem40  40682  fourierdlem41  40683  fourierdlem46  40687  fourierdlem48  40689  fourierdlem49  40690  fourierdlem51  40692  fourierdlem53  40694  fourierdlem64  40705  fourierdlem70  40711  fourierdlem71  40712  fourierdlem76  40717  fourierdlem78  40719  fourierdlem79  40720  fourierdlem80  40721  fourierdlem93  40734  fourierdlem97  40738  fourierdlem103  40744  fourierdlem104  40745  rrxbasefi  40821  qndenserrn  40837  intsaluni  40865  salexct  40870  salgencntex  40879  gsumge0cl  40906  sge0fodjrnlem  40951  sge0reuz  40982  iundjiun  40995  meadjiunlem  41000  icoresmbl  41078  hoicvr  41083  hoidmv1le  41129  hoidmvlelem1  41130  hoidmvlelem3  41132  hoiqssbllem2  41158  hspmbllem2  41162  opnvonmbllem2  41168  iinhoiicc  41209  iunhoiioo  41211  smfpimbor1lem2  41327  setrec1lem2  42760  setrec1lem3  42761
  Copyright terms: Public domain W3C validator