Theorem dfss3 3997

Description: Alternate definition of subclass relationship. (Contributed by NM, 14-Oct-1999.)

Assertion

Ref	Expression
dfss3	⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem dfss3

Step	Hyp	Ref	Expression
1		df-ss 3993	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		df-ral 3068	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
3	1, 2	bitr4i 278	1 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵)

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1535   ∈ wcel 2108  ∀wral 3067   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-ral 3068  df-ss 3993

This theorem is referenced by:  ssrab  4096  dfss5  4294  elpwunsn  4707  eqsn  4854  uni0b  4957  uni0c  4958  ssint  4988  ssiinf  5077  sspwuni  5123  dftr3  5289  wefrc  5694  rninxp  6210  frpoinsg  6375  wfisgOLD  6386  ordunisssuc  6501  fnres  6707  eqfnfv3  7066  funimass3  7087  ffvresb  7159  tfisg  7891  tfis  7892  smogt  8423  cofonr  8730  naddrid  8739  unifi  9412  unifi2  9413  fissuni  9427  fipreima  9428  cantnf  9762  frinsg  9820  tz9.12lem3  9858  r1elss  9875  rankval3b  9895  rankonidlem  9897  bndrank  9910  iscard  10044  cfub  10318  cflm  10319  fin1a2s  10483  dcomex  10516  ttukeylem6  10583  unirnfdomd  10636  alephreg  10651  tskord  10849  gruuni  10869  intgru  10883  grudomon  10886  axgroth3  10900  suplem1pr  11121  supexpr  11123  supsr  11181  hashfun  14486  4sqlem19  17010  imasaddfnlem  17588  imasvscafn  17597  setcepi  18155  acsfiindd  18623  sylow2blem3  19664  sylow3lem6  19674  efgval2  19766  iscyggen2  19923  iscyg3  19928  isdomn2  20733  isdomn2OLD  20734  issubdrg  20803  ishil2  21762  rintopn  22936  isbasis2g  22976  tgval2  22984  eltg2b  22987  tgss2  23015  basgen2  23017  bastop1  23021  intcld  23069  unicld  23075  isclo  23116  isclo2  23117  neips  23142  opnnei  23149  neiptopnei  23161  isperf3  23182  ssidcn  23284  ist1-3  23378  cmpcov2  23419  cmpsub  23429  2ndcdisj2  23486  txkgen  23681  xkoinjcn  23716  tgqtop  23741  flimopn  24004  flfnei  24020  tmdcn2  24118  qustgplem  24150  cfil3i  25322  cmetcaulem  25341  ovolfioo  25521  ovolficc  25522  ovolicc2lem4  25574  opnmblALT  25657  xrlimcnp  27029  madebdayim  27944  uvtxnbgrss  29427  iscplgr  29450  vdiscusgrb  29566  ubthlem1  30902  isdrng4  33264  prmidl2  33434  hasheuni  34049  dmvlsiga  34093  ispisys2  34117  omssubadd  34265  eulerpartlemr  34339  eulerpartlemn  34346  cvmlift2lem1  35270  cvmlift2lem12  35282  mclsax  35537  setinds  35742  isfne4  36306  isfne2  36308  isfne3  36309  neibastop2lem  36326  filnetlem4  36347  fvineqsneq  37378  fin2so  37567  poimirlem24  37604  poimirlem27  37607  nninfnub  37711  unichnidl  37991  ispridl2  37998  n0elqs  38282  pmapglb  39727  hdmapoc  41888  isnacs2  42662  setindtrs  42982  dford3lem2  42984  dford3  42985  ssunib  43181  ntrneicls00  44051  ntrneixb  44057  ntrneik3  44058  ntrneix3  44059  ntrneik13  44060  ntrneix13  44061  pwssfi  44947  ssdf  44977  ballss3  44995  iunincfi  44996  restuni3  45020  disjf1o  45098  mapss2  45112  difmap  45114  unirnmap  45115  inmap  45116  difmapsn  45119  uzfissfz  45241  iuneqfzuzlem  45249  ssuzfz  45264  iccdificc  45457  iooiinicc  45460  ressiocsup  45472  ressioosup  45473  iooiinioc  45474  ressiooinf  45475  fsumiunss  45496  limciccioolb  45542  limcicciooub  45558  limcresiooub  45563  limsupresxr  45687  liminfresxr  45688  icccncfext  45808  dmvolss  45906  stoweidlem31  45952  stoweidlem39  45960  fourierdlem8  46036  fourierdlem27  46055  fourierdlem38  46066  fourierdlem40  46068  fourierdlem41  46069  fourierdlem46  46073  fourierdlem48  46075  fourierdlem49  46076  fourierdlem51  46078  fourierdlem64  46091  fourierdlem70  46097  fourierdlem71  46098  fourierdlem76  46103  fourierdlem78  46105  fourierdlem79  46106  fourierdlem80  46107  fourierdlem93  46120  fourierdlem97  46124  fourierdlem103  46130  fourierdlem104  46131  salexct  46255  salgencntex  46264  gsumge0cl  46292  sge0fodjrnlem  46337  sge0reuz  46368  iundjiun  46381  icoresmbl  46464  hoicvr  46469  hoidmv1le  46515  hoidmvlelem1  46516  hoidmvlelem3  46518  hoiqssbllem2  46544  hspmbllem2  46548  opnvonmbllem2  46554  iinhoiicc  46595  smfpimbor1lem2  46720  isclatd  48655  setrec1lem2  48780  setrec1lem3  48781