Theorem dfss3 3927

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568   ∈ wcel 2146  ∀wral 3081   ⊆ wss 3906

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ral 3082  df-ss 3923

This theorem is used by:  ssrab  4026  dfss5  4228  elpwunsn  4652  eqsn  4797  uni0b  4901  uni0c  4902  ssint  4931  ssiinf  5021  sspwuni  5068  dftr3  5225  wefrc  5657  rninxp  6179  frpoinsg  6348  ordunisssuc  6473  fnres  6666  eqfnfv3  7031  funimass3  7053  ffvresb  7125  tfisg  7852  tfis  7853  smogt  8356  cofonr  8662  naddrid  8672  pwssfi  9164  unifi  9304  unifi2  9305  fissuni  9317  fipreima  9318  cantnf  9665  setinds  9721  frinsg  9726  tz9.12lem3  9764  r1elss  9781  rankval3b  9801  rankonidlem  9803  bndrank  9816  iscard  9973  cfub  10243  cflm  10244  fin1a2s  10409  dcomex  10442  ttukeylem6  10509  unirnfdomd  10563  alephreg  10578  tskord  10776  gruuni  10796  intgru  10810  grudomon  10813  axgroth3  10827  suplem1pr  11048  supexpr  11050  supsr  11108  hashfun  14488  4sqlem19  17041  imasaddfnlem  17600  imasvscafn  17609  setcepi  18163  acsfiindd  18627  sylow2blem3  19716  sylow3lem6  19726  efgval2  19818  iscyggen2  19975  iscyg3  19980  isdomn2  20840  isdrng4  20869  issubdrg  20913  unichnlidl  21392  prmidl2  21496  ishil2  21899  rintopn  23096  isbasis2g  23135  tgval2  23143  eltg2b  23146  tgss2  23174  basgen2  23176  bastop1  23180  intcld  23227  unicld  23233  isclo  23274  isclo2  23275  neips  23300  opnnei  23307  neiptopnei  23319  isperf3  23340  ssidcn  23442  ist1-3  23536  cmpcov2  23577  cmpsub  23587  2ndcdisj2  23645  txkgen  23840  xkoinjcn  23875  tgqtop  23900  flimopn  24163  flfnei  24179  tmdcn2  24277  qustgplem  24309  cfil3i  25459  cmetcaulem  25478  ovolfioo  25657  ovolficc  25658  ovolicc2lem4  25710  opnmblALT  25793  xrlimcnp  27164  madebdayim  28112  oldfib  28601  uvtxnbgrss  29776  iscplgr  29799  vdiscusgrb  29914  ubthlem1  31269  hasheuni  34515  dmvlsiga  34559  ispisys2  34584  omssubadd  34731  eulerpartlemr  34805  eulerpartlemn  34812  cvmlift2lem1  35807  cvmlift2lem12  35819  mclsax  36074  nmulrid  36702  isfne4  36884  isfne2  36886  isfne3  36887  neibastop2lem  36904  filnetlem4  36925  fvineqsneq  38091  fin2so  38291  poimirlem24  38328  poimirlem27  38331  nninfnub  38435  unichnidl  38715  ispridl2  38722  n0elqs  39014  ssdmral  39061  pmapglb  40577  hdmapoc  42738  isnacs2  43470  setindtrs  43785  dford3lem2  43787  dford3  43788  ssunib  43980  ntrneicls00  44848  ntrneixb  44854  ntrneik3  44855  ntrneix3  44856  ntrneik13  44857  ntrneix13  44858  trfr  45704  ssabso  45716  ssdf  45828  ballss3  45844  iunincfi  45845  restuni3  45869  disjf1o  45942  mapss2  45955  difmap  45956  unirnmap  45957  inmap  45958  difmapsn  45961  uzfissfz  46075  iuneqfzuzlem  46083  ssuzfz  46098  iccdificc  46288  iooiinicc  46291  ressiocsup  46303  ressioosup  46304  iooiinioc  46305  ressiooinf  46306  fsumiunss  46324  limciccioolb  46370  limcicciooub  46384  limcresiooub  46389  limsupresxr  46513  liminfresxr  46514  icccncfext  46634  dmvolss  46732  stoweidlem31  46778  stoweidlem39  46786  fourierdlem8  46862  fourierdlem27  46881  fourierdlem38  46892  fourierdlem40  46894  fourierdlem41  46895  fourierdlem46  46899  fourierdlem51  46904  fourierdlem64  46917  fourierdlem70  46923  fourierdlem71  46924  fourierdlem76  46929  fourierdlem78  46931  fourierdlem79  46932  fourierdlem80  46933  fourierdlem93  46946  fourierdlem97  46950  fourierdlem103  46956  fourierdlem104  46957  salexct  47081  salgencntex  47090  gsumge0cl  47118  sge0fodjrnlem  47163  sge0reuz  47194  iundjiun  47207  icoresmbl  47290  hoidmv1le  47341  hoidmvlelem1  47342  hoidmvlelem3  47344  hoiqssbllem2  47370  hspmbllem2  47374  opnvonmbllem2  47380  iinhoiicc  47421  smfpimbor1lem2  47546  isclatd  49794  setrec1lem2  50499  setrec1lem3  50500