Theorem dfss3 3924

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540   ∈ wcel 2114  ∀wral 3052   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-ral 3053  df-ss 3920

This theorem is referenced by:  ssrab  4025  dfss5  4229  elpwunsn  4643  eqsn  4787  uni0b  4891  uni0c  4892  ssint  4921  ssiinf  5012  sspwuni  5057  dftr3  5212  wefrc  5626  rninxp  6145  frpoinsg  6309  ordunisssuc  6433  fnres  6627  eqfnfv3  6987  funimass3  7008  ffvresb  7080  tfisg  7806  tfis  7807  smogt  8309  cofonr  8612  naddrid  8621  pwssfi  9113  unifi  9256  unifi2  9257  fissuni  9269  fipreima  9270  cantnf  9614  setinds  9670  frinsg  9675  tz9.12lem3  9713  r1elss  9730  rankval3b  9750  rankonidlem  9752  bndrank  9765  iscard  9899  cfub  10171  cflm  10172  fin1a2s  10336  dcomex  10369  ttukeylem6  10436  unirnfdomd  10490  alephreg  10505  tskord  10703  gruuni  10723  intgru  10737  grudomon  10740  axgroth3  10754  suplem1pr  10975  supexpr  10977  supsr  11035  hashfun  14372  4sqlem19  16903  imasaddfnlem  17461  imasvscafn  17470  setcepi  18024  acsfiindd  18488  sylow2blem3  19563  sylow3lem6  19573  efgval2  19665  iscyggen2  19822  iscyg3  19827  isdomn2  20656  isdomn2OLD  20657  issubdrg  20725  ishil2  21686  rintopn  22865  isbasis2g  22904  tgval2  22912  eltg2b  22915  tgss2  22943  basgen2  22945  bastop1  22949  intcld  22996  unicld  23002  isclo  23043  isclo2  23044  neips  23069  opnnei  23076  neiptopnei  23088  isperf3  23109  ssidcn  23211  ist1-3  23305  cmpcov2  23346  cmpsub  23356  2ndcdisj2  23413  txkgen  23608  xkoinjcn  23643  tgqtop  23668  flimopn  23931  flfnei  23947  tmdcn2  24045  qustgplem  24077  cfil3i  25237  cmetcaulem  25256  ovolfioo  25436  ovolficc  25437  ovolicc2lem4  25489  opnmblALT  25572  xrlimcnp  26946  madebdayim  27896  oldfib  28385  uvtxnbgrss  29477  iscplgr  29500  vdiscusgrb  29616  ubthlem1  30958  isdrng4  33389  prmidl2  33534  hasheuni  34263  dmvlsiga  34307  ispisys2  34331  omssubadd  34478  eulerpartlemr  34552  eulerpartlemn  34559  cvmlift2lem1  35518  cvmlift2lem12  35530  mclsax  35785  isfne4  36556  isfne2  36558  isfne3  36559  neibastop2lem  36576  filnetlem4  36597  fvineqsneq  37667  fin2so  37858  poimirlem24  37895  poimirlem27  37898  nninfnub  38002  unichnidl  38282  ispridl2  38289  n0elqs  38583  ssdmral  38630  pmapglb  40146  hdmapoc  42307  isnacs2  43063  setindtrs  43382  dford3lem2  43384  dford3  43385  ssunib  43577  ntrneicls00  44445  ntrneixb  44451  ntrneik3  44452  ntrneix3  44453  ntrneik13  44454  ntrneix13  44455  trfr  45318  ssabso  45330  ssdf  45435  ballss3  45452  iunincfi  45453  restuni3  45477  disjf1o  45550  mapss2  45563  difmap  45565  unirnmap  45566  inmap  45567  difmapsn  45570  uzfissfz  45685  iuneqfzuzlem  45693  ssuzfz  45708  iccdificc  45899  iooiinicc  45902  ressiocsup  45914  ressioosup  45915  iooiinioc  45916  ressiooinf  45917  fsumiunss  45935  limciccioolb  45981  limcicciooub  45995  limcresiooub  46000  limsupresxr  46124  liminfresxr  46125  icccncfext  46245  dmvolss  46343  stoweidlem31  46389  stoweidlem39  46397  fourierdlem8  46473  fourierdlem27  46492  fourierdlem38  46503  fourierdlem40  46505  fourierdlem41  46506  fourierdlem46  46510  fourierdlem48  46512  fourierdlem49  46513  fourierdlem51  46515  fourierdlem64  46528  fourierdlem70  46534  fourierdlem71  46535  fourierdlem76  46540  fourierdlem78  46542  fourierdlem79  46543  fourierdlem80  46544  fourierdlem93  46557  fourierdlem97  46561  fourierdlem103  46567  fourierdlem104  46568  salexct  46692  salgencntex  46701  gsumge0cl  46729  sge0fodjrnlem  46774  sge0reuz  46805  iundjiun  46818  icoresmbl  46901  hoicvr  46906  hoidmv1le  46952  hoidmvlelem1  46953  hoidmvlelem3  46955  hoiqssbllem2  46981  hspmbllem2  46985  opnvonmbllem2  46991  iinhoiicc  47032  smfpimbor1lem2  47157  isclatd  49342  setrec1lem2  50047  setrec1lem3  50048