Theorem dfss3 3956

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

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1535   ∈ wcel 2114  ∀wral 3138   ⊆ wss 3936

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-ral 3143  df-in 3943  df-ss 3952

This theorem is referenced by:  ssrab  4049  dfss5  4241  elpwunsn  4621  eqsn  4762  uni0b  4864  uni0c  4865  ssint  4892  ssiinf  4978  sspwuni  5022  dftr3  5176  wefrc  5549  rninxp  6036  wfisg  6183  ordunisssuc  6293  fnres  6474  eqfnfv3  6804  funimass3  6824  ffvresb  6888  tfis  7569  smogt  8004  unifi  8813  unifi2  8814  fissuni  8829  fipreima  8830  cantnf  9156  tz9.12lem3  9218  r1elss  9235  rankval3b  9255  rankonidlem  9257  bndrank  9270  iscard  9404  cfub  9671  cflm  9672  fin1a2s  9836  dcomex  9869  ttukeylem6  9936  unirnfdomd  9989  alephreg  10004  tskord  10202  gruuni  10222  intgru  10236  grudomon  10239  axgroth3  10253  suplem1pr  10474  supexpr  10476  supsr  10534  hashfun  13799  4sqlem19  16299  imasaddfnlem  16801  imasvscafn  16810  setcepi  17348  acsfiindd  17787  sylow2blem3  18747  sylow3lem6  18757  efgval2  18850  iscyggen2  19000  iscyg3  19005  issubdrg  19560  isdomn2  20072  ishil2  20863  rintopn  21517  isbasis2g  21556  tgval2  21564  eltg2b  21567  tgss2  21595  basgen2  21597  bastop1  21601  intcld  21648  unicld  21654  isclo  21695  isclo2  21696  neips  21721  opnnei  21728  neiptopnei  21740  isperf3  21761  ssidcn  21863  ist1-3  21957  cmpcov2  21998  cmpsub  22008  2ndcdisj2  22065  txkgen  22260  xkoinjcn  22295  tgqtop  22320  flimopn  22583  flfnei  22599  tmdcn2  22697  qustgplem  22729  cfil3i  23872  cmetcaulem  23891  ovolfioo  24068  ovolficc  24069  ovolicc2lem4  24121  opnmblALT  24204  xrlimcnp  25546  uvtxnbgrss  27174  iscplgr  27197  vdiscusgrb  27312  ubthlem1  28647  prmidl2  30958  hasheuni  31344  dmvlsiga  31388  ispisys2  31412  omssubadd  31558  eulerpartlemr  31632  eulerpartlemn  31639  cvmlift2lem1  32549  cvmlift2lem12  32561  mclsax  32816  setinds  33023  tfisg  33055  frpoinsg  33081  frinsg  33087  isfne4  33688  isfne2  33690  isfne3  33691  neibastop2lem  33708  filnetlem4  33729  fvineqsneq  34696  fin2so  34894  poimirlem24  34931  poimirlem27  34934  nninfnub  35041  unichnidl  35324  ispridl2  35331  n0elqs  35598  pmapglb  36921  hdmapoc  39082  isnacs2  39323  setindtrs  39642  dford3lem2  39644  dford3  39645  ntrneicls00  40459  ntrneixb  40465  ntrneik3  40466  ntrneix3  40467  ntrneik13  40468  ntrneix13  40469  pwssfi  41327  ssdf  41359  ballss3  41379  iunincfi  41380  restuni3  41404  disjf1o  41472  mapss2  41488  difmap  41490  unirnmap  41491  inmap  41492  difmapsn  41495  uzfissfz  41614  iuneqfzuzlem  41622  ssuzfz  41637  iccdificc  41835  iooiinicc  41838  ressiocsup  41850  ressioosup  41851  iooiinioc  41852  ressiooinf  41853  fsumiunss  41876  limciccioolb  41922  limcicciooub  41938  limcresiooub  41943  limsupresxr  42067  liminfresxr  42068  icccncfext  42190  dmvolss  42290  stoweidlem31  42336  stoweidlem39  42344  fourierdlem8  42420  fourierdlem27  42439  fourierdlem38  42450  fourierdlem40  42452  fourierdlem41  42453  fourierdlem46  42457  fourierdlem48  42459  fourierdlem49  42460  fourierdlem51  42462  fourierdlem53  42464  fourierdlem64  42475  fourierdlem70  42481  fourierdlem71  42482  fourierdlem76  42487  fourierdlem78  42489  fourierdlem79  42490  fourierdlem80  42491  fourierdlem93  42504  fourierdlem97  42508  fourierdlem103  42514  fourierdlem104  42515  salexct  42637  salgencntex  42646  gsumge0cl  42673  sge0fodjrnlem  42718  sge0reuz  42749  iundjiun  42762  icoresmbl  42845  hoicvr  42850  hoidmv1le  42896  hoidmvlelem1  42897  hoidmvlelem3  42899  hoiqssbllem2  42925  hspmbllem2  42929  opnvonmbllem2  42935  iinhoiicc  42976  smfpimbor1lem2  43094  setrec1lem2  44811  setrec1lem3  44812