Theorem dfss3 3923

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568   ∈ wcel 2145  ∀wral 3078   ⊆ wss 3902

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 3079  df-ss 3919

This theorem is used by:  ssrab  4022  dfss5  4224  elpwunsn  4648  eqsn  4793  uni0b  4897  uni0c  4898  ssint  4927  ssiinf  5017  sspwuni  5064  dftr3  5221  wefrc  5653  rninxp  6176  frpoinsg  6345  ordunisssuc  6470  fnres  6663  eqfnfv3  7028  funimass3  7050  ffvresb  7123  tfisg  7854  tfis  7855  smogt  8360  cofonr  8666  naddrid  8676  pwssfi  9175  unifi  9315  unifi2  9316  fissuni  9328  fipreima  9329  cantnf  9676  setinds  9732  frinsg  9737  tz9.12lem3  9775  r1elss  9792  rankval3b  9812  rankonidlem  9814  bndrank  9827  iscard  9984  cfub  10254  cflm  10255  fin1a2s  10420  dcomex  10453  ttukeylem6  10520  unirnfdomd  10580  alephreg  10595  tskord  10793  gruuni  10813  intgru  10827  grudomon  10830  axgroth3  10844  suplem1pr  11065  supexpr  11067  supsr  11125  hashfun  14506  4sqlem19  17061  imasaddfnlem  17620  imasvscafn  17629  setcepi  18183  acsfiindd  18647  sylow2blem3  19755  sylow3lem6  19765  efgval2  19857  iscyggen2  20014  iscyg3  20019  isdomn2  20879  isdrng4  20908  issubdrg  20952  unichnlidl  21431  prmidl2  21535  ishil2  21938  rintopn  23140  isbasis2g  23179  tgval2  23187  eltg2b  23190  tgss2  23218  basgen2  23220  bastop1  23224  intcld  23271  unicld  23277  isclo  23318  isclo2  23319  neips  23344  opnnei  23351  neiptopnei  23363  isperf3  23384  ssidcn  23486  ist1-3  23580  cmpcov2  23621  cmpsub  23631  2ndcdisj2  23689  txkgen  23884  xkoinjcn  23919  tgqtop  23944  flimopn  24207  flfnei  24223  tmdcn2  24321  qustgplem  24353  cfil3i  25503  cmetcaulem  25522  ovolfioo  25701  ovolficc  25702  ovolicc2lem4  25754  opnmblALT  25837  xrlimcnp  27213  madebdayim  28161  oldfib  28650  uvtxnbgrss  29860  iscplgr  29883  vdiscusgrb  29998  ubthlem1  31359  hasheuni  34603  dmvlsiga  34647  ispisys2  34672  omssubadd  34819  eulerpartlemr  34893  eulerpartlemn  34900  cvmlift2lem1  35889  cvmlift2lem12  35901  mclsax  36156  dffr5  36341  dffr7  36543  nmulrid  36785  isfne4  36967  isfne2  36969  isfne3  36970  neibastop2lem  36987  filnetlem4  37008  fvineqsneq  38174  fin2so  38369  poimirlem24  38401  poimirlem27  38404  nninfnub  38509  unichnidl  38789  ispridl2  38796  n0elqs  39088  ssdmral  39135  pmapglb  40651  hdmapoc  42812  isnacs2  43559  setindtrs  43874  dford3lem2  43876  dford3  43877  ssunib  44069  ntrneicls00  44937  ntrneixb  44943  ntrneik3  44944  ntrneix3  44945  ntrneik13  44946  ntrneix13  44947  trfr  45793  ssabso  45805  ssdf  45917  ballss3  45933  iunincfi  45934  restuni3  45958  disjf1o  46031  mapss2  46044  difmap  46045  unirnmap  46046  inmap  46047  difmapsn  46050  uzfissfz  46164  iuneqfzuzlem  46172  ssuzfz  46187  iccdificc  46377  iooiinicc  46380  ressiocsup  46392  ressioosup  46393  iooiinioc  46394  ressiooinf  46395  fsumiunss  46413  limciccioolb  46459  limcicciooub  46473  limcresiooub  46478  limsupresxr  46602  liminfresxr  46603  icccncfext  46723  dmvolss  46821  stoweidlem31  46867  stoweidlem39  46875  fourierdlem8  46951  fourierdlem27  46970  fourierdlem38  46981  fourierdlem40  46983  fourierdlem41  46984  fourierdlem46  46988  fourierdlem51  46993  fourierdlem64  47006  fourierdlem70  47012  fourierdlem71  47013  fourierdlem76  47018  fourierdlem78  47020  fourierdlem79  47021  fourierdlem80  47022  fourierdlem93  47035  fourierdlem97  47039  fourierdlem103  47045  fourierdlem104  47046  salexct  47170  salgencntex  47179  gsumge0cl  47207  sge0fodjrnlem  47252  sge0reuz  47283  iundjiun  47296  icoresmbl  47379  hoidmv1le  47430  hoidmvlelem1  47431  hoidmvlelem3  47433  hoiqssbllem2  47459  hspmbllem2  47463  opnvonmbllem2  47469  iinhoiicc  47510  smfpimbor1lem2  47635  isclatd  49917  setrec1lem2  50622  setrec1lem3  50623