Theorem dfss3 3970

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1539   ∈ wcel 2106  ∀wral 3061   ⊆ wss 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-v 3476  df-in 3955  df-ss 3965

This theorem is referenced by:  ssrab  4070  dfss5  4264  elpwunsn  4687  eqsn  4832  uni0b  4937  uni0c  4938  ssint  4968  ssiinf  5057  sspwuni  5103  dftr3  5271  wefrc  5670  rninxp  6178  frpoinsg  6344  wfisgOLD  6355  ordunisssuc  6470  fnres  6677  eqfnfv3  7034  funimass3  7055  ffvresb  7126  tfisg  7845  tfis  7846  smogt  8369  cofonr  8675  naddrid  8684  unifi  9343  unifi2  9344  fissuni  9359  fipreima  9360  cantnf  9690  frinsg  9748  tz9.12lem3  9786  r1elss  9803  rankval3b  9823  rankonidlem  9825  bndrank  9838  iscard  9972  cfub  10246  cflm  10247  fin1a2s  10411  dcomex  10444  ttukeylem6  10511  unirnfdomd  10564  alephreg  10579  tskord  10777  gruuni  10797  intgru  10811  grudomon  10814  axgroth3  10828  suplem1pr  11049  supexpr  11051  supsr  11109  hashfun  14401  4sqlem19  16900  imasaddfnlem  17478  imasvscafn  17487  setcepi  18042  acsfiindd  18510  sylow2blem3  19531  sylow3lem6  19541  efgval2  19633  iscyggen2  19790  iscyg3  19795  issubdrg  20544  isdomn2  21115  ishil2  21493  rintopn  22631  isbasis2g  22671  tgval2  22679  eltg2b  22682  tgss2  22710  basgen2  22712  bastop1  22716  intcld  22764  unicld  22770  isclo  22811  isclo2  22812  neips  22837  opnnei  22844  neiptopnei  22856  isperf3  22877  ssidcn  22979  ist1-3  23073  cmpcov2  23114  cmpsub  23124  2ndcdisj2  23181  txkgen  23376  xkoinjcn  23411  tgqtop  23436  flimopn  23699  flfnei  23715  tmdcn2  23813  qustgplem  23845  cfil3i  25010  cmetcaulem  25029  ovolfioo  25208  ovolficc  25209  ovolicc2lem4  25261  opnmblALT  25344  xrlimcnp  26697  madebdayim  27607  uvtxnbgrss  28904  iscplgr  28927  vdiscusgrb  29042  ubthlem1  30378  isdrng4  32653  prmidl2  32821  hasheuni  33369  dmvlsiga  33413  ispisys2  33437  omssubadd  33585  eulerpartlemr  33659  eulerpartlemn  33666  cvmlift2lem1  34579  cvmlift2lem12  34591  mclsax  34846  setinds  35042  isfne4  35528  isfne2  35530  isfne3  35531  neibastop2lem  35548  filnetlem4  35569  fvineqsneq  36596  fin2so  36778  poimirlem24  36815  poimirlem27  36818  nninfnub  36922  unichnidl  37202  ispridl2  37209  n0elqs  37498  pmapglb  38944  hdmapoc  41105  isnacs2  41746  setindtrs  42066  dford3lem2  42068  dford3  42069  ssunib  42271  ntrneicls00  43142  ntrneixb  43148  ntrneik3  43149  ntrneix3  43150  ntrneik13  43151  ntrneix13  43152  pwssfi  44034  ssdf  44066  ballss3  44084  iunincfi  44085  restuni3  44109  disjf1o  44189  mapss2  44203  difmap  44205  unirnmap  44206  inmap  44207  difmapsn  44210  uzfissfz  44335  iuneqfzuzlem  44343  ssuzfz  44358  iccdificc  44551  iooiinicc  44554  ressiocsup  44566  ressioosup  44567  iooiinioc  44568  ressiooinf  44569  fsumiunss  44590  limciccioolb  44636  limcicciooub  44652  limcresiooub  44657  limsupresxr  44781  liminfresxr  44782  icccncfext  44902  dmvolss  45000  stoweidlem31  45046  stoweidlem39  45054  fourierdlem8  45130  fourierdlem27  45149  fourierdlem38  45160  fourierdlem40  45162  fourierdlem41  45163  fourierdlem46  45167  fourierdlem48  45169  fourierdlem49  45170  fourierdlem51  45172  fourierdlem64  45185  fourierdlem70  45191  fourierdlem71  45192  fourierdlem76  45197  fourierdlem78  45199  fourierdlem79  45200  fourierdlem80  45201  fourierdlem93  45214  fourierdlem97  45218  fourierdlem103  45224  fourierdlem104  45225  salexct  45349  salgencntex  45358  gsumge0cl  45386  sge0fodjrnlem  45431  sge0reuz  45462  iundjiun  45475  icoresmbl  45558  hoicvr  45563  hoidmv1le  45609  hoidmvlelem1  45610  hoidmvlelem3  45612  hoiqssbllem2  45638  hspmbllem2  45642  opnvonmbllem2  45648  iinhoiicc  45689  smfpimbor1lem2  45814  isclatd  47696  setrec1lem2  47821  setrec1lem3  47822