Theorem dfss3 3919

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1539   ∈ wcel 2113  ∀wral 3048   ⊆ wss 3898

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 3049  df-ss 3915

This theorem is referenced by:  ssrab  4020  dfss5  4224  elpwunsn  4638  eqsn  4782  uni0b  4886  uni0c  4887  ssint  4916  ssiinf  5007  sspwuni  5052  dftr3  5207  wefrc  5615  rninxp  6134  frpoinsg  6298  ordunisssuc  6422  fnres  6616  eqfnfv3  6975  funimass3  6996  ffvresb  7067  tfisg  7793  tfis  7794  smogt  8296  cofonr  8598  naddrid  8607  pwssfi  9097  unifi  9239  unifi2  9240  fissuni  9252  fipreima  9253  cantnf  9594  setinds  9650  frinsg  9655  tz9.12lem3  9693  r1elss  9710  rankval3b  9730  rankonidlem  9732  bndrank  9745  iscard  9879  cfub  10151  cflm  10152  fin1a2s  10316  dcomex  10349  ttukeylem6  10416  unirnfdomd  10469  alephreg  10484  tskord  10682  gruuni  10702  intgru  10716  grudomon  10719  axgroth3  10733  suplem1pr  10954  supexpr  10956  supsr  11014  hashfun  14351  4sqlem19  16882  imasaddfnlem  17440  imasvscafn  17449  setcepi  18003  acsfiindd  18467  sylow2blem3  19542  sylow3lem6  19552  efgval2  19644  iscyggen2  19801  iscyg3  19806  isdomn2  20635  isdomn2OLD  20636  issubdrg  20704  ishil2  21665  rintopn  22844  isbasis2g  22883  tgval2  22891  eltg2b  22894  tgss2  22922  basgen2  22924  bastop1  22928  intcld  22975  unicld  22981  isclo  23022  isclo2  23023  neips  23048  opnnei  23055  neiptopnei  23067  isperf3  23088  ssidcn  23190  ist1-3  23284  cmpcov2  23325  cmpsub  23335  2ndcdisj2  23392  txkgen  23587  xkoinjcn  23622  tgqtop  23647  flimopn  23910  flfnei  23926  tmdcn2  24024  qustgplem  24056  cfil3i  25216  cmetcaulem  25235  ovolfioo  25415  ovolficc  25416  ovolicc2lem4  25468  opnmblALT  25551  xrlimcnp  26925  madebdayim  27853  uvtxnbgrss  29391  iscplgr  29414  vdiscusgrb  29530  ubthlem1  30871  isdrng4  33305  prmidl2  33450  hasheuni  34170  dmvlsiga  34214  ispisys2  34238  omssubadd  34385  eulerpartlemr  34459  eulerpartlemn  34466  cvmlift2lem1  35418  cvmlift2lem12  35430  mclsax  35685  isfne4  36456  isfne2  36458  isfne3  36459  neibastop2lem  36476  filnetlem4  36497  fvineqsneq  37529  fin2so  37720  poimirlem24  37757  poimirlem27  37760  nninfnub  37864  unichnidl  38144  ispridl2  38151  n0elqs  38437  ssdmral  38476  pmapglb  39942  hdmapoc  42103  isnacs2  42863  setindtrs  43182  dford3lem2  43184  dford3  43185  ssunib  43377  ntrneicls00  44246  ntrneixb  44252  ntrneik3  44253  ntrneix3  44254  ntrneik13  44255  ntrneix13  44256  trfr  45119  ssabso  45131  ssdf  45236  ballss3  45253  iunincfi  45254  restuni3  45278  disjf1o  45351  mapss2  45365  difmap  45367  unirnmap  45368  inmap  45369  difmapsn  45372  uzfissfz  45487  iuneqfzuzlem  45495  ssuzfz  45510  iccdificc  45701  iooiinicc  45704  ressiocsup  45716  ressioosup  45717  iooiinioc  45718  ressiooinf  45719  fsumiunss  45737  limciccioolb  45783  limcicciooub  45797  limcresiooub  45802  limsupresxr  45926  liminfresxr  45927  icccncfext  46047  dmvolss  46145  stoweidlem31  46191  stoweidlem39  46199  fourierdlem8  46275  fourierdlem27  46294  fourierdlem38  46305  fourierdlem40  46307  fourierdlem41  46308  fourierdlem46  46312  fourierdlem48  46314  fourierdlem49  46315  fourierdlem51  46317  fourierdlem64  46330  fourierdlem70  46336  fourierdlem71  46337  fourierdlem76  46342  fourierdlem78  46344  fourierdlem79  46345  fourierdlem80  46346  fourierdlem93  46359  fourierdlem97  46363  fourierdlem103  46369  fourierdlem104  46370  salexct  46494  salgencntex  46503  gsumge0cl  46531  sge0fodjrnlem  46576  sge0reuz  46607  iundjiun  46620  icoresmbl  46703  hoicvr  46708  hoidmv1le  46754  hoidmvlelem1  46755  hoidmvlelem3  46757  hoiqssbllem2  46783  hspmbllem2  46787  opnvonmbllem2  46793  iinhoiicc  46834  smfpimbor1lem2  46959  isclatd  49144  setrec1lem2  49849  setrec1lem3  49850