Theorem dfss3 3934

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

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1565   ∈ wcel 2149  ∀wral 3085   ⊆ wss 3913

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 210  df-ral 3086  df-ss 3930

This theorem is referenced by:  ssrab  4033  dfss5  4236  elpwunsn  4652  eqsn  4796  uni0b  4900  uni0c  4901  ssint  4930  ssiinf  5020  sspwuni  5067  dftr3  5224  wefrc  5653  rninxp  6175  frpoinsg  6342  ordunisssuc  6467  fnres  6660  eqfnfv3  7025  funimass3  7047  ffvresb  7119  tfisg  7846  tfis  7847  smogt  8350  cofonr  8656  naddrid  8666  pwssfi  9157  unifi  9297  unifi2  9298  fissuni  9310  fipreima  9311  cantnf  9658  setinds  9714  frinsg  9719  tz9.12lem3  9757  r1elss  9774  rankval3b  9794  rankonidlem  9796  bndrank  9809  iscard  9957  cfub  10228  cflm  10229  fin1a2s  10394  dcomex  10427  ttukeylem6  10494  unirnfdomd  10548  alephreg  10563  tskord  10761  gruuni  10781  intgru  10795  grudomon  10798  axgroth3  10812  suplem1pr  11033  supexpr  11035  supsr  11093  hashfun  14470  4sqlem19  17019  imasaddfnlem  17578  imasvscafn  17587  setcepi  18141  acsfiindd  18605  sylow2blem3  19688  sylow3lem6  19698  efgval2  19790  iscyggen2  19947  iscyg3  19952  isdomn2  20792  issubdrg  20857  unichnlidl  21336  prmidl2  21433  ishil2  21834  rintopn  23031  isbasis2g  23070  tgval2  23078  eltg2b  23081  tgss2  23109  basgen2  23111  bastop1  23115  intcld  23162  unicld  23168  isclo  23209  isclo2  23210  neips  23235  opnnei  23242  neiptopnei  23254  isperf3  23275  ssidcn  23377  ist1-3  23471  cmpcov2  23512  cmpsub  23522  2ndcdisj2  23579  txkgen  23774  xkoinjcn  23809  tgqtop  23834  flimopn  24097  flfnei  24113  tmdcn2  24211  qustgplem  24243  cfil3i  25393  cmetcaulem  25412  ovolfioo  25591  ovolficc  25592  ovolicc2lem4  25644  opnmblALT  25727  xrlimcnp  27095  madebdayim  28043  oldfib  28532  uvtxnbgrss  29679  iscplgr  29702  vdiscusgrb  29817  ubthlem1  31159  isdrng4  33555  hasheuni  34416  dmvlsiga  34460  ispisys2  34484  omssubadd  34631  eulerpartlemr  34705  eulerpartlemn  34712  cvmlift2lem1  35689  cvmlift2lem12  35701  mclsax  35956  isfne4  36736  isfne2  36738  isfne3  36739  neibastop2lem  36756  filnetlem4  36777  fvineqsneq  37941  fin2so  38141  poimirlem24  38178  poimirlem27  38181  nninfnub  38285  unichnidl  38565  ispridl2  38572  n0elqs  38866  ssdmral  38913  pmapglb  40429  hdmapoc  42590  isnacs2  43324  setindtrs  43639  dford3lem2  43641  dford3  43642  ssunib  43834  ntrneicls00  44702  ntrneixb  44708  ntrneik3  44709  ntrneix3  44710  ntrneik13  44711  ntrneix13  44712  trfr  45558  ssabso  45570  ssdf  45682  ballss3  45698  iunincfi  45699  restuni3  45723  disjf1o  45796  mapss2  45809  difmap  45810  unirnmap  45811  inmap  45812  difmapsn  45815  uzfissfz  45929  iuneqfzuzlem  45937  ssuzfz  45952  iccdificc  46142  iooiinicc  46145  ressiocsup  46157  ressioosup  46158  iooiinioc  46159  ressiooinf  46160  fsumiunss  46178  limciccioolb  46224  limcicciooub  46238  limcresiooub  46243  limsupresxr  46367  liminfresxr  46368  icccncfext  46488  dmvolss  46586  stoweidlem31  46632  stoweidlem39  46640  fourierdlem8  46716  fourierdlem27  46735  fourierdlem38  46746  fourierdlem40  46748  fourierdlem41  46749  fourierdlem46  46753  fourierdlem51  46758  fourierdlem64  46771  fourierdlem70  46777  fourierdlem71  46778  fourierdlem76  46783  fourierdlem78  46785  fourierdlem79  46786  fourierdlem80  46787  fourierdlem93  46800  fourierdlem97  46804  fourierdlem103  46810  fourierdlem104  46811  salexct  46935  salgencntex  46944  gsumge0cl  46972  sge0fodjrnlem  47017  sge0reuz  47048  iundjiun  47061  icoresmbl  47144  hoidmv1le  47195  hoidmvlelem1  47196  hoidmvlelem3  47198  hoiqssbllem2  47224  hspmbllem2  47228  opnvonmbllem2  47234  iinhoiicc  47275  smfpimbor1lem2  47400  isclatd  49641  setrec1lem2  50346  setrec1lem3  50347