Theorem dfss3 3897

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1567   ∈ wcel 2144  ∀wral 3076   ⊆ wss 3895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ral 3077  df-ss 3896

This theorem is used by:  ssrab  3996  dfss5  4220  elpwunsn  4641  eqsn  4784  uni0b  4893  uni0c  4894  ssint  4923  ssiinf  5012  sspwuni  5059  dftr3  5216  wefrc  5644  rninxp  6170  frpoinsg  6346  ordunisssuc  6471  fnres  6667  eqfnfv3  7032  funimass3  7054  ffvresb  7127  tfisg  7866  tfis  7867  smogt  8379  cofonr  8687  naddrid  8697  pwssfi  9196  unifi  9337  unifi2  9338  fissuni  9350  fipreima  9351  cantnf  9698  setinds  9754  frinsg  9759  tz9.12lem3  9800  r1elss  9818  rankval3b  9840  rankonidlem  9842  bndrank  9858  elhf3  9917  setrec1lem2  9971  setrec1lem3  9973  iscard  10060  cfub  10330  cflm  10331  fin1a2s  10496  dcomex  10529  ttukeylem6  10596  unirnfdomd  10656  alephreg  10671  tskord  10869  gruuni  10889  intgru  10903  grudomon  10906  axgroth3  10920  suplem1pr  11141  supexpr  11143  supsr  11201  hashfun  14586  4sqlem19  17147  imasaddfnlem  17706  imasvscafn  17715  setcepi  18269  acsfiindd  18733  sylow2blem3  19842  sylow3lem6  19852  efgval2  19944  iscyggen2  20101  iscyg3  20106  isdomn2  20969  isdrng4  20998  issubdrg  21043  unichnlidl  21522  prmidl2  21628  ishil2  22031  rintopn  23233  isbasis2g  23272  tgval2  23280  eltg2b  23283  tgss2  23311  basgen2  23313  bastop1  23317  intcld  23364  unicld  23370  isclo  23411  isclo2  23412  neips  23437  opnnei  23444  neiptopnei  23456  isperf3  23477  ssidcn  23579  ist1-3  23673  cmpcov2  23714  cmpsub  23724  2ndcdisj2  23782  txkgen  23977  xkoinjcn  24012  tgqtop  24037  flimopn  24300  flfnei  24316  tmdcn2  24414  qustgplem  24446  cfil3i  25596  cmetcaulem  25615  ovolfioo  25794  ovolficc  25795  ovolicc2lem4  25847  opnmblALT  25930  xrlimcnp  27302  madebdayim  28280  oldfib  28769  uvtxnbgrss  29979  iscplgr  30002  vdiscusgrb  30117  ubthlem1  31478  hasheuni  34764  dmvlsiga  34808  ispisys2  34833  omssubadd  34979  eulerpartlemr  35053  eulerpartlemn  35060  cvmlift2lem1  36154  cvmlift2lem12  36166  mclsax  36421  dffr5  36612  dffr7  36813  nmulrid  37039  isfne4  37221  isfne2  37223  isfne3  37224  neibastop2lem  37241  filnetlem4  37262  fvineqsneq  38429  fin2so  38624  poimirlem24  38656  poimirlem27  38659  nninfnub  38779  unichnidl  39059  ispridl2  39066  n0elqs  39358  ssdmral  39405  pmapglb  40921  hdmapoc  43082  isnacs2  43811  setindtrs  44126  dford3lem2  44128  dford3  44129  ssunib  44316  ntrneicls00  45183  ntrneixb  45189  ntrneik3  45190  ntrneix3  45191  ntrneik13  45192  ntrneix13  45193  trfr  46046  ssabso  46058  ssdf  46186  ballss3  46202  iunincfi  46203  restuni3  46227  disjf1o  46300  mapss2  46313  difmap  46314  unirnmap  46315  inmap  46316  difmapsn  46319  uzfissfz  46432  iuneqfzuzlem  46440  ssuzfz  46455  iccdificc  46645  iooiinicc  46648  ressiocsup  46660  ressioosup  46661  iooiinioc  46662  ressiooinf  46663  fsumiunss  46681  limciccioolb  46727  limcicciooub  46741  limcresiooub  46746  limsupresxr  46870  liminfresxr  46871  icccncfext  46991  dmvolss  47089  stoweidlem31  47135  stoweidlem39  47143  fourierdlem8  47219  fourierdlem27  47238  fourierdlem38  47249  fourierdlem40  47251  fourierdlem41  47252  fourierdlem46  47256  fourierdlem51  47261  fourierdlem64  47274  fourierdlem70  47280  fourierdlem71  47281  fourierdlem76  47286  fourierdlem78  47288  fourierdlem79  47289  fourierdlem80  47290  fourierdlem93  47303  fourierdlem97  47307  fourierdlem103  47313  fourierdlem104  47314  salexct  47438  salgencntex  47447  gsumge0cl  47475  sge0fodjrnlem  47520  sge0reuz  47551  iundjiun  47564  icoresmbl  47647  hoidmv1le  47698  hoidmvlelem1  47699  hoidmvlelem3  47701  hoiqssbllem2  47727  hspmbllem2  47731  opnvonmbllem2  47737  iinhoiicc  47778  smfpimbor1lem2  47903  isclatd  50191