Theorem dfss3 3884

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

Syntax hints:   → wi 4   ↔ wb 207  ∀wal 1523   ∈ wcel 2083  ∀wral 3107   ⊆ wss 3865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-ral 3112  df-in 3872  df-ss 3880

This theorem is referenced by:  ssrab  3976  dfss5  4167  elpwunsn  4534  eqsn  4675  uni0b  4776  uni0c  4777  ssint  4804  ssiinf  4883  sspwuni  4927  dftr3  5074  wefrc  5444  rninxp  5919  wfisg  6065  ordunisssuc  6175  fnres  6351  eqfnfv3  6676  funimass3  6696  ffvresb  6758  tfis  7432  smogt  7863  unifi  8666  unifi2  8667  fissuni  8682  fipreima  8683  cantnf  9009  tz9.12lem3  9071  r1elss  9088  rankval3b  9108  rankonidlem  9110  bndrank  9123  iscard  9257  cfub  9524  cflm  9525  fin1a2s  9689  dcomex  9722  ttukeylem6  9789  unirnfdomd  9842  alephreg  9857  tskord  10055  gruuni  10075  intgru  10089  grudomon  10092  axgroth3  10106  suplem1pr  10327  supexpr  10329  supsr  10387  hashfun  13650  4sqlem19  16132  imasaddfnlem  16634  imasvscafn  16643  setcepi  17181  acsfiindd  17620  sylow2blem3  18481  sylow3lem6  18491  efgval2  18581  iscyggen2  18727  iscyg3  18732  issubdrg  19254  isdomn2  19765  ishil2  20549  rintopn  21205  isbasis2g  21244  tgval2  21252  eltg2b  21255  tgss2  21283  basgen2  21285  bastop1  21289  intcld  21336  unicld  21342  isclo  21383  isclo2  21384  neips  21409  opnnei  21416  neiptopnei  21428  isperf3  21449  ssidcn  21551  ist1-3  21645  cmpcov2  21686  cmpsub  21696  2ndcdisj2  21753  txkgen  21948  xkoinjcn  21983  tgqtop  22008  flimopn  22271  flfnei  22287  tmdcn2  22385  qustgplem  22416  cfil3i  23559  cmetcaulem  23578  ovolfioo  23755  ovolficc  23756  ovolicc2lem4  23808  opnmblALT  23891  xrlimcnp  25232  uvtxnbgrss  26861  iscplgr  26884  vdiscusgrb  26999  ubthlem1  28334  hasheuni  30957  dmvlsiga  31001  ispisys2  31025  omssubadd  31171  eulerpartlemr  31245  eulerpartlemn  31252  cvmlift2lem1  32159  cvmlift2lem12  32171  mclsax  32426  setinds  32633  tfisg  32666  frpoinsg  32692  frinsg  32698  isfne4  33299  isfne2  33301  isfne3  33302  neibastop2lem  33319  filnetlem4  33340  fvineqsneq  34245  fin2so  34431  poimirlem24  34468  poimirlem27  34471  nninfnub  34579  unichnidl  34862  ispridl2  34869  n0elqs  35136  pmapglb  36458  hdmapoc  38619  isnacs2  38809  setindtrs  39128  dford3lem2  39130  dford3  39131  ntrneicls00  39945  ntrneixb  39951  ntrneik3  39952  ntrneix3  39953  ntrneik13  39954  ntrneix13  39955  pwssfi  40867  ssdf  40899  ballss3  40919  iunincfi  40920  restuni3  40945  disjf1o  41013  mapss2  41029  difmap  41031  unirnmap  41032  inmap  41033  difmapsn  41036  uzfissfz  41156  iuneqfzuzlem  41164  ssuzfz  41179  iccdificc  41378  iooiinicc  41381  ressiocsup  41393  ressioosup  41394  iooiinioc  41395  ressiooinf  41396  fsumiunss  41419  limciccioolb  41465  limcicciooub  41481  limcresiooub  41486  limsupresxr  41610  liminfresxr  41611  icccncfext  41733  dmvolss  41834  stoweidlem31  41880  stoweidlem39  41888  fourierdlem8  41964  fourierdlem27  41983  fourierdlem38  41994  fourierdlem40  41996  fourierdlem41  41997  fourierdlem46  42001  fourierdlem48  42003  fourierdlem49  42004  fourierdlem51  42006  fourierdlem53  42008  fourierdlem64  42019  fourierdlem70  42025  fourierdlem71  42026  fourierdlem76  42031  fourierdlem78  42033  fourierdlem79  42034  fourierdlem80  42035  fourierdlem93  42048  fourierdlem97  42052  fourierdlem103  42058  fourierdlem104  42059  salexct  42181  salgencntex  42190  gsumge0cl  42217  sge0fodjrnlem  42262  sge0reuz  42293  iundjiun  42306  icoresmbl  42389  hoicvr  42394  hoidmv1le  42440  hoidmvlelem1  42441  hoidmvlelem3  42443  hoiqssbllem2  42469  hspmbllem2  42473  opnvonmbllem2  42479  iinhoiicc  42520  smfpimbor1lem2  42638  setrec1lem2  44293  setrec1lem3  44294