Theorem dfss3 3922

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1539   ∈ wcel 2113  ∀wral 3051   ⊆ wss 3901

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 3052  df-ss 3918

This theorem is referenced by:  ssrab  4023  dfss5  4227  elpwunsn  4641  eqsn  4785  uni0b  4889  uni0c  4890  ssint  4919  ssiinf  5010  sspwuni  5055  dftr3  5210  wefrc  5618  rninxp  6137  frpoinsg  6301  ordunisssuc  6425  fnres  6619  eqfnfv3  6978  funimass3  6999  ffvresb  7070  tfisg  7796  tfis  7797  smogt  8299  cofonr  8602  naddrid  8611  pwssfi  9101  unifi  9244  unifi2  9245  fissuni  9257  fipreima  9258  cantnf  9602  setinds  9658  frinsg  9663  tz9.12lem3  9701  r1elss  9718  rankval3b  9738  rankonidlem  9740  bndrank  9753  iscard  9887  cfub  10159  cflm  10160  fin1a2s  10324  dcomex  10357  ttukeylem6  10424  unirnfdomd  10478  alephreg  10493  tskord  10691  gruuni  10711  intgru  10725  grudomon  10728  axgroth3  10742  suplem1pr  10963  supexpr  10965  supsr  11023  hashfun  14360  4sqlem19  16891  imasaddfnlem  17449  imasvscafn  17458  setcepi  18012  acsfiindd  18476  sylow2blem3  19551  sylow3lem6  19561  efgval2  19653  iscyggen2  19810  iscyg3  19815  isdomn2  20644  isdomn2OLD  20645  issubdrg  20713  ishil2  21674  rintopn  22853  isbasis2g  22892  tgval2  22900  eltg2b  22903  tgss2  22931  basgen2  22933  bastop1  22937  intcld  22984  unicld  22990  isclo  23031  isclo2  23032  neips  23057  opnnei  23064  neiptopnei  23076  isperf3  23097  ssidcn  23199  ist1-3  23293  cmpcov2  23334  cmpsub  23344  2ndcdisj2  23401  txkgen  23596  xkoinjcn  23631  tgqtop  23656  flimopn  23919  flfnei  23935  tmdcn2  24033  qustgplem  24065  cfil3i  25225  cmetcaulem  25244  ovolfioo  25424  ovolficc  25425  ovolicc2lem4  25477  opnmblALT  25560  xrlimcnp  26934  madebdayim  27884  oldfib  28373  uvtxnbgrss  29465  iscplgr  29488  vdiscusgrb  29604  ubthlem1  30945  isdrng4  33377  prmidl2  33522  hasheuni  34242  dmvlsiga  34286  ispisys2  34310  omssubadd  34457  eulerpartlemr  34531  eulerpartlemn  34538  cvmlift2lem1  35496  cvmlift2lem12  35508  mclsax  35763  isfne4  36534  isfne2  36536  isfne3  36537  neibastop2lem  36554  filnetlem4  36575  fvineqsneq  37617  fin2so  37808  poimirlem24  37845  poimirlem27  37848  nninfnub  37952  unichnidl  38232  ispridl2  38239  n0elqs  38525  ssdmral  38564  pmapglb  40030  hdmapoc  42191  isnacs2  42948  setindtrs  43267  dford3lem2  43269  dford3  43270  ssunib  43462  ntrneicls00  44330  ntrneixb  44336  ntrneik3  44337  ntrneix3  44338  ntrneik13  44339  ntrneix13  44340  trfr  45203  ssabso  45215  ssdf  45320  ballss3  45337  iunincfi  45338  restuni3  45362  disjf1o  45435  mapss2  45449  difmap  45451  unirnmap  45452  inmap  45453  difmapsn  45456  uzfissfz  45571  iuneqfzuzlem  45579  ssuzfz  45594  iccdificc  45785  iooiinicc  45788  ressiocsup  45800  ressioosup  45801  iooiinioc  45802  ressiooinf  45803  fsumiunss  45821  limciccioolb  45867  limcicciooub  45881  limcresiooub  45886  limsupresxr  46010  liminfresxr  46011  icccncfext  46131  dmvolss  46229  stoweidlem31  46275  stoweidlem39  46283  fourierdlem8  46359  fourierdlem27  46378  fourierdlem38  46389  fourierdlem40  46391  fourierdlem41  46392  fourierdlem46  46396  fourierdlem48  46398  fourierdlem49  46399  fourierdlem51  46401  fourierdlem64  46414  fourierdlem70  46420  fourierdlem71  46421  fourierdlem76  46426  fourierdlem78  46428  fourierdlem79  46429  fourierdlem80  46430  fourierdlem93  46443  fourierdlem97  46447  fourierdlem103  46453  fourierdlem104  46454  salexct  46578  salgencntex  46587  gsumge0cl  46615  sge0fodjrnlem  46660  sge0reuz  46691  iundjiun  46704  icoresmbl  46787  hoicvr  46792  hoidmv1le  46838  hoidmvlelem1  46839  hoidmvlelem3  46841  hoiqssbllem2  46867  hspmbllem2  46871  opnvonmbllem2  46877  iinhoiicc  46918  smfpimbor1lem2  47043  isclatd  49228  setrec1lem2  49933  setrec1lem3  49934