Theorem dfss3 3935

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

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

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 3045  df-ss 3931

This theorem is referenced by:  ssrab  4036  dfss5  4238  elpwunsn  4648  eqsn  4793  uni0b  4897  uni0c  4898  ssint  4928  ssiinf  5018  sspwuni  5064  dftr3  5220  wefrc  5632  rninxp  6152  frpoinsg  6316  ordunisssuc  6440  fnres  6645  eqfnfv3  7005  funimass3  7026  ffvresb  7097  tfisg  7830  tfis  7831  smogt  8336  cofonr  8638  naddrid  8647  pwssfi  9141  unifi  9295  unifi2  9296  fissuni  9308  fipreima  9309  cantnf  9646  frinsg  9704  tz9.12lem3  9742  r1elss  9759  rankval3b  9779  rankonidlem  9781  bndrank  9794  iscard  9928  cfub  10202  cflm  10203  fin1a2s  10367  dcomex  10400  ttukeylem6  10467  unirnfdomd  10520  alephreg  10535  tskord  10733  gruuni  10753  intgru  10767  grudomon  10770  axgroth3  10784  suplem1pr  11005  supexpr  11007  supsr  11065  hashfun  14402  4sqlem19  16934  imasaddfnlem  17491  imasvscafn  17500  setcepi  18050  acsfiindd  18512  sylow2blem3  19552  sylow3lem6  19562  efgval2  19654  iscyggen2  19811  iscyg3  19816  isdomn2  20620  isdomn2OLD  20621  issubdrg  20689  ishil2  21628  rintopn  22796  isbasis2g  22835  tgval2  22843  eltg2b  22846  tgss2  22874  basgen2  22876  bastop1  22880  intcld  22927  unicld  22933  isclo  22974  isclo2  22975  neips  23000  opnnei  23007  neiptopnei  23019  isperf3  23040  ssidcn  23142  ist1-3  23236  cmpcov2  23277  cmpsub  23287  2ndcdisj2  23344  txkgen  23539  xkoinjcn  23574  tgqtop  23599  flimopn  23862  flfnei  23878  tmdcn2  23976  qustgplem  24008  cfil3i  25169  cmetcaulem  25188  ovolfioo  25368  ovolficc  25369  ovolicc2lem4  25421  opnmblALT  25504  xrlimcnp  26878  madebdayim  27799  uvtxnbgrss  29319  iscplgr  29342  vdiscusgrb  29458  ubthlem1  30799  isdrng4  33245  prmidl2  33412  hasheuni  34075  dmvlsiga  34119  ispisys2  34143  omssubadd  34291  eulerpartlemr  34365  eulerpartlemn  34372  cvmlift2lem1  35289  cvmlift2lem12  35301  mclsax  35556  setinds  35766  isfne4  36328  isfne2  36330  isfne3  36331  neibastop2lem  36348  filnetlem4  36369  fvineqsneq  37400  fin2so  37601  poimirlem24  37638  poimirlem27  37641  nninfnub  37745  unichnidl  38025  ispridl2  38032  n0elqs  38314  pmapglb  39764  hdmapoc  41925  isnacs2  42694  setindtrs  43014  dford3lem2  43016  dford3  43017  ssunib  43209  ntrneicls00  44078  ntrneixb  44084  ntrneik3  44085  ntrneix3  44086  ntrneik13  44087  ntrneix13  44088  trfr  44952  ssabso  44964  ssdf  45069  ballss3  45087  iunincfi  45088  restuni3  45112  disjf1o  45185  mapss2  45199  difmap  45201  unirnmap  45202  inmap  45203  difmapsn  45206  uzfissfz  45322  iuneqfzuzlem  45330  ssuzfz  45345  iccdificc  45537  iooiinicc  45540  ressiocsup  45552  ressioosup  45553  iooiinioc  45554  ressiooinf  45555  fsumiunss  45573  limciccioolb  45619  limcicciooub  45635  limcresiooub  45640  limsupresxr  45764  liminfresxr  45765  icccncfext  45885  dmvolss  45983  stoweidlem31  46029  stoweidlem39  46037  fourierdlem8  46113  fourierdlem27  46132  fourierdlem38  46143  fourierdlem40  46145  fourierdlem41  46146  fourierdlem46  46150  fourierdlem48  46152  fourierdlem49  46153  fourierdlem51  46155  fourierdlem64  46168  fourierdlem70  46174  fourierdlem71  46175  fourierdlem76  46180  fourierdlem78  46182  fourierdlem79  46183  fourierdlem80  46184  fourierdlem93  46197  fourierdlem97  46201  fourierdlem103  46207  fourierdlem104  46208  salexct  46332  salgencntex  46341  gsumge0cl  46369  sge0fodjrnlem  46414  sge0reuz  46445  iundjiun  46458  icoresmbl  46541  hoicvr  46546  hoidmv1le  46592  hoidmvlelem1  46593  hoidmvlelem3  46595  hoiqssbllem2  46621  hspmbllem2  46625  opnvonmbllem2  46631  iinhoiicc  46672  smfpimbor1lem2  46797  isclatd  48971  setrec1lem2  49677  setrec1lem3  49678