Theorem dfss3 3592

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		dfss2 3591	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		df-ral 2917	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
3	1, 2	bitr4i 267	1 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵)

Syntax hints:   → wi 4   ↔ wb 196  ∀wal 1481   ∈ wcel 1990  ∀wral 2912   ⊆ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-ral 2917  df-in 3581  df-ss 3588

This theorem is referenced by:  ssrab  3680  dfss5  3864  elpwunsn  4224  ssdifsn  4318  eqsn  4361  eqsnOLD  4362  uni0b  4463  uni0c  4464  ssint  4493  ssiinf  4569  sspwuni  4611  dftr3  4756  wefrc  5108  rninxp  5573  wfisg  5715  ordunisssuc  5830  fnres  6007  eqfnfv3  6313  funimass3  6333  ffvresb  6394  tfis  7054  smogt  7464  unifi  8255  unifi2  8256  fissuni  8271  fipreima  8272  cantnf  8590  tz9.12lem3  8652  r1elss  8669  rankval3b  8689  rankonidlem  8691  bndrank  8704  iscard  8801  cfub  9071  cflm  9072  fin1a2s  9236  dcomex  9269  ttukeylem6  9336  unirnfdomd  9389  alephreg  9404  tskord  9602  gruuni  9622  intgru  9636  grudomon  9639  axgroth3  9653  suplem1pr  9874  supexpr  9876  supsr  9933  hashfun  13224  4sqlem19  15667  imasaddfnlem  16188  imasvscafn  16197  setcepi  16738  acsfiindd  17177  sylow2blem3  18037  sylow3lem6  18047  efgval2  18137  iscyggen2  18283  iscyg3  18288  issubdrg  18805  isdomn2  19299  ishil2  20063  rintopn  20714  isbasis2g  20752  tgval2  20760  eltg2b  20763  tgss2  20791  basgen2  20793  bastop1  20797  intcld  20844  unicld  20850  isclo  20891  isclo2  20892  neips  20917  opnnei  20924  neiptopnei  20936  isperf3  20957  ssidcn  21059  ist1-3  21153  cmpcov2  21193  cmpsub  21203  2ndcdisj2  21260  txkgen  21455  xkoinjcn  21490  tgqtop  21515  flimopn  21779  flfnei  21795  tmdcn2  21893  qustgplem  21924  cfil3i  23067  cmetcaulem  23086  ovolfioo  23236  ovolficc  23237  ovolicc2lem4  23288  opnmblALT  23371  xrlimcnp  24695  uvtxanbgr  26292  nbupgruvtxres  26308  cplgruvtxb  26311  vdiscusgrb  26426  ubthlem1  27726  hasheuni  30147  dmvlsiga  30192  ispisys2  30216  omssubadd  30362  eulerpartlemr  30436  eulerpartlemn  30443  cvmlift2lem1  31284  cvmlift2lem12  31296  mclsax  31466  setinds  31683  tfisg  31716  frinsg  31742  isfne4  32335  isfne2  32337  isfne3  32338  neibastop2lem  32355  filnetlem4  32376  fin2so  33396  poimirlem24  33433  poimirlem27  33436  nninfnub  33547  unichnidl  33830  ispridl2  33837  n0elqs  34098  pmapglb  35056  hdmapoc  37223  isnacs2  37269  setindtrs  37592  dford3lem2  37594  dford3  37595  ntrneicls00  38387  ntrneixb  38393  ntrneik3  38394  ntrneix3  38395  ntrneik13  38396  ntrneix13  38397  pwssfi  39211  ssdf  39247  ballss3  39270  iunincfi  39272  restuni3  39301  iinssiin  39312  disjf1o  39378  mapss2  39397  difmap  39399  unirnmap  39400  inmap  39401  difmapsn  39404  unirnmapsn  39406  iunmapsn  39409  uzfissfz  39542  iuneqfzuzlem  39550  ssuzfz  39565  iccdificc  39766  iooiinicc  39769  ressiocsup  39781  ressioosup  39782  iooiinioc  39783  ressiooinf  39784  fsumiunss  39807  limciccioolb  39853  limcicciooub  39869  limcresiooub  39874  limsupresxr  39998  liminfresxr  39999  icccncfext  40100  dmvolss  40202  stoweidlem31  40248  stoweidlem39  40256  fourierdlem8  40332  fourierdlem27  40351  fourierdlem38  40362  fourierdlem40  40364  fourierdlem41  40365  fourierdlem46  40369  fourierdlem48  40371  fourierdlem49  40372  fourierdlem51  40374  fourierdlem53  40376  fourierdlem64  40387  fourierdlem70  40393  fourierdlem71  40394  fourierdlem76  40399  fourierdlem78  40401  fourierdlem79  40402  fourierdlem80  40403  fourierdlem93  40416  fourierdlem97  40420  fourierdlem103  40426  fourierdlem104  40427  rrxbasefi  40503  qndenserrn  40519  intsaluni  40547  salexct  40552  salgencntex  40561  gsumge0cl  40588  sge0fodjrnlem  40633  sge0reuz  40664  iundjiun  40677  meadjiunlem  40682  icoresmbl  40757  hoicvr  40762  hoidmv1le  40808  hoidmvlelem1  40809  hoidmvlelem3  40811  hoiqssbllem2  40837  hspmbllem2  40841  opnvonmbllem2  40847  iinhoiicc  40888  iunhoiioo  40890  smfpimbor1lem2  41006  setrec1lem2  42435  setrec1lem3  42436