Theorem dfss3 3926

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

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1568   ∈ wcel 2143  ∀wral 3079   ⊆ wss 3905

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 210  df-ral 3080  df-ss 3922

This theorem is referenced by:  ssrab  4025  dfss5  4228  elpwunsn  4650  eqsn  4795  uni0b  4899  uni0c  4900  ssint  4929  ssiinf  5019  sspwuni  5066  dftr3  5223  wefrc  5655  rninxp  6177  frpoinsg  6344  ordunisssuc  6469  fnres  6662  eqfnfv3  7027  funimass3  7049  ffvresb  7121  tfisg  7846  tfis  7847  smogt  8350  cofonr  8656  naddrid  8666  pwssfi  9157  unifi  9297  unifi2  9298  fissuni  9310  fipreima  9311  cantnf  9658  setinds  9714  frinsg  9719  tz9.12lem3  9757  r1elss  9774  rankval3b  9794  rankonidlem  9796  bndrank  9809  iscard  9957  cfub  10227  cflm  10228  fin1a2s  10393  dcomex  10426  ttukeylem6  10493  unirnfdomd  10547  alephreg  10562  tskord  10760  gruuni  10780  intgru  10794  grudomon  10797  axgroth3  10811  suplem1pr  11032  supexpr  11034  supsr  11092  hashfun  14470  4sqlem19  17018  imasaddfnlem  17577  imasvscafn  17586  setcepi  18140  acsfiindd  18604  sylow2blem3  19687  sylow3lem6  19697  efgval2  19789  iscyggen2  19946  iscyg3  19951  isdomn2  20810  isdrng4  20839  issubdrg  20883  unichnlidl  21362  prmidl2  21466  ishil2  21869  rintopn  23066  isbasis2g  23105  tgval2  23113  eltg2b  23116  tgss2  23144  basgen2  23146  bastop1  23150  intcld  23197  unicld  23203  isclo  23244  isclo2  23245  neips  23270  opnnei  23277  neiptopnei  23289  isperf3  23310  ssidcn  23412  ist1-3  23506  cmpcov2  23547  cmpsub  23557  2ndcdisj2  23614  txkgen  23809  xkoinjcn  23844  tgqtop  23869  flimopn  24132  flfnei  24148  tmdcn2  24246  qustgplem  24278  cfil3i  25428  cmetcaulem  25447  ovolfioo  25626  ovolficc  25627  ovolicc2lem4  25679  opnmblALT  25762  xrlimcnp  27133  madebdayim  28081  oldfib  28570  uvtxnbgrss  29742  iscplgr  29765  vdiscusgrb  29880  ubthlem1  31222  hasheuni  34475  dmvlsiga  34519  ispisys2  34543  omssubadd  34690  eulerpartlemr  34764  eulerpartlemn  34771  cvmlift2lem1  35794  cvmlift2lem12  35806  mclsax  36061  nmulrid  36697  isfne4  36851  isfne2  36853  isfne3  36854  neibastop2lem  36871  filnetlem4  36892  fvineqsneq  38058  fin2so  38258  poimirlem24  38295  poimirlem27  38298  nninfnub  38402  unichnidl  38682  ispridl2  38689  n0elqs  38981  ssdmral  39028  pmapglb  40544  hdmapoc  42705  isnacs2  43437  setindtrs  43752  dford3lem2  43754  dford3  43755  ssunib  43947  ntrneicls00  44815  ntrneixb  44821  ntrneik3  44822  ntrneix3  44823  ntrneik13  44824  ntrneix13  44825  trfr  45671  ssabso  45683  ssdf  45795  ballss3  45811  iunincfi  45812  restuni3  45836  disjf1o  45909  mapss2  45922  difmap  45923  unirnmap  45924  inmap  45925  difmapsn  45928  uzfissfz  46042  iuneqfzuzlem  46050  ssuzfz  46065  iccdificc  46255  iooiinicc  46258  ressiocsup  46270  ressioosup  46271  iooiinioc  46272  ressiooinf  46273  fsumiunss  46291  limciccioolb  46337  limcicciooub  46351  limcresiooub  46356  limsupresxr  46480  liminfresxr  46481  icccncfext  46601  dmvolss  46699  stoweidlem31  46745  stoweidlem39  46753  fourierdlem8  46829  fourierdlem27  46848  fourierdlem38  46859  fourierdlem40  46861  fourierdlem41  46862  fourierdlem46  46866  fourierdlem51  46871  fourierdlem64  46884  fourierdlem70  46890  fourierdlem71  46891  fourierdlem76  46896  fourierdlem78  46898  fourierdlem79  46899  fourierdlem80  46900  fourierdlem93  46913  fourierdlem97  46917  fourierdlem103  46923  fourierdlem104  46924  salexct  47048  salgencntex  47057  gsumge0cl  47085  sge0fodjrnlem  47130  sge0reuz  47161  iundjiun  47174  icoresmbl  47257  hoidmv1le  47308  hoidmvlelem1  47309  hoidmvlelem3  47311  hoiqssbllem2  47337  hspmbllem2  47341  opnvonmbllem2  47347  iinhoiicc  47388  smfpimbor1lem2  47513  isclatd  49761  setrec1lem2  50466  setrec1lem3  50467