Theorem dfss3 3904

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

Syntax hints:   → wi 4   ↔ wb 207  ∀wal 1545   ∈ wcel 2119  ∀wral 3053   ⊆ wss 3883

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 208  df-ral 3054  df-ss 3900

This theorem is referenced by:  ssrab  4002  dfss5  4203  elpwunsn  4616  eqsn  4760  uni0b  4864  uni0c  4865  ssint  4894  ssiinf  4984  sspwuni  5029  dftr3  5184  wefrc  5612  rninxp  6130  frpoinsg  6294  ordunisssuc  6418  fnres  6612  eqfnfv3  6973  funimass3  6995  ffvresb  7067  tfisg  7794  tfis  7795  smogt  8297  cofonr  8600  naddrid  8609  pwssfi  9101  unifi  9244  unifi2  9245  fissuni  9257  fipreima  9258  cantnf  9605  setinds  9661  frinsg  9666  tz9.12lem3  9704  r1elss  9721  rankval3b  9741  rankonidlem  9743  bndrank  9756  iscard  9890  cfub  10162  cflm  10163  fin1a2s  10327  dcomex  10360  ttukeylem6  10427  unirnfdomd  10481  alephreg  10496  tskord  10694  gruuni  10714  intgru  10728  grudomon  10731  axgroth3  10745  suplem1pr  10966  supexpr  10968  supsr  11026  hashfun  14390  4sqlem19  16925  imasaddfnlem  17483  imasvscafn  17492  setcepi  18046  acsfiindd  18510  sylow2blem3  19588  sylow3lem6  19598  efgval2  19690  iscyggen2  19847  iscyg3  19852  isdomn2  20683  isdomn2OLD  20684  issubdrg  20752  ishil2  21694  rintopn  22892  isbasis2g  22931  tgval2  22939  eltg2b  22942  tgss2  22970  basgen2  22972  bastop1  22976  intcld  23023  unicld  23029  isclo  23070  isclo2  23071  neips  23096  opnnei  23103  neiptopnei  23115  isperf3  23136  ssidcn  23238  ist1-3  23332  cmpcov2  23373  cmpsub  23383  2ndcdisj2  23440  txkgen  23635  xkoinjcn  23670  tgqtop  23695  flimopn  23958  flfnei  23974  tmdcn2  24072  qustgplem  24104  cfil3i  25254  cmetcaulem  25273  ovolfioo  25452  ovolficc  25453  ovolicc2lem4  25505  opnmblALT  25588  xrlimcnp  26950  madebdayim  27898  oldfib  28387  uvtxnbgrss  29479  iscplgr  29502  vdiscusgrb  29617  ubthlem1  30959  isdrng4  33379  prmidl2  33524  hasheuni  34269  dmvlsiga  34313  ispisys2  34337  omssubadd  34484  eulerpartlemr  34558  eulerpartlemn  34565  cvmlift2lem1  35530  cvmlift2lem12  35542  mclsax  35797  isfne4  36568  isfne2  36570  isfne3  36571  neibastop2lem  36588  filnetlem4  36609  fvineqsneq  37774  fin2so  37974  poimirlem24  38011  poimirlem27  38014  nninfnub  38118  unichnidl  38398  ispridl2  38405  n0elqs  38699  ssdmral  38746  pmapglb  40262  hdmapoc  42423  isnacs2  43155  setindtrs  43470  dford3lem2  43472  dford3  43473  ssunib  43665  ntrneicls00  44533  ntrneixb  44539  ntrneik3  44540  ntrneix3  44541  ntrneik13  44542  ntrneix13  44543  trfr  45406  ssabso  45418  ssdf  45523  ballss3  45540  iunincfi  45541  restuni3  45565  disjf1o  45638  mapss2  45651  difmap  45652  unirnmap  45653  inmap  45654  difmapsn  45657  uzfissfz  45771  iuneqfzuzlem  45779  ssuzfz  45794  iccdificc  45984  iooiinicc  45987  ressiocsup  45999  ressioosup  46000  iooiinioc  46001  ressiooinf  46002  fsumiunss  46020  limciccioolb  46066  limcicciooub  46080  limcresiooub  46085  limsupresxr  46209  liminfresxr  46210  icccncfext  46330  dmvolss  46428  stoweidlem31  46474  stoweidlem39  46482  fourierdlem8  46558  fourierdlem27  46577  fourierdlem38  46588  fourierdlem40  46590  fourierdlem41  46591  fourierdlem46  46595  fourierdlem48  46597  fourierdlem49  46598  fourierdlem51  46600  fourierdlem64  46613  fourierdlem70  46619  fourierdlem71  46620  fourierdlem76  46625  fourierdlem78  46627  fourierdlem79  46628  fourierdlem80  46629  fourierdlem93  46642  fourierdlem97  46646  fourierdlem103  46652  fourierdlem104  46653  salexct  46777  salgencntex  46786  gsumge0cl  46814  sge0fodjrnlem  46859  sge0reuz  46890  iundjiun  46903  icoresmbl  46986  hoidmv1le  47037  hoidmvlelem1  47038  hoidmvlelem3  47040  hoiqssbllem2  47066  hspmbllem2  47070  opnvonmbllem2  47076  iinhoiicc  47117  smfpimbor1lem2  47242  isclatd  49473  setrec1lem2  50178  setrec1lem3  50179