Theorem dfss3 3918

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1539   ∈ wcel 2111  ∀wral 3047   ⊆ wss 3897

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 3048  df-ss 3914

This theorem is referenced by:  ssrab  4018  dfss5  4222  elpwunsn  4634  eqsn  4778  uni0b  4882  uni0c  4883  ssint  4912  ssiinf  5001  sspwuni  5046  dftr3  5201  wefrc  5608  rninxp  6126  frpoinsg  6290  ordunisssuc  6414  fnres  6608  eqfnfv3  6966  funimass3  6987  ffvresb  7058  tfisg  7784  tfis  7785  smogt  8287  cofonr  8589  naddrid  8598  pwssfi  9086  unifi  9228  unifi2  9229  fissuni  9241  fipreima  9242  cantnf  9583  setinds  9639  frinsg  9644  tz9.12lem3  9682  r1elss  9699  rankval3b  9719  rankonidlem  9721  bndrank  9734  iscard  9868  cfub  10140  cflm  10141  fin1a2s  10305  dcomex  10338  ttukeylem6  10405  unirnfdomd  10458  alephreg  10473  tskord  10671  gruuni  10691  intgru  10705  grudomon  10708  axgroth3  10722  suplem1pr  10943  supexpr  10945  supsr  11003  hashfun  14344  4sqlem19  16875  imasaddfnlem  17432  imasvscafn  17441  setcepi  17995  acsfiindd  18459  sylow2blem3  19534  sylow3lem6  19544  efgval2  19636  iscyggen2  19793  iscyg3  19798  isdomn2  20626  isdomn2OLD  20627  issubdrg  20695  ishil2  21656  rintopn  22824  isbasis2g  22863  tgval2  22871  eltg2b  22874  tgss2  22902  basgen2  22904  bastop1  22908  intcld  22955  unicld  22961  isclo  23002  isclo2  23003  neips  23028  opnnei  23035  neiptopnei  23047  isperf3  23068  ssidcn  23170  ist1-3  23264  cmpcov2  23305  cmpsub  23315  2ndcdisj2  23372  txkgen  23567  xkoinjcn  23602  tgqtop  23627  flimopn  23890  flfnei  23906  tmdcn2  24004  qustgplem  24036  cfil3i  25196  cmetcaulem  25215  ovolfioo  25395  ovolficc  25396  ovolicc2lem4  25448  opnmblALT  25531  xrlimcnp  26905  madebdayim  27833  uvtxnbgrss  29370  iscplgr  29393  vdiscusgrb  29509  ubthlem1  30850  isdrng4  33261  prmidl2  33406  hasheuni  34098  dmvlsiga  34142  ispisys2  34166  omssubadd  34313  eulerpartlemr  34387  eulerpartlemn  34394  cvmlift2lem1  35346  cvmlift2lem12  35358  mclsax  35613  isfne4  36384  isfne2  36386  isfne3  36387  neibastop2lem  36404  filnetlem4  36425  fvineqsneq  37456  fin2so  37646  poimirlem24  37683  poimirlem27  37686  nninfnub  37790  unichnidl  38070  ispridl2  38077  n0elqs  38363  ssdmral  38402  pmapglb  39868  hdmapoc  42029  isnacs2  42798  setindtrs  43117  dford3lem2  43119  dford3  43120  ssunib  43312  ntrneicls00  44181  ntrneixb  44187  ntrneik3  44188  ntrneix3  44189  ntrneik13  44190  ntrneix13  44191  trfr  45054  ssabso  45066  ssdf  45171  ballss3  45189  iunincfi  45190  restuni3  45214  disjf1o  45287  mapss2  45301  difmap  45303  unirnmap  45304  inmap  45305  difmapsn  45308  uzfissfz  45424  iuneqfzuzlem  45432  ssuzfz  45447  iccdificc  45638  iooiinicc  45641  ressiocsup  45653  ressioosup  45654  iooiinioc  45655  ressiooinf  45656  fsumiunss  45674  limciccioolb  45720  limcicciooub  45734  limcresiooub  45739  limsupresxr  45863  liminfresxr  45864  icccncfext  45984  dmvolss  46082  stoweidlem31  46128  stoweidlem39  46136  fourierdlem8  46212  fourierdlem27  46231  fourierdlem38  46242  fourierdlem40  46244  fourierdlem41  46245  fourierdlem46  46249  fourierdlem48  46251  fourierdlem49  46252  fourierdlem51  46254  fourierdlem64  46267  fourierdlem70  46273  fourierdlem71  46274  fourierdlem76  46279  fourierdlem78  46281  fourierdlem79  46282  fourierdlem80  46283  fourierdlem93  46296  fourierdlem97  46300  fourierdlem103  46306  fourierdlem104  46307  salexct  46431  salgencntex  46440  gsumge0cl  46468  sge0fodjrnlem  46513  sge0reuz  46544  iundjiun  46557  icoresmbl  46640  hoicvr  46645  hoidmv1le  46691  hoidmvlelem1  46692  hoidmvlelem3  46694  hoiqssbllem2  46720  hspmbllem2  46724  opnvonmbllem2  46730  iinhoiicc  46771  smfpimbor1lem2  46896  isclatd  49082  setrec1lem2  49788  setrec1lem3  49789