Theorem dfss3 3913

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1539   ∈ wcel 2109  ∀wral 3065   ⊆ wss 3891

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-v 3432  df-in 3898  df-ss 3908

This theorem is referenced by:  ssrab  4010  dfss5  4203  elpwunsn  4624  eqsn  4767  uni0b  4872  uni0c  4873  ssint  4900  ssiinf  4988  sspwuni  5033  dftr3  5199  wefrc  5582  rninxp  6079  frpoinsg  6243  wfisgOLD  6254  ordunisssuc  6365  fnres  6555  eqfnfv3  6905  funimass3  6925  ffvresb  6992  tfis  7689  smogt  8182  unifi  9069  unifi2  9070  fissuni  9085  fipreima  9086  cantnf  9412  frinsg  9493  tz9.12lem3  9531  r1elss  9548  rankval3b  9568  rankonidlem  9570  bndrank  9583  iscard  9717  cfub  9989  cflm  9990  fin1a2s  10154  dcomex  10187  ttukeylem6  10254  unirnfdomd  10307  alephreg  10322  tskord  10520  gruuni  10540  intgru  10554  grudomon  10557  axgroth3  10571  suplem1pr  10792  supexpr  10794  supsr  10852  hashfun  14133  4sqlem19  16645  imasaddfnlem  17220  imasvscafn  17229  setcepi  17784  acsfiindd  18252  sylow2blem3  19208  sylow3lem6  19218  efgval2  19311  iscyggen2  19462  iscyg3  19467  issubdrg  20030  isdomn2  20551  ishil2  20907  rintopn  22039  isbasis2g  22079  tgval2  22087  eltg2b  22090  tgss2  22118  basgen2  22120  bastop1  22124  intcld  22172  unicld  22178  isclo  22219  isclo2  22220  neips  22245  opnnei  22252  neiptopnei  22264  isperf3  22285  ssidcn  22387  ist1-3  22481  cmpcov2  22522  cmpsub  22532  2ndcdisj2  22589  txkgen  22784  xkoinjcn  22819  tgqtop  22844  flimopn  23107  flfnei  23123  tmdcn2  23221  qustgplem  23253  cfil3i  24414  cmetcaulem  24433  ovolfioo  24612  ovolficc  24613  ovolicc2lem4  24665  opnmblALT  24748  xrlimcnp  26099  uvtxnbgrss  27740  iscplgr  27763  vdiscusgrb  27878  ubthlem1  29211  prmidl2  31595  hasheuni  32032  dmvlsiga  32076  ispisys2  32100  omssubadd  32246  eulerpartlemr  32320  eulerpartlemn  32327  cvmlift2lem1  33243  cvmlift2lem12  33255  mclsax  33510  setinds  33733  tfisg  33765  naddid1  33815  madebdayim  34049  isfne4  34508  isfne2  34510  isfne3  34511  neibastop2lem  34528  filnetlem4  34549  fvineqsneq  35562  fin2so  35743  poimirlem24  35780  poimirlem27  35783  nninfnub  35888  unichnidl  36168  ispridl2  36175  n0elqs  36440  pmapglb  37763  hdmapoc  39924  isnacs2  40508  setindtrs  40827  dford3lem2  40829  dford3  40830  ntrneicls00  41652  ntrneixb  41658  ntrneik3  41659  ntrneix3  41660  ntrneik13  41661  ntrneix13  41662  pwssfi  42546  ssdf  42578  ballss3  42596  iunincfi  42597  restuni3  42620  disjf1o  42682  mapss2  42698  difmap  42700  unirnmap  42701  inmap  42702  difmapsn  42705  uzfissfz  42819  iuneqfzuzlem  42827  ssuzfz  42842  iccdificc  43031  iooiinicc  43034  ressiocsup  43046  ressioosup  43047  iooiinioc  43048  ressiooinf  43049  fsumiunss  43070  limciccioolb  43116  limcicciooub  43132  limcresiooub  43137  limsupresxr  43261  liminfresxr  43262  icccncfext  43382  dmvolss  43480  stoweidlem31  43526  stoweidlem39  43534  fourierdlem8  43610  fourierdlem27  43629  fourierdlem38  43640  fourierdlem40  43642  fourierdlem41  43643  fourierdlem46  43647  fourierdlem48  43649  fourierdlem49  43650  fourierdlem51  43652  fourierdlem64  43665  fourierdlem70  43671  fourierdlem71  43672  fourierdlem76  43677  fourierdlem78  43679  fourierdlem79  43680  fourierdlem80  43681  fourierdlem93  43694  fourierdlem97  43698  fourierdlem103  43704  fourierdlem104  43705  salexct  43827  salgencntex  43836  gsumge0cl  43863  sge0fodjrnlem  43908  sge0reuz  43939  iundjiun  43952  icoresmbl  44035  hoicvr  44040  hoidmv1le  44086  hoidmvlelem1  44087  hoidmvlelem3  44089  hoiqssbllem2  44115  hspmbllem2  44119  opnvonmbllem2  44125  iinhoiicc  44166  smfpimbor1lem2  44284  isclatd  46221  setrec1lem2  46346  setrec1lem3  46347