Theorem dfss3 3920

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568   ∈ wcel 2145  ∀wral 3076   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ral 3077  df-ss 3916

This theorem is used by:  ssrab  4019  dfss5  4221  elpwunsn  4645  eqsn  4790  uni0b  4894  uni0c  4895  ssint  4924  ssiinf  5013  sspwuni  5060  dftr3  5217  wefrc  5649  rninxp  6172  frpoinsg  6341  ordunisssuc  6466  fnres  6659  eqfnfv3  7024  funimass3  7046  ffvresb  7119  tfisg  7850  tfis  7851  smogt  8356  cofonr  8662  naddrid  8672  pwssfi  9171  unifi  9311  unifi2  9312  fissuni  9324  fipreima  9325  cantnf  9672  setinds  9728  frinsg  9733  tz9.12lem3  9771  r1elss  9788  rankval3b  9808  rankonidlem  9810  bndrank  9823  iscard  9980  cfub  10250  cflm  10251  fin1a2s  10416  dcomex  10449  ttukeylem6  10516  unirnfdomd  10576  alephreg  10591  tskord  10789  gruuni  10809  intgru  10823  grudomon  10826  axgroth3  10840  suplem1pr  11061  supexpr  11063  supsr  11121  hashfun  14502  4sqlem19  17055  imasaddfnlem  17614  imasvscafn  17623  setcepi  18177  acsfiindd  18641  sylow2blem3  19749  sylow3lem6  19759  efgval2  19851  iscyggen2  20008  iscyg3  20013  isdomn2  20873  isdrng4  20902  issubdrg  20946  unichnlidl  21425  prmidl2  21529  ishil2  21932  rintopn  23134  isbasis2g  23173  tgval2  23181  eltg2b  23184  tgss2  23212  basgen2  23214  bastop1  23218  intcld  23265  unicld  23271  isclo  23312  isclo2  23313  neips  23338  opnnei  23345  neiptopnei  23357  isperf3  23378  ssidcn  23480  ist1-3  23574  cmpcov2  23615  cmpsub  23625  2ndcdisj2  23683  txkgen  23878  xkoinjcn  23913  tgqtop  23938  flimopn  24201  flfnei  24217  tmdcn2  24315  qustgplem  24347  cfil3i  25497  cmetcaulem  25516  ovolfioo  25695  ovolficc  25696  ovolicc2lem4  25748  opnmblALT  25831  xrlimcnp  27205  madebdayim  28153  oldfib  28642  uvtxnbgrss  29852  iscplgr  29875  vdiscusgrb  29990  ubthlem1  31351  hasheuni  34595  dmvlsiga  34639  ispisys2  34664  omssubadd  34811  eulerpartlemr  34885  eulerpartlemn  34892  cvmlift2lem1  35881  cvmlift2lem12  35893  mclsax  36148  dffr5  36333  dffr7  36535  nmulrid  36777  isfne4  36959  isfne2  36961  isfne3  36962  neibastop2lem  36979  filnetlem4  37000  fvineqsneq  38166  fin2so  38361  poimirlem24  38393  poimirlem27  38396  nninfnub  38501  unichnidl  38781  ispridl2  38788  n0elqs  39080  ssdmral  39127  pmapglb  40643  hdmapoc  42804  isnacs2  43551  setindtrs  43866  dford3lem2  43868  dford3  43869  ssunib  44061  ntrneicls00  44929  ntrneixb  44935  ntrneik3  44936  ntrneix3  44937  ntrneik13  44938  ntrneix13  44939  trfr  45785  ssabso  45797  ssdf  45909  ballss3  45925  iunincfi  45926  restuni3  45950  disjf1o  46023  mapss2  46036  difmap  46037  unirnmap  46038  inmap  46039  difmapsn  46042  uzfissfz  46156  iuneqfzuzlem  46164  ssuzfz  46179  iccdificc  46369  iooiinicc  46372  ressiocsup  46384  ressioosup  46385  iooiinioc  46386  ressiooinf  46387  fsumiunss  46405  limciccioolb  46451  limcicciooub  46465  limcresiooub  46470  limsupresxr  46594  liminfresxr  46595  icccncfext  46715  dmvolss  46813  stoweidlem31  46859  stoweidlem39  46867  fourierdlem8  46943  fourierdlem27  46962  fourierdlem38  46973  fourierdlem40  46975  fourierdlem41  46976  fourierdlem46  46980  fourierdlem51  46985  fourierdlem64  46998  fourierdlem70  47004  fourierdlem71  47005  fourierdlem76  47010  fourierdlem78  47012  fourierdlem79  47013  fourierdlem80  47014  fourierdlem93  47027  fourierdlem97  47031  fourierdlem103  47037  fourierdlem104  47038  salexct  47162  salgencntex  47171  gsumge0cl  47199  sge0fodjrnlem  47244  sge0reuz  47275  iundjiun  47288  icoresmbl  47371  hoidmv1le  47422  hoidmvlelem1  47423  hoidmvlelem3  47425  hoiqssbllem2  47451  hspmbllem2  47455  opnvonmbllem2  47461  iinhoiicc  47502  smfpimbor1lem2  47627  isclatd  49909  setrec1lem2  50614  setrec1lem3  50615