Theorem dfss3 3910

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

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

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 3052  df-ss 3906

This theorem is referenced by:  ssrab  4011  dfss5  4215  elpwunsn  4628  eqsn  4772  uni0b  4876  uni0c  4877  ssint  4906  ssiinf  4997  sspwuni  5042  dftr3  5197  wefrc  5625  rninxp  6143  frpoinsg  6307  ordunisssuc  6431  fnres  6625  eqfnfv3  6985  funimass3  7006  ffvresb  7078  tfisg  7805  tfis  7806  smogt  8307  cofonr  8610  naddrid  8619  pwssfi  9111  unifi  9254  unifi2  9255  fissuni  9267  fipreima  9268  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  14399  4sqlem19  16934  imasaddfnlem  17492  imasvscafn  17501  setcepi  18055  acsfiindd  18519  sylow2blem3  19597  sylow3lem6  19607  efgval2  19699  iscyggen2  19856  iscyg3  19861  isdomn2  20688  isdomn2OLD  20689  issubdrg  20757  ishil2  21699  rintopn  22874  isbasis2g  22913  tgval2  22921  eltg2b  22924  tgss2  22952  basgen2  22954  bastop1  22958  intcld  23005  unicld  23011  isclo  23052  isclo2  23053  neips  23078  opnnei  23085  neiptopnei  23097  isperf3  23118  ssidcn  23220  ist1-3  23314  cmpcov2  23355  cmpsub  23365  2ndcdisj2  23422  txkgen  23617  xkoinjcn  23652  tgqtop  23677  flimopn  23940  flfnei  23956  tmdcn2  24054  qustgplem  24086  cfil3i  25236  cmetcaulem  25255  ovolfioo  25434  ovolficc  25435  ovolicc2lem4  25487  opnmblALT  25570  xrlimcnp  26932  madebdayim  27880  oldfib  28369  uvtxnbgrss  29461  iscplgr  29484  vdiscusgrb  29599  ubthlem1  30941  isdrng4  33356  prmidl2  33501  hasheuni  34229  dmvlsiga  34273  ispisys2  34297  omssubadd  34444  eulerpartlemr  34518  eulerpartlemn  34525  cvmlift2lem1  35484  cvmlift2lem12  35496  mclsax  35751  isfne4  36522  isfne2  36524  isfne3  36525  neibastop2lem  36542  filnetlem4  36563  fvineqsneq  37728  fin2so  37928  poimirlem24  37965  poimirlem27  37968  nninfnub  38072  unichnidl  38352  ispridl2  38359  n0elqs  38653  ssdmral  38700  pmapglb  40216  hdmapoc  42377  isnacs2  43138  setindtrs  43453  dford3lem2  43455  dford3  43456  ssunib  43648  ntrneicls00  44516  ntrneixb  44522  ntrneik3  44523  ntrneix3  44524  ntrneik13  44525  ntrneix13  44526  trfr  45389  ssabso  45401  ssdf  45506  ballss3  45523  iunincfi  45524  restuni3  45548  disjf1o  45621  mapss2  45634  difmap  45636  unirnmap  45637  inmap  45638  difmapsn  45641  uzfissfz  45756  iuneqfzuzlem  45764  ssuzfz  45779  iccdificc  45969  iooiinicc  45972  ressiocsup  45984  ressioosup  45985  iooiinioc  45986  ressiooinf  45987  fsumiunss  46005  limciccioolb  46051  limcicciooub  46065  limcresiooub  46070  limsupresxr  46194  liminfresxr  46195  icccncfext  46315  dmvolss  46413  stoweidlem31  46459  stoweidlem39  46467  fourierdlem8  46543  fourierdlem27  46562  fourierdlem38  46573  fourierdlem40  46575  fourierdlem41  46576  fourierdlem46  46580  fourierdlem48  46582  fourierdlem49  46583  fourierdlem51  46585  fourierdlem64  46598  fourierdlem70  46604  fourierdlem71  46605  fourierdlem76  46610  fourierdlem78  46612  fourierdlem79  46613  fourierdlem80  46614  fourierdlem93  46627  fourierdlem97  46631  fourierdlem103  46637  fourierdlem104  46638  salexct  46762  salgencntex  46771  gsumge0cl  46799  sge0fodjrnlem  46844  sge0reuz  46875  iundjiun  46888  icoresmbl  46971  hoidmv1le  47022  hoidmvlelem1  47023  hoidmvlelem3  47025  hoiqssbllem2  47051  hspmbllem2  47055  opnvonmbllem2  47061  iinhoiicc  47102  smfpimbor1lem2  47227  isclatd  49458  setrec1lem2  50163  setrec1lem3  50164