Theorem dfss3 3972

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538   ∈ wcel 2108  ∀wral 3061   ⊆ wss 3951

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 3062  df-ss 3968

This theorem is referenced by:  ssrab  4073  dfss5  4275  elpwunsn  4684  eqsn  4829  uni0b  4933  uni0c  4934  ssint  4964  ssiinf  5054  sspwuni  5100  dftr3  5265  wefrc  5679  rninxp  6199  frpoinsg  6364  wfisgOLD  6375  ordunisssuc  6490  fnres  6695  eqfnfv3  7053  funimass3  7074  ffvresb  7145  tfisg  7875  tfis  7876  smogt  8407  cofonr  8712  naddrid  8721  pwssfi  9217  unifi  9384  unifi2  9385  fissuni  9397  fipreima  9398  cantnf  9733  frinsg  9791  tz9.12lem3  9829  r1elss  9846  rankval3b  9866  rankonidlem  9868  bndrank  9881  iscard  10015  cfub  10289  cflm  10290  fin1a2s  10454  dcomex  10487  ttukeylem6  10554  unirnfdomd  10607  alephreg  10622  tskord  10820  gruuni  10840  intgru  10854  grudomon  10857  axgroth3  10871  suplem1pr  11092  supexpr  11094  supsr  11152  hashfun  14476  4sqlem19  17001  imasaddfnlem  17573  imasvscafn  17582  setcepi  18133  acsfiindd  18598  sylow2blem3  19640  sylow3lem6  19650  efgval2  19742  iscyggen2  19899  iscyg3  19904  isdomn2  20711  isdomn2OLD  20712  issubdrg  20781  ishil2  21739  rintopn  22915  isbasis2g  22955  tgval2  22963  eltg2b  22966  tgss2  22994  basgen2  22996  bastop1  23000  intcld  23048  unicld  23054  isclo  23095  isclo2  23096  neips  23121  opnnei  23128  neiptopnei  23140  isperf3  23161  ssidcn  23263  ist1-3  23357  cmpcov2  23398  cmpsub  23408  2ndcdisj2  23465  txkgen  23660  xkoinjcn  23695  tgqtop  23720  flimopn  23983  flfnei  23999  tmdcn2  24097  qustgplem  24129  cfil3i  25303  cmetcaulem  25322  ovolfioo  25502  ovolficc  25503  ovolicc2lem4  25555  opnmblALT  25638  xrlimcnp  27011  madebdayim  27926  uvtxnbgrss  29409  iscplgr  29432  vdiscusgrb  29548  ubthlem1  30889  isdrng4  33298  prmidl2  33469  hasheuni  34086  dmvlsiga  34130  ispisys2  34154  omssubadd  34302  eulerpartlemr  34376  eulerpartlemn  34383  cvmlift2lem1  35307  cvmlift2lem12  35319  mclsax  35574  setinds  35779  isfne4  36341  isfne2  36343  isfne3  36344  neibastop2lem  36361  filnetlem4  36382  fvineqsneq  37413  fin2so  37614  poimirlem24  37651  poimirlem27  37654  nninfnub  37758  unichnidl  38038  ispridl2  38045  n0elqs  38327  pmapglb  39772  hdmapoc  41933  isnacs2  42717  setindtrs  43037  dford3lem2  43039  dford3  43040  ssunib  43232  ntrneicls00  44102  ntrneixb  44108  ntrneik3  44109  ntrneix3  44110  ntrneik13  44111  ntrneix13  44112  trfr  44979  ssabso  44991  ssdf  45080  ballss3  45098  iunincfi  45099  restuni3  45123  disjf1o  45196  mapss2  45210  difmap  45212  unirnmap  45213  inmap  45214  difmapsn  45217  uzfissfz  45337  iuneqfzuzlem  45345  ssuzfz  45360  iccdificc  45552  iooiinicc  45555  ressiocsup  45567  ressioosup  45568  iooiinioc  45569  ressiooinf  45570  fsumiunss  45590  limciccioolb  45636  limcicciooub  45652  limcresiooub  45657  limsupresxr  45781  liminfresxr  45782  icccncfext  45902  dmvolss  46000  stoweidlem31  46046  stoweidlem39  46054  fourierdlem8  46130  fourierdlem27  46149  fourierdlem38  46160  fourierdlem40  46162  fourierdlem41  46163  fourierdlem46  46167  fourierdlem48  46169  fourierdlem49  46170  fourierdlem51  46172  fourierdlem64  46185  fourierdlem70  46191  fourierdlem71  46192  fourierdlem76  46197  fourierdlem78  46199  fourierdlem79  46200  fourierdlem80  46201  fourierdlem93  46214  fourierdlem97  46218  fourierdlem103  46224  fourierdlem104  46225  salexct  46349  salgencntex  46358  gsumge0cl  46386  sge0fodjrnlem  46431  sge0reuz  46462  iundjiun  46475  icoresmbl  46558  hoicvr  46563  hoidmv1le  46609  hoidmvlelem1  46610  hoidmvlelem3  46612  hoiqssbllem2  46638  hspmbllem2  46642  opnvonmbllem2  46648  iinhoiicc  46689  smfpimbor1lem2  46814  isclatd  48872  setrec1lem2  49207  setrec1lem3  49208