Theorem dfss3 3902

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568   ∈ wcel 2147  ∀wral 3080   ⊆ wss 3900

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 3081  df-ss 3901

This theorem is used by:  ssrab  3999  dfss5  4223  elpwunsn  4645  eqsn  4788  uni0b  4897  uni0c  4898  ssint  4927  ssiinf  5016  sspwuni  5063  dftr3  5221  wefrc  5650  rninxp  6187  frpoinsg  6370  ordunisssuc  6495  fnres  6694  eqfnfv3  7060  funimass3  7082  ffvresb  7156  tfisg  7897  tfis  7898  smogt  8411  cofonr  8719  naddrid  8729  pwssfi  9228  unifi  9369  unifi2  9370  fissuni  9382  fipreima  9383  cantnf  9729  setinds  9785  frinsg  9790  tz9.12lem3  9831  r1elss  9849  rankval3b  9871  rankonidlem  9873  bndrank  9889  elhf3  9948  setrec1lem2  10002  setrec1lem3  10004  iscard  10091  cfub  10363  cflm  10364  fin1a2s  10529  dcomex  10562  ttukeylem6  10629  unirnfdomd  10689  alephreg  10704  tskord  10902  gruuni  10922  intgru  10936  grudomon  10939  axgroth3  10953  suplem1pr  11174  supexpr  11176  supsr  11234  hashfun  14621  4sqlem19  17182  imasaddfnlem  17741  imasvscafn  17750  setcepi  18304  acsfiindd  18768  sylow2blem3  19878  sylow3lem6  19888  efgval2  19980  iscyggen2  20137  iscyg3  20142  isdomn2  21005  isdrng4  21034  issubdrg  21079  unichnlidl  21558  prmidl2  21664  ishil2  22069  rintopn  23271  isbasis2g  23310  tgval2  23318  eltg2b  23321  tgss2  23349  basgen2  23351  bastop1  23355  intcld  23402  unicld  23408  isclo  23449  isclo2  23450  neips  23475  opnnei  23482  neiptopnei  23494  isperf3  23515  ssidcn  23617  ist1-3  23711  cmpcov2  23752  cmpsub  23762  2ndcdisj2  23820  txkgen  24015  xkoinjcn  24050  tgqtop  24075  flimopn  24338  flfnei  24354  tmdcn2  24452  qustgplem  24484  cfil3i  25634  cmetcaulem  25653  ovolfioo  25832  ovolficc  25833  ovolicc2lem4  25885  opnmblALT  25968  xrlimcnp  27342  madebdayim  28320  oldfib  28809  uvtxnbgrss  30019  iscplgr  30042  vdiscusgrb  30157  ubthlem1  31518  hasheuni  34821  dmvlsiga  34865  ispisys2  34890  omssubadd  35036  eulerpartlemr  35110  eulerpartlemn  35117  cvmlift2lem1  36268  cvmlift2lem12  36280  mclsax  36535  dffr5  36727  dffr7  36928  nmulrid  37154  isfne4  37336  isfne2  37338  isfne3  37339  neibastop2lem  37356  filnetlem4  37377  fvineqsneq  38596  fin2so  38791  poimirlem24  38823  poimirlem27  38826  nninfnub  38944  unichnidl  39224  ispridl2  39231  n0elqs  39523  ssdmral  39570  pmapglb  41086  hdmapoc  43247  isnacs2  43977  setindtrs  44292  dford3lem2  44294  dford3  44295  ssunib  44477  ntrneicls00  45344  ntrneixb  45350  ntrneik3  45351  ntrneix3  45352  ntrneik13  45353  ntrneix13  45354  trfr  46210  ssabso  46222  ssdf  46360  ballss3  46375  iunincfi  46376  restuni3  46400  disjf1o  46473  mapss2  46486  difmap  46487  unirnmap  46488  inmap  46489  difmapsn  46492  uzfissfz  46605  iuneqfzuzlem  46613  ssuzfz  46628  iccdificc  46818  iooiinicc  46821  ressiocsup  46833  ressioosup  46834  iooiinioc  46835  ressiooinf  46836  fsumiunss  46854  limciccioolb  46900  limcicciooub  46914  limcresiooub  46919  limsupresxr  47043  liminfresxr  47044  icccncfext  47164  dmvolss  47262  stoweidlem31  47308  stoweidlem39  47316  fourierdlem8  47392  fourierdlem27  47411  fourierdlem38  47422  fourierdlem40  47424  fourierdlem41  47425  fourierdlem46  47429  fourierdlem51  47434  fourierdlem64  47447  fourierdlem70  47453  fourierdlem71  47454  fourierdlem76  47459  fourierdlem78  47461  fourierdlem79  47462  fourierdlem80  47463  fourierdlem93  47476  fourierdlem97  47480  fourierdlem103  47486  fourierdlem104  47487  salexct  47611  salgencntex  47620  gsumge0cl  47648  sge0fodjrnlem  47693  sge0reuz  47724  iundjiun  47737  icoresmbl  47820  hoidmv1le  47871  hoidmvlelem1  47872  hoidmvlelem3  47874  hoiqssbllem2  47900  hspmbllem2  47904  opnvonmbllem2  47910  iinhoiicc  47951  smfpimbor1lem2  48076  isclatd  50422