Theorem dfss3 3947

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538   ∈ wcel 2108  ∀wral 3051   ⊆ wss 3926

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 3052  df-ss 3943

This theorem is referenced by:  ssrab  4048  dfss5  4250  elpwunsn  4660  eqsn  4805  uni0b  4909  uni0c  4910  ssint  4940  ssiinf  5030  sspwuni  5076  dftr3  5235  wefrc  5648  rninxp  6168  frpoinsg  6332  wfisgOLD  6343  ordunisssuc  6459  fnres  6664  eqfnfv3  7022  funimass3  7043  ffvresb  7114  tfisg  7847  tfis  7848  smogt  8379  cofonr  8684  naddrid  8693  pwssfi  9189  unifi  9354  unifi2  9355  fissuni  9367  fipreima  9368  cantnf  9705  frinsg  9763  tz9.12lem3  9801  r1elss  9818  rankval3b  9838  rankonidlem  9840  bndrank  9853  iscard  9987  cfub  10261  cflm  10262  fin1a2s  10426  dcomex  10459  ttukeylem6  10526  unirnfdomd  10579  alephreg  10594  tskord  10792  gruuni  10812  intgru  10826  grudomon  10829  axgroth3  10843  suplem1pr  11064  supexpr  11066  supsr  11124  hashfun  14453  4sqlem19  16981  imasaddfnlem  17540  imasvscafn  17549  setcepi  18099  acsfiindd  18561  sylow2blem3  19601  sylow3lem6  19611  efgval2  19703  iscyggen2  19860  iscyg3  19865  isdomn2  20669  isdomn2OLD  20670  issubdrg  20738  ishil2  21677  rintopn  22845  isbasis2g  22884  tgval2  22892  eltg2b  22895  tgss2  22923  basgen2  22925  bastop1  22929  intcld  22976  unicld  22982  isclo  23023  isclo2  23024  neips  23049  opnnei  23056  neiptopnei  23068  isperf3  23089  ssidcn  23191  ist1-3  23285  cmpcov2  23326  cmpsub  23336  2ndcdisj2  23393  txkgen  23588  xkoinjcn  23623  tgqtop  23648  flimopn  23911  flfnei  23927  tmdcn2  24025  qustgplem  24057  cfil3i  25219  cmetcaulem  25238  ovolfioo  25418  ovolficc  25419  ovolicc2lem4  25471  opnmblALT  25554  xrlimcnp  26928  madebdayim  27843  uvtxnbgrss  29317  iscplgr  29340  vdiscusgrb  29456  ubthlem1  30797  isdrng4  33235  prmidl2  33402  hasheuni  34062  dmvlsiga  34106  ispisys2  34130  omssubadd  34278  eulerpartlemr  34352  eulerpartlemn  34359  cvmlift2lem1  35270  cvmlift2lem12  35282  mclsax  35537  setinds  35742  isfne4  36304  isfne2  36306  isfne3  36307  neibastop2lem  36324  filnetlem4  36345  fvineqsneq  37376  fin2so  37577  poimirlem24  37614  poimirlem27  37617  nninfnub  37721  unichnidl  38001  ispridl2  38008  n0elqs  38290  pmapglb  39735  hdmapoc  41896  isnacs2  42676  setindtrs  42996  dford3lem2  42998  dford3  42999  ssunib  43191  ntrneicls00  44060  ntrneixb  44066  ntrneik3  44067  ntrneix3  44068  ntrneik13  44069  ntrneix13  44070  trfr  44935  ssabso  44947  ssdf  45047  ballss3  45065  iunincfi  45066  restuni3  45090  disjf1o  45163  mapss2  45177  difmap  45179  unirnmap  45180  inmap  45181  difmapsn  45184  uzfissfz  45301  iuneqfzuzlem  45309  ssuzfz  45324  iccdificc  45516  iooiinicc  45519  ressiocsup  45531  ressioosup  45532  iooiinioc  45533  ressiooinf  45534  fsumiunss  45552  limciccioolb  45598  limcicciooub  45614  limcresiooub  45619  limsupresxr  45743  liminfresxr  45744  icccncfext  45864  dmvolss  45962  stoweidlem31  46008  stoweidlem39  46016  fourierdlem8  46092  fourierdlem27  46111  fourierdlem38  46122  fourierdlem40  46124  fourierdlem41  46125  fourierdlem46  46129  fourierdlem48  46131  fourierdlem49  46132  fourierdlem51  46134  fourierdlem64  46147  fourierdlem70  46153  fourierdlem71  46154  fourierdlem76  46159  fourierdlem78  46161  fourierdlem79  46162  fourierdlem80  46163  fourierdlem93  46176  fourierdlem97  46180  fourierdlem103  46186  fourierdlem104  46187  salexct  46311  salgencntex  46320  gsumge0cl  46348  sge0fodjrnlem  46393  sge0reuz  46424  iundjiun  46437  icoresmbl  46520  hoicvr  46525  hoidmv1le  46571  hoidmvlelem1  46572  hoidmvlelem3  46574  hoiqssbllem2  46600  hspmbllem2  46604  opnvonmbllem2  46610  iinhoiicc  46651  smfpimbor1lem2  46776  isclatd  48905  setrec1lem2  49500  setrec1lem3  49501