Theorem dfss3 3938

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 3934	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		df-ral 3046	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
3	1, 2	bitr4i 278	1 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵)

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538   ∈ wcel 2109  ∀wral 3045   ⊆ wss 3917

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 3046  df-ss 3934

This theorem is referenced by:  ssrab  4039  dfss5  4241  elpwunsn  4651  eqsn  4796  uni0b  4900  uni0c  4901  ssint  4931  ssiinf  5021  sspwuni  5067  dftr3  5223  wefrc  5635  rninxp  6155  frpoinsg  6319  ordunisssuc  6443  fnres  6648  eqfnfv3  7008  funimass3  7029  ffvresb  7100  tfisg  7833  tfis  7834  smogt  8339  cofonr  8641  naddrid  8650  pwssfi  9147  unifi  9302  unifi2  9303  fissuni  9315  fipreima  9316  cantnf  9653  frinsg  9711  tz9.12lem3  9749  r1elss  9766  rankval3b  9786  rankonidlem  9788  bndrank  9801  iscard  9935  cfub  10209  cflm  10210  fin1a2s  10374  dcomex  10407  ttukeylem6  10474  unirnfdomd  10527  alephreg  10542  tskord  10740  gruuni  10760  intgru  10774  grudomon  10777  axgroth3  10791  suplem1pr  11012  supexpr  11014  supsr  11072  hashfun  14409  4sqlem19  16941  imasaddfnlem  17498  imasvscafn  17507  setcepi  18057  acsfiindd  18519  sylow2blem3  19559  sylow3lem6  19569  efgval2  19661  iscyggen2  19818  iscyg3  19823  isdomn2  20627  isdomn2OLD  20628  issubdrg  20696  ishil2  21635  rintopn  22803  isbasis2g  22842  tgval2  22850  eltg2b  22853  tgss2  22881  basgen2  22883  bastop1  22887  intcld  22934  unicld  22940  isclo  22981  isclo2  22982  neips  23007  opnnei  23014  neiptopnei  23026  isperf3  23047  ssidcn  23149  ist1-3  23243  cmpcov2  23284  cmpsub  23294  2ndcdisj2  23351  txkgen  23546  xkoinjcn  23581  tgqtop  23606  flimopn  23869  flfnei  23885  tmdcn2  23983  qustgplem  24015  cfil3i  25176  cmetcaulem  25195  ovolfioo  25375  ovolficc  25376  ovolicc2lem4  25428  opnmblALT  25511  xrlimcnp  26885  madebdayim  27806  uvtxnbgrss  29326  iscplgr  29349  vdiscusgrb  29465  ubthlem1  30806  isdrng4  33252  prmidl2  33419  hasheuni  34082  dmvlsiga  34126  ispisys2  34150  omssubadd  34298  eulerpartlemr  34372  eulerpartlemn  34379  cvmlift2lem1  35296  cvmlift2lem12  35308  mclsax  35563  setinds  35773  isfne4  36335  isfne2  36337  isfne3  36338  neibastop2lem  36355  filnetlem4  36376  fvineqsneq  37407  fin2so  37608  poimirlem24  37645  poimirlem27  37648  nninfnub  37752  unichnidl  38032  ispridl2  38039  n0elqs  38321  pmapglb  39771  hdmapoc  41932  isnacs2  42701  setindtrs  43021  dford3lem2  43023  dford3  43024  ssunib  43216  ntrneicls00  44085  ntrneixb  44091  ntrneik3  44092  ntrneix3  44093  ntrneik13  44094  ntrneix13  44095  trfr  44959  ssabso  44971  ssdf  45076  ballss3  45094  iunincfi  45095  restuni3  45119  disjf1o  45192  mapss2  45206  difmap  45208  unirnmap  45209  inmap  45210  difmapsn  45213  uzfissfz  45329  iuneqfzuzlem  45337  ssuzfz  45352  iccdificc  45544  iooiinicc  45547  ressiocsup  45559  ressioosup  45560  iooiinioc  45561  ressiooinf  45562  fsumiunss  45580  limciccioolb  45626  limcicciooub  45642  limcresiooub  45647  limsupresxr  45771  liminfresxr  45772  icccncfext  45892  dmvolss  45990  stoweidlem31  46036  stoweidlem39  46044  fourierdlem8  46120  fourierdlem27  46139  fourierdlem38  46150  fourierdlem40  46152  fourierdlem41  46153  fourierdlem46  46157  fourierdlem48  46159  fourierdlem49  46160  fourierdlem51  46162  fourierdlem64  46175  fourierdlem70  46181  fourierdlem71  46182  fourierdlem76  46187  fourierdlem78  46189  fourierdlem79  46190  fourierdlem80  46191  fourierdlem93  46204  fourierdlem97  46208  fourierdlem103  46214  fourierdlem104  46215  salexct  46339  salgencntex  46348  gsumge0cl  46376  sge0fodjrnlem  46421  sge0reuz  46452  iundjiun  46465  icoresmbl  46548  hoicvr  46553  hoidmv1le  46599  hoidmvlelem1  46600  hoidmvlelem3  46602  hoiqssbllem2  46628  hspmbllem2  46632  opnvonmbllem2  46638  iinhoiicc  46679  smfpimbor1lem2  46804  isclatd  48975  setrec1lem2  49681  setrec1lem3  49682