Theorem dfss3 3914

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1537   ∈ wcel 2104  ∀wral 3062   ⊆ wss 3892

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3063  df-v 3439  df-in 3899  df-ss 3909

This theorem is referenced by:  ssrab  4012  dfss5  4204  elpwunsn  4623  eqsn  4768  uni0b  4873  uni0c  4874  ssint  4902  ssiinf  4991  sspwuni  5036  dftr3  5204  wefrc  5594  rninxp  6097  frpoinsg  6261  wfisgOLD  6272  ordunisssuc  6385  fnres  6590  eqfnfv3  6943  funimass3  6963  ffvresb  7030  tfis  7733  smogt  8229  unifi  9152  unifi2  9153  fissuni  9168  fipreima  9169  cantnf  9495  frinsg  9553  tz9.12lem3  9591  r1elss  9608  rankval3b  9628  rankonidlem  9630  bndrank  9643  iscard  9777  cfub  10051  cflm  10052  fin1a2s  10216  dcomex  10249  ttukeylem6  10316  unirnfdomd  10369  alephreg  10384  tskord  10582  gruuni  10602  intgru  10616  grudomon  10619  axgroth3  10633  suplem1pr  10854  supexpr  10856  supsr  10914  hashfun  14197  4sqlem19  16709  imasaddfnlem  17284  imasvscafn  17293  setcepi  17848  acsfiindd  18316  sylow2blem3  19272  sylow3lem6  19282  efgval2  19375  iscyggen2  19526  iscyg3  19531  issubdrg  20094  isdomn2  20615  ishil2  20971  rintopn  22103  isbasis2g  22143  tgval2  22151  eltg2b  22154  tgss2  22182  basgen2  22184  bastop1  22188  intcld  22236  unicld  22242  isclo  22283  isclo2  22284  neips  22309  opnnei  22316  neiptopnei  22328  isperf3  22349  ssidcn  22451  ist1-3  22545  cmpcov2  22586  cmpsub  22596  2ndcdisj2  22653  txkgen  22848  xkoinjcn  22883  tgqtop  22908  flimopn  23171  flfnei  23187  tmdcn2  23285  qustgplem  23317  cfil3i  24478  cmetcaulem  24497  ovolfioo  24676  ovolficc  24677  ovolicc2lem4  24729  opnmblALT  24812  xrlimcnp  26163  uvtxnbgrss  27804  iscplgr  27827  vdiscusgrb  27942  ubthlem1  29277  prmidl2  31661  hasheuni  32098  dmvlsiga  32142  ispisys2  32166  omssubadd  32312  eulerpartlemr  32386  eulerpartlemn  32393  cvmlift2lem1  33309  cvmlift2lem12  33321  mclsax  33576  setinds  33799  tfisg  33831  naddid1  33881  madebdayim  34115  isfne4  34574  isfne2  34576  isfne3  34577  neibastop2lem  34594  filnetlem4  34615  fvineqsneq  35627  fin2so  35808  poimirlem24  35845  poimirlem27  35848  nninfnub  35953  unichnidl  36233  ispridl2  36240  n0elqs  36503  pmapglb  37826  hdmapoc  39987  isnacs2  40565  setindtrs  40885  dford3lem2  40887  dford3  40888  ntrneicls00  41737  ntrneixb  41743  ntrneik3  41744  ntrneix3  41745  ntrneik13  41746  ntrneix13  41747  pwssfi  42631  ssdf  42663  ballss3  42681  iunincfi  42682  restuni3  42705  disjf1o  42773  mapss2  42789  difmap  42791  unirnmap  42792  inmap  42793  difmapsn  42796  uzfissfz  42913  iuneqfzuzlem  42921  ssuzfz  42936  iccdificc  43126  iooiinicc  43129  ressiocsup  43141  ressioosup  43142  iooiinioc  43143  ressiooinf  43144  fsumiunss  43165  limciccioolb  43211  limcicciooub  43227  limcresiooub  43232  limsupresxr  43356  liminfresxr  43357  icccncfext  43477  dmvolss  43575  stoweidlem31  43621  stoweidlem39  43629  fourierdlem8  43705  fourierdlem27  43724  fourierdlem38  43735  fourierdlem40  43737  fourierdlem41  43738  fourierdlem46  43742  fourierdlem48  43744  fourierdlem49  43745  fourierdlem51  43747  fourierdlem64  43760  fourierdlem70  43766  fourierdlem71  43767  fourierdlem76  43772  fourierdlem78  43774  fourierdlem79  43775  fourierdlem80  43776  fourierdlem93  43789  fourierdlem97  43793  fourierdlem103  43799  fourierdlem104  43800  salexct  43922  salgencntex  43931  gsumge0cl  43959  sge0fodjrnlem  44004  sge0reuz  44035  iundjiun  44048  icoresmbl  44131  hoicvr  44136  hoidmv1le  44182  hoidmvlelem1  44183  hoidmvlelem3  44185  hoiqssbllem2  44211  hspmbllem2  44215  opnvonmbllem2  44221  iinhoiicc  44262  smfpimbor1lem2  44387  isclatd  46327  setrec1lem2  46452  setrec1lem3  46453