Theorem dfss3 3919

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1538   ∈ wcel 2105  ∀wral 3061   ⊆ wss 3897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3062  df-v 3443  df-in 3904  df-ss 3914

This theorem is referenced by:  ssrab  4017  dfss5  4210  elpwunsn  4630  eqsn  4775  uni0b  4880  uni0c  4881  ssint  4909  ssiinf  4998  sspwuni  5044  dftr3  5212  wefrc  5608  rninxp  6111  frpoinsg  6276  wfisgOLD  6287  ordunisssuc  6400  fnres  6605  eqfnfv3  6961  funimass3  6981  ffvresb  7048  tfisg  7760  tfis  7761  smogt  8260  unifi  9198  unifi2  9199  fissuni  9214  fipreima  9215  cantnf  9542  frinsg  9600  tz9.12lem3  9638  r1elss  9655  rankval3b  9675  rankonidlem  9677  bndrank  9690  iscard  9824  cfub  10098  cflm  10099  fin1a2s  10263  dcomex  10296  ttukeylem6  10363  unirnfdomd  10416  alephreg  10431  tskord  10629  gruuni  10649  intgru  10663  grudomon  10666  axgroth3  10680  suplem1pr  10901  supexpr  10903  supsr  10961  hashfun  14244  4sqlem19  16753  imasaddfnlem  17328  imasvscafn  17337  setcepi  17892  acsfiindd  18360  sylow2blem3  19315  sylow3lem6  19325  efgval2  19417  iscyggen2  19568  iscyg3  19573  issubdrg  20146  isdomn2  20668  ishil2  21024  rintopn  22156  isbasis2g  22196  tgval2  22204  eltg2b  22207  tgss2  22235  basgen2  22237  bastop1  22241  intcld  22289  unicld  22295  isclo  22336  isclo2  22337  neips  22362  opnnei  22369  neiptopnei  22381  isperf3  22402  ssidcn  22504  ist1-3  22598  cmpcov2  22639  cmpsub  22649  2ndcdisj2  22706  txkgen  22901  xkoinjcn  22936  tgqtop  22961  flimopn  23224  flfnei  23240  tmdcn2  23338  qustgplem  23370  cfil3i  24531  cmetcaulem  24550  ovolfioo  24729  ovolficc  24730  ovolicc2lem4  24782  opnmblALT  24865  xrlimcnp  26216  uvtxnbgrss  27989  iscplgr  28012  vdiscusgrb  28127  ubthlem1  29461  prmidl2  31854  hasheuni  32292  dmvlsiga  32336  ispisys2  32360  omssubadd  32508  eulerpartlemr  32582  eulerpartlemn  32589  cvmlift2lem1  33504  cvmlift2lem12  33516  mclsax  33771  setinds  33981  naddid1  34059  madebdayim  34161  isfne4  34620  isfne2  34622  isfne3  34623  neibastop2lem  34640  filnetlem4  34661  fvineqsneq  35681  fin2so  35862  poimirlem24  35899  poimirlem27  35902  nninfnub  36007  unichnidl  36287  ispridl2  36294  n0elqs  36585  pmapglb  38031  hdmapoc  40192  isnacs2  40778  setindtrs  41098  dford3lem2  41100  dford3  41101  ntrneicls00  42009  ntrneixb  42015  ntrneik3  42016  ntrneix3  42017  ntrneik13  42018  ntrneix13  42019  pwssfi  42902  ssdf  42934  ballss3  42952  iunincfi  42953  restuni3  42977  disjf1o  43045  mapss2  43061  difmap  43063  unirnmap  43064  inmap  43065  difmapsn  43068  uzfissfz  43189  iuneqfzuzlem  43197  ssuzfz  43212  iccdificc  43402  iooiinicc  43405  ressiocsup  43417  ressioosup  43418  iooiinioc  43419  ressiooinf  43420  fsumiunss  43441  limciccioolb  43487  limcicciooub  43503  limcresiooub  43508  limsupresxr  43632  liminfresxr  43633  icccncfext  43753  dmvolss  43851  stoweidlem31  43897  stoweidlem39  43905  fourierdlem8  43981  fourierdlem27  44000  fourierdlem38  44011  fourierdlem40  44013  fourierdlem41  44014  fourierdlem46  44018  fourierdlem48  44020  fourierdlem49  44021  fourierdlem51  44023  fourierdlem64  44036  fourierdlem70  44042  fourierdlem71  44043  fourierdlem76  44048  fourierdlem78  44050  fourierdlem79  44051  fourierdlem80  44052  fourierdlem93  44065  fourierdlem97  44069  fourierdlem103  44075  fourierdlem104  44076  salexct  44198  salgencntex  44207  gsumge0cl  44235  sge0fodjrnlem  44280  sge0reuz  44311  iundjiun  44324  icoresmbl  44407  hoicvr  44412  hoidmv1le  44458  hoidmvlelem1  44459  hoidmvlelem3  44461  hoiqssbllem2  44487  hspmbllem2  44491  opnvonmbllem2  44497  iinhoiicc  44538  smfpimbor1lem2  44663  isclatd  46609  setrec1lem2  46734  setrec1lem3  46735