Theorem dfss3 3888

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

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1541   ∈ wcel 2110  ∀wral 3061   ⊆ wss 3866

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3066  df-v 3410  df-in 3873  df-ss 3883

This theorem is referenced by:  ssrab  3986  dfss5  4179  elpwunsn  4599  eqsn  4742  uni0b  4847  uni0c  4848  ssint  4875  ssiinf  4963  sspwuni  5008  dftr3  5165  wefrc  5545  rninxp  6042  frpoinsg  6197  wfisg  6205  ordunisssuc  6315  fnres  6504  eqfnfv3  6854  funimass3  6874  ffvresb  6941  tfis  7633  smogt  8104  unifi  8965  unifi2  8966  fissuni  8981  fipreima  8982  cantnf  9308  frinsg  9367  tz9.12lem3  9405  r1elss  9422  rankval3b  9442  rankonidlem  9444  bndrank  9457  iscard  9591  cfub  9863  cflm  9864  fin1a2s  10028  dcomex  10061  ttukeylem6  10128  unirnfdomd  10181  alephreg  10196  tskord  10394  gruuni  10414  intgru  10428  grudomon  10431  axgroth3  10445  suplem1pr  10666  supexpr  10668  supsr  10726  hashfun  14004  4sqlem19  16516  imasaddfnlem  17033  imasvscafn  17042  setcepi  17594  acsfiindd  18059  sylow2blem3  19011  sylow3lem6  19021  efgval2  19114  iscyggen2  19265  iscyg3  19270  issubdrg  19825  isdomn2  20337  ishil2  20681  rintopn  21806  isbasis2g  21845  tgval2  21853  eltg2b  21856  tgss2  21884  basgen2  21886  bastop1  21890  intcld  21937  unicld  21943  isclo  21984  isclo2  21985  neips  22010  opnnei  22017  neiptopnei  22029  isperf3  22050  ssidcn  22152  ist1-3  22246  cmpcov2  22287  cmpsub  22297  2ndcdisj2  22354  txkgen  22549  xkoinjcn  22584  tgqtop  22609  flimopn  22872  flfnei  22888  tmdcn2  22986  qustgplem  23018  cfil3i  24166  cmetcaulem  24185  ovolfioo  24364  ovolficc  24365  ovolicc2lem4  24417  opnmblALT  24500  xrlimcnp  25851  uvtxnbgrss  27480  iscplgr  27503  vdiscusgrb  27618  ubthlem1  28951  prmidl2  31330  hasheuni  31765  dmvlsiga  31809  ispisys2  31833  omssubadd  31979  eulerpartlemr  32053  eulerpartlemn  32060  cvmlift2lem1  32977  cvmlift2lem12  32989  mclsax  33244  setinds  33473  tfisg  33505  naddid1  33573  madebdayim  33807  isfne4  34266  isfne2  34268  isfne3  34269  neibastop2lem  34286  filnetlem4  34307  fvineqsneq  35320  fin2so  35501  poimirlem24  35538  poimirlem27  35541  nninfnub  35646  unichnidl  35926  ispridl2  35933  n0elqs  36198  pmapglb  37521  hdmapoc  39682  isnacs2  40231  setindtrs  40550  dford3lem2  40552  dford3  40553  ntrneicls00  41376  ntrneixb  41382  ntrneik3  41383  ntrneix3  41384  ntrneik13  41385  ntrneix13  41386  pwssfi  42266  ssdf  42298  ballss3  42316  iunincfi  42317  restuni3  42340  disjf1o  42402  mapss2  42418  difmap  42420  unirnmap  42421  inmap  42422  difmapsn  42425  uzfissfz  42538  iuneqfzuzlem  42546  ssuzfz  42561  iccdificc  42752  iooiinicc  42755  ressiocsup  42767  ressioosup  42768  iooiinioc  42769  ressiooinf  42770  fsumiunss  42791  limciccioolb  42837  limcicciooub  42853  limcresiooub  42858  limsupresxr  42982  liminfresxr  42983  icccncfext  43103  dmvolss  43201  stoweidlem31  43247  stoweidlem39  43255  fourierdlem8  43331  fourierdlem27  43350  fourierdlem38  43361  fourierdlem40  43363  fourierdlem41  43364  fourierdlem46  43368  fourierdlem48  43370  fourierdlem49  43371  fourierdlem51  43373  fourierdlem64  43386  fourierdlem70  43392  fourierdlem71  43393  fourierdlem76  43398  fourierdlem78  43400  fourierdlem79  43401  fourierdlem80  43402  fourierdlem93  43415  fourierdlem97  43419  fourierdlem103  43425  fourierdlem104  43426  salexct  43548  salgencntex  43557  gsumge0cl  43584  sge0fodjrnlem  43629  sge0reuz  43660  iundjiun  43673  icoresmbl  43756  hoicvr  43761  hoidmv1le  43807  hoidmvlelem1  43808  hoidmvlelem3  43810  hoiqssbllem2  43836  hspmbllem2  43840  opnvonmbllem2  43846  iinhoiicc  43887  smfpimbor1lem2  44005  isclatd  45942  setrec1lem2  46065  setrec1lem3  46066