Theorem dfss3 3911

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540   ∈ wcel 2114  ∀wral 3052   ⊆ wss 3890

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 3053  df-ss 3907

This theorem is referenced by:  ssrab  4012  dfss5  4216  elpwunsn  4629  eqsn  4773  uni0b  4877  uni0c  4878  ssint  4907  ssiinf  4998  sspwuni  5043  dftr3  5198  wefrc  5618  rninxp  6137  frpoinsg  6301  ordunisssuc  6425  fnres  6619  eqfnfv3  6979  funimass3  7000  ffvresb  7072  tfisg  7798  tfis  7799  smogt  8300  cofonr  8603  naddrid  8612  pwssfi  9104  unifi  9247  unifi2  9248  fissuni  9260  fipreima  9261  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  20679  isdomn2OLD  20680  issubdrg  20748  ishil2  21709  rintopn  22884  isbasis2g  22923  tgval2  22931  eltg2b  22934  tgss2  22962  basgen2  22964  bastop1  22968  intcld  23015  unicld  23021  isclo  23062  isclo2  23063  neips  23088  opnnei  23095  neiptopnei  23107  isperf3  23128  ssidcn  23230  ist1-3  23324  cmpcov2  23365  cmpsub  23375  2ndcdisj2  23432  txkgen  23627  xkoinjcn  23662  tgqtop  23687  flimopn  23950  flfnei  23966  tmdcn2  24064  qustgplem  24096  cfil3i  25246  cmetcaulem  25265  ovolfioo  25444  ovolficc  25445  ovolicc2lem4  25497  opnmblALT  25580  xrlimcnp  26945  madebdayim  27894  oldfib  28383  uvtxnbgrss  29475  iscplgr  29498  vdiscusgrb  29614  ubthlem1  30956  isdrng4  33371  prmidl2  33516  hasheuni  34245  dmvlsiga  34289  ispisys2  34313  omssubadd  34460  eulerpartlemr  34534  eulerpartlemn  34541  cvmlift2lem1  35500  cvmlift2lem12  35512  mclsax  35767  isfne4  36538  isfne2  36540  isfne3  36541  neibastop2lem  36558  filnetlem4  36579  fvineqsneq  37742  fin2so  37942  poimirlem24  37979  poimirlem27  37982  nninfnub  38086  unichnidl  38366  ispridl2  38373  n0elqs  38667  ssdmral  38714  pmapglb  40230  hdmapoc  42391  isnacs2  43152  setindtrs  43471  dford3lem2  43473  dford3  43474  ssunib  43666  ntrneicls00  44534  ntrneixb  44540  ntrneik3  44541  ntrneix3  44542  ntrneik13  44543  ntrneix13  44544  trfr  45407  ssabso  45419  ssdf  45524  ballss3  45541  iunincfi  45542  restuni3  45566  disjf1o  45639  mapss2  45652  difmap  45654  unirnmap  45655  inmap  45656  difmapsn  45659  uzfissfz  45774  iuneqfzuzlem  45782  ssuzfz  45797  iccdificc  45987  iooiinicc  45990  ressiocsup  46002  ressioosup  46003  iooiinioc  46004  ressiooinf  46005  fsumiunss  46023  limciccioolb  46069  limcicciooub  46083  limcresiooub  46088  limsupresxr  46212  liminfresxr  46213  icccncfext  46333  dmvolss  46431  stoweidlem31  46477  stoweidlem39  46485  fourierdlem8  46561  fourierdlem27  46580  fourierdlem38  46591  fourierdlem40  46593  fourierdlem41  46594  fourierdlem46  46598  fourierdlem48  46600  fourierdlem49  46601  fourierdlem51  46603  fourierdlem64  46616  fourierdlem70  46622  fourierdlem71  46623  fourierdlem76  46628  fourierdlem78  46630  fourierdlem79  46631  fourierdlem80  46632  fourierdlem93  46645  fourierdlem97  46649  fourierdlem103  46655  fourierdlem104  46656  salexct  46780  salgencntex  46789  gsumge0cl  46817  sge0fodjrnlem  46862  sge0reuz  46893  iundjiun  46906  icoresmbl  46989  hoidmv1le  47040  hoidmvlelem1  47041  hoidmvlelem3  47043  hoiqssbllem2  47069  hspmbllem2  47073  opnvonmbllem2  47079  iinhoiicc  47120  smfpimbor1lem2  47245  isclatd  49470  setrec1lem2  50175  setrec1lem3  50176