Theorem dfss3 3983

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1534   ∈ wcel 2105  ∀wral 3058   ⊆ wss 3962

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 3059  df-ss 3979

This theorem is referenced by:  ssrab  4082  dfss5  4280  elpwunsn  4688  eqsn  4833  uni0b  4937  uni0c  4938  ssint  4968  ssiinf  5058  sspwuni  5104  dftr3  5270  wefrc  5682  rninxp  6200  frpoinsg  6365  wfisgOLD  6376  ordunisssuc  6491  fnres  6695  eqfnfv3  7052  funimass3  7073  ffvresb  7144  tfisg  7874  tfis  7875  smogt  8405  cofonr  8710  naddrid  8719  unifi  9381  unifi2  9382  fissuni  9394  fipreima  9395  cantnf  9730  frinsg  9788  tz9.12lem3  9826  r1elss  9843  rankval3b  9863  rankonidlem  9865  bndrank  9878  iscard  10012  cfub  10286  cflm  10287  fin1a2s  10451  dcomex  10484  ttukeylem6  10551  unirnfdomd  10604  alephreg  10619  tskord  10817  gruuni  10837  intgru  10851  grudomon  10854  axgroth3  10868  suplem1pr  11089  supexpr  11091  supsr  11149  hashfun  14472  4sqlem19  16996  imasaddfnlem  17574  imasvscafn  17583  setcepi  18141  acsfiindd  18610  sylow2blem3  19654  sylow3lem6  19664  efgval2  19756  iscyggen2  19913  iscyg3  19918  isdomn2  20727  isdomn2OLD  20728  issubdrg  20797  ishil2  21756  rintopn  22930  isbasis2g  22970  tgval2  22978  eltg2b  22981  tgss2  23009  basgen2  23011  bastop1  23015  intcld  23063  unicld  23069  isclo  23110  isclo2  23111  neips  23136  opnnei  23143  neiptopnei  23155  isperf3  23176  ssidcn  23278  ist1-3  23372  cmpcov2  23413  cmpsub  23423  2ndcdisj2  23480  txkgen  23675  xkoinjcn  23710  tgqtop  23735  flimopn  23998  flfnei  24014  tmdcn2  24112  qustgplem  24144  cfil3i  25316  cmetcaulem  25335  ovolfioo  25515  ovolficc  25516  ovolicc2lem4  25568  opnmblALT  25651  xrlimcnp  27025  madebdayim  27940  uvtxnbgrss  29423  iscplgr  29446  vdiscusgrb  29562  ubthlem1  30898  isdrng4  33278  prmidl2  33448  hasheuni  34065  dmvlsiga  34109  ispisys2  34133  omssubadd  34281  eulerpartlemr  34355  eulerpartlemn  34362  cvmlift2lem1  35286  cvmlift2lem12  35298  mclsax  35553  setinds  35759  isfne4  36322  isfne2  36324  isfne3  36325  neibastop2lem  36342  filnetlem4  36363  fvineqsneq  37394  fin2so  37593  poimirlem24  37630  poimirlem27  37633  nninfnub  37737  unichnidl  38017  ispridl2  38024  n0elqs  38307  pmapglb  39752  hdmapoc  41913  isnacs2  42693  setindtrs  43013  dford3lem2  43015  dford3  43016  ssunib  43208  ntrneicls00  44078  ntrneixb  44084  ntrneik3  44085  ntrneix3  44086  ntrneik13  44087  ntrneix13  44088  pwssfi  44984  ssdf  45014  ballss3  45032  iunincfi  45033  restuni3  45057  disjf1o  45133  mapss2  45147  difmap  45149  unirnmap  45150  inmap  45151  difmapsn  45154  uzfissfz  45275  iuneqfzuzlem  45283  ssuzfz  45298  iccdificc  45491  iooiinicc  45494  ressiocsup  45506  ressioosup  45507  iooiinioc  45508  ressiooinf  45509  fsumiunss  45530  limciccioolb  45576  limcicciooub  45592  limcresiooub  45597  limsupresxr  45721  liminfresxr  45722  icccncfext  45842  dmvolss  45940  stoweidlem31  45986  stoweidlem39  45994  fourierdlem8  46070  fourierdlem27  46089  fourierdlem38  46100  fourierdlem40  46102  fourierdlem41  46103  fourierdlem46  46107  fourierdlem48  46109  fourierdlem49  46110  fourierdlem51  46112  fourierdlem64  46125  fourierdlem70  46131  fourierdlem71  46132  fourierdlem76  46137  fourierdlem78  46139  fourierdlem79  46140  fourierdlem80  46141  fourierdlem93  46154  fourierdlem97  46158  fourierdlem103  46164  fourierdlem104  46165  salexct  46289  salgencntex  46298  gsumge0cl  46326  sge0fodjrnlem  46371  sge0reuz  46402  iundjiun  46415  icoresmbl  46498  hoicvr  46503  hoidmv1le  46549  hoidmvlelem1  46550  hoidmvlelem3  46552  hoiqssbllem2  46578  hspmbllem2  46582  opnvonmbllem2  46588  iinhoiicc  46629  smfpimbor1lem2  46754  isclatd  48771  setrec1lem2  48918  setrec1lem3  48919