Theorem dfss3 3558

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

Syntax hints:   → wi 4   ↔ wb 195  ∀wal 1473   ∈ wcel 1977  ∀wral 2896   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-ral 2901  df-in 3547  df-ss 3554

This theorem is referenced by:  ssrab  3643  elpwunsn  4171  eqsn  4301  eqsnOLD  4302  uni0b  4399  uni0c  4400  ssint  4428  ssiinf  4505  sspwuni  4547  dftr3  4684  wefrc  5032  rninxp  5492  wfisg  5632  ordunisssuc  5747  fnres  5921  eqfnfv3  6221  funimass3  6241  ffvresb  6301  tfis  6946  smogt  7351  unifi  8138  unifi2  8139  fissuni  8154  fipreima  8155  cantnf  8473  tz9.12lem3  8535  r1elss  8552  rankval3b  8572  rankonidlem  8574  bndrank  8587  iscard  8684  cfub  8954  cflm  8955  fin1a2s  9119  dcomex  9152  ttukeylem6  9219  unirnfdomd  9268  alephreg  9283  tskord  9481  gruuni  9501  intgru  9515  grudomon  9518  axgroth3  9532  suplem1pr  9753  supexpr  9755  supsr  9812  hashfun  13084  4sqlem19  15505  imasaddfnlem  16011  imasvscafn  16020  setcepi  16561  acsfiindd  17000  sylow2blem3  17860  sylow3lem6  17870  efgval2  17960  iscyggen2  18106  iscyg3  18111  issubdrg  18628  isdomn2  19120  ishil2  19882  rintopn  20539  isbasis2g  20563  tgval2  20571  eltg2b  20574  tgss2  20602  basgen2  20604  bastop1  20608  intcld  20654  unicld  20660  isclo  20701  isclo2  20702  neips  20727  opnnei  20734  neiptopnei  20746  isperf3  20767  ssidcn  20869  ist1-3  20963  cmpcov2  21003  cmpsub  21013  2ndcdisj2  21070  txkgen  21265  xkoinjcn  21300  tgqtop  21325  flimopn  21589  flfnei  21605  tmdcn2  21703  qustgplem  21734  cfil3i  22875  cmetcaulem  22894  ovolfioo  23043  ovolficc  23044  ovolicc2lem4  23095  opnmblALT  23177  xrlimcnp  24495  ubthlem1  27110  hasheuni  29474  dmvlsiga  29519  ispisys2  29543  omssubadd  29689  eulerpartlemr  29763  eulerpartlemn  29770  cvmlift2lem1  30538  cvmlift2lem12  30550  mclsax  30720  setinds  30927  tfisg  30960  frinsg  30986  isfne4  31505  isfne2  31507  isfne3  31508  neibastop2lem  31525  filnetlem4  31546  fin2so  32566  poimirlem24  32603  poimirlem27  32606  nninfnub  32717  unichnidl  33000  ispridl2  33007  pmapglb  34074  hdmapoc  36241  isnacs2  36287  setindtrs  36610  dford3lem2  36612  dford3  36613  ntrneicls00  37407  ntrneixb  37413  ntrneik3  37414  ntrneix3  37415  ntrneik13  37416  ntrneix13  37417  pwssfi  38236  ssdf  38273  ballss3  38298  iunincfi  38300  restuni3  38333  disjf1o  38373  mapss2  38392  difmap  38394  unirnmap  38395  inmap  38396  difmapsn  38399  unirnmapsn  38401  iunmapsn  38404  uzfissfz  38483  iuneqfzuzlem  38491  ssuzfz  38506  iccdificc  38613  iooiinicc  38616  ressiocsup  38628  ressioosup  38629  iooiinioc  38630  ressiooinf  38631  fsumiunss  38642  limciccioolb  38688  limcicciooub  38704  limcresiooub  38709  icccncfext  38773  dmvolss  38878  stoweidlem31  38924  stoweidlem39  38932  fourierdlem8  39008  fourierdlem27  39027  fourierdlem38  39038  fourierdlem40  39040  fourierdlem41  39041  fourierdlem46  39045  fourierdlem48  39047  fourierdlem49  39048  fourierdlem51  39050  fourierdlem53  39052  fourierdlem64  39063  fourierdlem70  39069  fourierdlem71  39070  fourierdlem76  39075  fourierdlem78  39077  fourierdlem79  39078  fourierdlem80  39079  fourierdlem93  39092  fourierdlem97  39096  fourierdlem103  39102  fourierdlem104  39103  rrxbasefi  39179  qndenserrn  39195  intsaluni  39223  salexct  39228  salgencntex  39237  gsumge0cl  39264  sge0fodjrnlem  39309  sge0reuz  39340  iundjiun  39353  meadjiunlem  39358  icoresmbl  39433  hoicvr  39438  hoidmv1le  39484  hoidmvlelem1  39485  hoidmvlelem3  39487  hoiqssbllem2  39513  hspmbllem2  39517  opnvonmbllem2  39523  iinhoiicc  39565  iunhoiioo  39567  smfpimbor1lem2  39684  dfss7  40304  uvtxanbgr  40618  nbupgruvtxres  40634  cplgruvtxb  40637  vdiscusgrb  40746  ssdifsn  42228  setrec1lem2  42234  setrec1lem3  42235