Theorem dfss3 3923

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

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1557   ∈ wcel 2141  ∀wral 3075   ⊆ wss 3902

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 209  df-ral 3076  df-ss 3919

This theorem is referenced by:  ssrab  4022  dfss5  4225  elpwunsn  4640  eqsn  4784  uni0b  4889  uni0c  4890  ssint  4919  ssiinf  5009  sspwuni  5054  dftr3  5209  wefrc  5637  rninxp  6160  frpoinsg  6325  ordunisssuc  6449  fnres  6643  eqfnfv3  7008  funimass3  7030  ffvresb  7102  tfisg  7829  tfis  7830  smogt  8332  cofonr  8638  naddrid  8648  pwssfi  9139  unifi  9281  unifi2  9282  fissuni  9294  fipreima  9295  cantnf  9642  setinds  9698  frinsg  9703  tz9.12lem3  9741  r1elss  9758  rankval3b  9778  rankonidlem  9780  bndrank  9793  iscard  9927  cfub  10199  cflm  10200  fin1a2s  10365  dcomex  10398  ttukeylem6  10465  unirnfdomd  10519  alephreg  10534  tskord  10732  gruuni  10752  intgru  10766  grudomon  10769  axgroth3  10783  suplem1pr  11004  supexpr  11006  supsr  11064  hashfun  14444  4sqlem19  16990  imasaddfnlem  17549  imasvscafn  17558  setcepi  18112  acsfiindd  18576  sylow2blem3  19653  sylow3lem6  19663  efgval2  19755  iscyggen2  19912  iscyg3  19917  isdomn2  20748  isdomn2OLD  20749  issubdrg  20817  ishil2  21759  rintopn  22957  isbasis2g  22996  tgval2  23004  eltg2b  23007  tgss2  23035  basgen2  23037  bastop1  23041  intcld  23088  unicld  23094  isclo  23135  isclo2  23136  neips  23161  opnnei  23168  neiptopnei  23180  isperf3  23201  ssidcn  23303  ist1-3  23397  cmpcov2  23438  cmpsub  23448  2ndcdisj2  23505  txkgen  23700  xkoinjcn  23735  tgqtop  23760  flimopn  24023  flfnei  24039  tmdcn2  24137  qustgplem  24169  cfil3i  25319  cmetcaulem  25338  ovolfioo  25517  ovolficc  25518  ovolicc2lem4  25570  opnmblALT  25653  xrlimcnp  27021  madebdayim  27969  oldfib  28458  uvtxnbgrss  29550  iscplgr  29573  vdiscusgrb  29688  ubthlem1  31030  isdrng4  33443  prmidl2  33588  hasheuni  34343  dmvlsiga  34387  ispisys2  34411  omssubadd  34558  eulerpartlemr  34632  eulerpartlemn  34639  cvmlift2lem1  35613  cvmlift2lem12  35625  mclsax  35880  isfne4  36661  isfne2  36663  isfne3  36664  neibastop2lem  36681  filnetlem4  36702  fvineqsneq  37867  fin2so  38067  poimirlem24  38104  poimirlem27  38107  nninfnub  38211  unichnidl  38491  ispridl2  38498  n0elqs  38792  ssdmral  38839  pmapglb  40355  hdmapoc  42516  isnacs2  43248  setindtrs  43563  dford3lem2  43565  dford3  43566  ssunib  43758  ntrneicls00  44626  ntrneixb  44632  ntrneik3  44633  ntrneix3  44634  ntrneik13  44635  ntrneix13  44636  trfr  45499  ssabso  45511  ssdf  45616  ballss3  45632  iunincfi  45633  restuni3  45657  disjf1o  45730  mapss2  45743  difmap  45744  unirnmap  45745  inmap  45746  difmapsn  45749  uzfissfz  45863  iuneqfzuzlem  45871  ssuzfz  45886  iccdificc  46076  iooiinicc  46079  ressiocsup  46091  ressioosup  46092  iooiinioc  46093  ressiooinf  46094  fsumiunss  46112  limciccioolb  46158  limcicciooub  46172  limcresiooub  46177  limsupresxr  46301  liminfresxr  46302  icccncfext  46422  dmvolss  46520  stoweidlem31  46566  stoweidlem39  46574  fourierdlem8  46650  fourierdlem27  46669  fourierdlem38  46680  fourierdlem40  46682  fourierdlem41  46683  fourierdlem46  46687  fourierdlem51  46692  fourierdlem64  46705  fourierdlem70  46711  fourierdlem71  46712  fourierdlem76  46717  fourierdlem78  46719  fourierdlem79  46720  fourierdlem80  46721  fourierdlem93  46734  fourierdlem97  46738  fourierdlem103  46744  fourierdlem104  46745  salexct  46869  salgencntex  46878  gsumge0cl  46906  sge0fodjrnlem  46951  sge0reuz  46982  iundjiun  46995  icoresmbl  47078  hoidmv1le  47129  hoidmvlelem1  47130  hoidmvlelem3  47132  hoiqssbllem2  47158  hspmbllem2  47162  opnvonmbllem2  47168  iinhoiicc  47209  smfpimbor1lem2  47334  isclatd  49565  setrec1lem2  50270  setrec1lem3  50271