Theorem dfss3 3932

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 3928	. 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 3911

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 3928

This theorem is referenced by:  ssrab  4032  dfss5  4234  elpwunsn  4644  eqsn  4789  uni0b  4893  uni0c  4894  ssint  4924  ssiinf  5013  sspwuni  5059  dftr3  5215  wefrc  5625  rninxp  6140  frpoinsg  6304  ordunisssuc  6428  fnres  6627  eqfnfv3  6987  funimass3  7008  ffvresb  7079  tfisg  7810  tfis  7811  smogt  8313  cofonr  8615  naddrid  8624  pwssfi  9118  unifi  9271  unifi2  9272  fissuni  9284  fipreima  9285  cantnf  9622  frinsg  9680  tz9.12lem3  9718  r1elss  9735  rankval3b  9755  rankonidlem  9757  bndrank  9770  iscard  9904  cfub  10178  cflm  10179  fin1a2s  10343  dcomex  10376  ttukeylem6  10443  unirnfdomd  10496  alephreg  10511  tskord  10709  gruuni  10729  intgru  10743  grudomon  10746  axgroth3  10760  suplem1pr  10981  supexpr  10983  supsr  11041  hashfun  14378  4sqlem19  16910  imasaddfnlem  17467  imasvscafn  17476  setcepi  18026  acsfiindd  18488  sylow2blem3  19528  sylow3lem6  19538  efgval2  19630  iscyggen2  19787  iscyg3  19792  isdomn2  20596  isdomn2OLD  20597  issubdrg  20665  ishil2  21604  rintopn  22772  isbasis2g  22811  tgval2  22819  eltg2b  22822  tgss2  22850  basgen2  22852  bastop1  22856  intcld  22903  unicld  22909  isclo  22950  isclo2  22951  neips  22976  opnnei  22983  neiptopnei  22995  isperf3  23016  ssidcn  23118  ist1-3  23212  cmpcov2  23253  cmpsub  23263  2ndcdisj2  23320  txkgen  23515  xkoinjcn  23550  tgqtop  23575  flimopn  23838  flfnei  23854  tmdcn2  23952  qustgplem  23984  cfil3i  25145  cmetcaulem  25164  ovolfioo  25344  ovolficc  25345  ovolicc2lem4  25397  opnmblALT  25480  xrlimcnp  26854  madebdayim  27775  uvtxnbgrss  29295  iscplgr  29318  vdiscusgrb  29434  ubthlem1  30772  isdrng4  33218  prmidl2  33385  hasheuni  34048  dmvlsiga  34092  ispisys2  34116  omssubadd  34264  eulerpartlemr  34338  eulerpartlemn  34345  cvmlift2lem1  35262  cvmlift2lem12  35274  mclsax  35529  setinds  35739  isfne4  36301  isfne2  36303  isfne3  36304  neibastop2lem  36321  filnetlem4  36342  fvineqsneq  37373  fin2so  37574  poimirlem24  37611  poimirlem27  37614  nninfnub  37718  unichnidl  37998  ispridl2  38005  n0elqs  38287  pmapglb  39737  hdmapoc  41898  isnacs2  42667  setindtrs  42987  dford3lem2  42989  dford3  42990  ssunib  43182  ntrneicls00  44051  ntrneixb  44057  ntrneik3  44058  ntrneix3  44059  ntrneik13  44060  ntrneix13  44061  trfr  44925  ssabso  44937  ssdf  45042  ballss3  45060  iunincfi  45061  restuni3  45085  disjf1o  45158  mapss2  45172  difmap  45174  unirnmap  45175  inmap  45176  difmapsn  45179  uzfissfz  45295  iuneqfzuzlem  45303  ssuzfz  45318  iccdificc  45510  iooiinicc  45513  ressiocsup  45525  ressioosup  45526  iooiinioc  45527  ressiooinf  45528  fsumiunss  45546  limciccioolb  45592  limcicciooub  45608  limcresiooub  45613  limsupresxr  45737  liminfresxr  45738  icccncfext  45858  dmvolss  45956  stoweidlem31  46002  stoweidlem39  46010  fourierdlem8  46086  fourierdlem27  46105  fourierdlem38  46116  fourierdlem40  46118  fourierdlem41  46119  fourierdlem46  46123  fourierdlem48  46125  fourierdlem49  46126  fourierdlem51  46128  fourierdlem64  46141  fourierdlem70  46147  fourierdlem71  46148  fourierdlem76  46153  fourierdlem78  46155  fourierdlem79  46156  fourierdlem80  46157  fourierdlem93  46170  fourierdlem97  46174  fourierdlem103  46180  fourierdlem104  46181  salexct  46305  salgencntex  46314  gsumge0cl  46342  sge0fodjrnlem  46387  sge0reuz  46418  iundjiun  46431  icoresmbl  46514  hoicvr  46519  hoidmv1le  46565  hoidmvlelem1  46566  hoidmvlelem3  46568  hoiqssbllem2  46594  hspmbllem2  46598  opnvonmbllem2  46604  iinhoiicc  46645  smfpimbor1lem2  46770  isclatd  48944  setrec1lem2  49650  setrec1lem3  49651