Theorem dfss3 3926

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538   ∈ wcel 2109  ∀wral 3044   ⊆ wss 3905

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 3045  df-ss 3922

This theorem is referenced by:  ssrab  4026  dfss5  4228  elpwunsn  4638  eqsn  4783  uni0b  4887  uni0c  4888  ssint  4917  ssiinf  5006  sspwuni  5052  dftr3  5207  wefrc  5617  rninxp  6132  frpoinsg  6295  ordunisssuc  6419  fnres  6613  eqfnfv3  6971  funimass3  6992  ffvresb  7063  tfisg  7794  tfis  7795  smogt  8297  cofonr  8599  naddrid  8608  pwssfi  9101  unifi  9253  unifi2  9254  fissuni  9266  fipreima  9267  cantnf  9608  frinsg  9666  tz9.12lem3  9704  r1elss  9721  rankval3b  9741  rankonidlem  9743  bndrank  9756  iscard  9890  cfub  10162  cflm  10163  fin1a2s  10327  dcomex  10360  ttukeylem6  10427  unirnfdomd  10480  alephreg  10495  tskord  10693  gruuni  10713  intgru  10727  grudomon  10730  axgroth3  10744  suplem1pr  10965  supexpr  10967  supsr  11025  hashfun  14363  4sqlem19  16894  imasaddfnlem  17451  imasvscafn  17460  setcepi  18014  acsfiindd  18478  sylow2blem3  19520  sylow3lem6  19530  efgval2  19622  iscyggen2  19779  iscyg3  19784  isdomn2  20615  isdomn2OLD  20616  issubdrg  20684  ishil2  21645  rintopn  22813  isbasis2g  22852  tgval2  22860  eltg2b  22863  tgss2  22891  basgen2  22893  bastop1  22897  intcld  22944  unicld  22950  isclo  22991  isclo2  22992  neips  23017  opnnei  23024  neiptopnei  23036  isperf3  23057  ssidcn  23159  ist1-3  23253  cmpcov2  23294  cmpsub  23304  2ndcdisj2  23361  txkgen  23556  xkoinjcn  23591  tgqtop  23616  flimopn  23879  flfnei  23895  tmdcn2  23993  qustgplem  24025  cfil3i  25186  cmetcaulem  25205  ovolfioo  25385  ovolficc  25386  ovolicc2lem4  25438  opnmblALT  25521  xrlimcnp  26895  madebdayim  27821  uvtxnbgrss  29356  iscplgr  29379  vdiscusgrb  29495  ubthlem1  30833  isdrng4  33253  prmidl2  33397  hasheuni  34071  dmvlsiga  34115  ispisys2  34139  omssubadd  34287  eulerpartlemr  34361  eulerpartlemn  34368  cvmlift2lem1  35294  cvmlift2lem12  35306  mclsax  35561  setinds  35771  isfne4  36333  isfne2  36335  isfne3  36336  neibastop2lem  36353  filnetlem4  36374  fvineqsneq  37405  fin2so  37606  poimirlem24  37643  poimirlem27  37646  nninfnub  37750  unichnidl  38030  ispridl2  38037  n0elqs  38319  pmapglb  39769  hdmapoc  41930  isnacs2  42699  setindtrs  43018  dford3lem2  43020  dford3  43021  ssunib  43213  ntrneicls00  44082  ntrneixb  44088  ntrneik3  44089  ntrneix3  44090  ntrneik13  44091  ntrneix13  44092  trfr  44956  ssabso  44968  ssdf  45073  ballss3  45091  iunincfi  45092  restuni3  45116  disjf1o  45189  mapss2  45203  difmap  45205  unirnmap  45206  inmap  45207  difmapsn  45210  uzfissfz  45326  iuneqfzuzlem  45334  ssuzfz  45349  iccdificc  45540  iooiinicc  45543  ressiocsup  45555  ressioosup  45556  iooiinioc  45557  ressiooinf  45558  fsumiunss  45576  limciccioolb  45622  limcicciooub  45638  limcresiooub  45643  limsupresxr  45767  liminfresxr  45768  icccncfext  45888  dmvolss  45986  stoweidlem31  46032  stoweidlem39  46040  fourierdlem8  46116  fourierdlem27  46135  fourierdlem38  46146  fourierdlem40  46148  fourierdlem41  46149  fourierdlem46  46153  fourierdlem48  46155  fourierdlem49  46156  fourierdlem51  46158  fourierdlem64  46171  fourierdlem70  46177  fourierdlem71  46178  fourierdlem76  46183  fourierdlem78  46185  fourierdlem79  46186  fourierdlem80  46187  fourierdlem93  46200  fourierdlem97  46204  fourierdlem103  46210  fourierdlem104  46211  salexct  46335  salgencntex  46344  gsumge0cl  46372  sge0fodjrnlem  46417  sge0reuz  46448  iundjiun  46461  icoresmbl  46544  hoicvr  46549  hoidmv1le  46595  hoidmvlelem1  46596  hoidmvlelem3  46598  hoiqssbllem2  46624  hspmbllem2  46628  opnvonmbllem2  46634  iinhoiicc  46675  smfpimbor1lem2  46800  isclatd  48987  setrec1lem2  49693  setrec1lem3  49694