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

Theorem dfss3 3557
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 3556 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
2 df-ral 2900 . 2 (∀𝑥𝐴 𝑥𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
31, 2bitr4i 265 1 (𝐴𝐵 ↔ ∀𝑥𝐴 𝑥𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wal 1472  wcel 1976  wral 2895  wss 3539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-ral 2900  df-in 3546  df-ss 3553
This theorem is referenced by:  ssrab  3642  elpwunsn  4170  eqsn  4298  eqsnOLD  4299  uni0b  4393  uni0c  4394  ssint  4422  ssiinf  4499  sspwuni  4541  dftr3  4678  wefrc  5022  rninxp  5478  wfisg  5618  ordunisssuc  5733  fnres  5907  eqfnfv3  6206  funimass3  6226  ffvresb  6286  tfis  6923  smogt  7328  unifi  8115  unifi2  8116  fissuni  8131  fipreima  8132  cantnf  8450  tz9.12lem3  8512  r1elss  8529  rankval3b  8549  rankonidlem  8551  bndrank  8564  iscard  8661  cfub  8931  cflm  8932  fin1a2s  9096  dcomex  9129  ttukeylem6  9196  unirnfdomd  9245  alephreg  9260  tskord  9458  gruuni  9478  intgru  9492  grudomon  9495  axgroth3  9509  suplem1pr  9730  supexpr  9732  supsr  9789  hashfun  13036  4sqlem19  15451  imasaddfnlem  15957  imasvscafn  15966  setcepi  16507  acsfiindd  16946  sylow2blem3  17806  sylow3lem6  17816  efgval2  17906  iscyggen2  18052  iscyg3  18057  issubdrg  18574  isdomn2  19066  ishil2  19824  rintopn  20481  isbasis2g  20505  tgval2  20513  eltg2b  20516  tgss2  20544  basgen2  20546  bastop1  20550  intcld  20596  unicld  20602  isclo  20643  isclo2  20644  neips  20669  opnnei  20676  neiptopnei  20688  isperf3  20709  ssidcn  20811  ist1-3  20905  cmpcov2  20945  cmpsub  20955  2ndcdisj2  21012  txkgen  21207  xkoinjcn  21242  tgqtop  21267  flimopn  21531  flfnei  21547  tmdcn2  21645  qustgplem  21676  cfil3i  22793  cmetcaulem  22812  ovolfioo  22960  ovolficc  22961  ovolicc2lem4  23012  opnmblALT  23094  xrlimcnp  24412  ubthlem1  26916  hasheuni  29280  dmvlsiga  29325  ispisys2  29349  omssubadd  29495  eulerpartlemr  29569  eulerpartlemn  29576  cvmlift2lem1  30344  cvmlift2lem12  30356  mclsax  30526  setinds  30733  tfisg  30766  frinsg  30792  isfne4  31311  isfne2  31313  isfne3  31314  neibastop2lem  31331  filnetlem4  31352  fin2so  32362  poimirlem24  32399  poimirlem27  32402  nninfnub  32513  unichnidl  32796  ispridl2  32803  pmapglb  33870  hdmapoc  36037  isnacs2  36083  setindtrs  36406  dford3lem2  36408  dford3  36409  ntrneicls00  37203  ntrneixb  37209  ntrneik3  37210  ntrneix3  37211  ntrneik13  37212  ntrneix13  37213  pwssfi  38032  ssdf  38069  ballss3  38094  iunincfi  38096  restuni3  38129  disjf1o  38169  mapss2  38188  difmap  38190  unirnmap  38191  inmap  38192  difmapsn  38195  unirnmapsn  38197  iunmapsn  38200  uzfissfz  38280  iuneqfzuzlem  38288  ssuzfz  38303  iccdificc  38410  iooiinicc  38413  ressiocsup  38425  ressioosup  38426  iooiinioc  38427  ressiooinf  38428  fsumiunss  38439  limciccioolb  38485  limcicciooub  38501  limcresiooub  38506  icccncfext  38570  dmvolss  38675  stoweidlem31  38721  stoweidlem39  38729  fourierdlem8  38805  fourierdlem27  38824  fourierdlem38  38835  fourierdlem40  38837  fourierdlem41  38838  fourierdlem46  38842  fourierdlem48  38844  fourierdlem49  38845  fourierdlem51  38847  fourierdlem53  38849  fourierdlem64  38860  fourierdlem70  38866  fourierdlem71  38867  fourierdlem76  38872  fourierdlem78  38874  fourierdlem79  38875  fourierdlem80  38876  fourierdlem93  38889  fourierdlem97  38893  fourierdlem103  38899  fourierdlem104  38900  rrxbasefi  38976  qndenserrn  38992  intsaluni  39020  salexct  39025  salgencntex  39034  gsumge0cl  39061  sge0fodjrnlem  39106  sge0reuz  39137  iundjiun  39150  meadjiunlem  39155  icoresmbl  39230  hoicvr  39235  hoidmv1le  39281  hoidmvlelem1  39282  hoidmvlelem3  39284  hoiqssbllem2  39310  hspmbllem2  39314  opnvonmbllem2  39320  iinhoiicc  39362  iunhoiioo  39364  smfpimbor1lem2  39481  dfss7  40102  uvtxanbgr  40613  nbupgruvtxres  40629  cplgruvtxb  40632  vdiscusgrb  40741
  Copyright terms: Public domain W3C validator