Theorem dfss3 3920

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568   ∈ wcel 2145  ∀wral 3077   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ral 3078  df-ss 3916

This theorem is used by:  ssrab  4019  dfss5  4221  elpwunsn  4645  eqsn  4790  uni0b  4894  uni0c  4895  ssint  4924  ssiinf  5013  sspwuni  5060  dftr3  5217  wefrc  5645  rninxp  6171  frpoinsg  6345  ordunisssuc  6470  fnres  6664  eqfnfv3  7029  funimass3  7051  ffvresb  7124  tfisg  7863  tfis  7864  smogt  8368  cofonr  8676  naddrid  8686  pwssfi  9185  unifi  9326  unifi2  9327  fissuni  9339  fipreima  9340  cantnf  9687  setinds  9743  frinsg  9748  tz9.12lem3  9789  r1elss  9807  rankval3b  9829  rankonidlem  9831  bndrank  9847  elhf3  9906  setrec1lem2  9960  setrec1lem3  9962  iscard  10049  cfub  10319  cflm  10320  fin1a2s  10485  dcomex  10518  ttukeylem6  10585  unirnfdomd  10645  alephreg  10660  tskord  10858  gruuni  10878  intgru  10892  grudomon  10895  axgroth3  10909  suplem1pr  11130  supexpr  11132  supsr  11190  hashfun  14575  4sqlem19  17134  imasaddfnlem  17693  imasvscafn  17702  setcepi  18256  acsfiindd  18720  sylow2blem3  19829  sylow3lem6  19839  efgval2  19931  iscyggen2  20088  iscyg3  20093  isdomn2  20956  isdrng4  20985  issubdrg  21030  unichnlidl  21509  prmidl2  21615  ishil2  22018  rintopn  23220  isbasis2g  23259  tgval2  23267  eltg2b  23270  tgss2  23298  basgen2  23300  bastop1  23304  intcld  23351  unicld  23357  isclo  23398  isclo2  23399  neips  23424  opnnei  23431  neiptopnei  23443  isperf3  23464  ssidcn  23566  ist1-3  23660  cmpcov2  23701  cmpsub  23711  2ndcdisj2  23769  txkgen  23964  xkoinjcn  23999  tgqtop  24024  flimopn  24287  flfnei  24303  tmdcn2  24401  qustgplem  24433  cfil3i  25583  cmetcaulem  25602  ovolfioo  25781  ovolficc  25782  ovolicc2lem4  25834  opnmblALT  25917  xrlimcnp  27289  madebdayim  28267  oldfib  28756  uvtxnbgrss  29966  iscplgr  29989  vdiscusgrb  30104  ubthlem1  31465  hasheuni  34710  dmvlsiga  34754  ispisys2  34779  omssubadd  34925  eulerpartlemr  34999  eulerpartlemn  35006  cvmlift2lem1  36046  cvmlift2lem12  36058  mclsax  36313  dffr5  36498  dffr7  36700  nmulrid  36926  isfne4  37108  isfne2  37110  isfne3  37111  neibastop2lem  37128  filnetlem4  37149  fvineqsneq  38315  fin2so  38510  poimirlem24  38542  poimirlem27  38545  nninfnub  38665  unichnidl  38945  ispridl2  38952  n0elqs  39244  ssdmral  39291  pmapglb  40807  hdmapoc  42968  isnacs2  43696  setindtrs  44011  dford3lem2  44013  dford3  44014  ssunib  44206  ntrneicls00  45074  ntrneixb  45080  ntrneik3  45081  ntrneix3  45082  ntrneik13  45083  ntrneix13  45084  trfr  45930  ssabso  45942  ssdf  46061  ballss3  46077  iunincfi  46078  restuni3  46102  disjf1o  46175  mapss2  46188  difmap  46189  unirnmap  46190  inmap  46191  difmapsn  46194  uzfissfz  46307  iuneqfzuzlem  46315  ssuzfz  46330  iccdificc  46520  iooiinicc  46523  ressiocsup  46535  ressioosup  46536  iooiinioc  46537  ressiooinf  46538  fsumiunss  46556  limciccioolb  46602  limcicciooub  46616  limcresiooub  46621  limsupresxr  46745  liminfresxr  46746  icccncfext  46866  dmvolss  46964  stoweidlem31  47010  stoweidlem39  47018  fourierdlem8  47094  fourierdlem27  47113  fourierdlem38  47124  fourierdlem40  47126  fourierdlem41  47127  fourierdlem46  47131  fourierdlem51  47136  fourierdlem64  47149  fourierdlem70  47155  fourierdlem71  47156  fourierdlem76  47161  fourierdlem78  47163  fourierdlem79  47164  fourierdlem80  47165  fourierdlem93  47178  fourierdlem97  47182  fourierdlem103  47188  fourierdlem104  47189  salexct  47313  salgencntex  47322  gsumge0cl  47350  sge0fodjrnlem  47395  sge0reuz  47426  iundjiun  47439  icoresmbl  47522  hoidmv1le  47573  hoidmvlelem1  47574  hoidmvlelem3  47576  hoiqssbllem2  47602  hspmbllem2  47606  opnvonmbllem2  47612  iinhoiicc  47653  smfpimbor1lem2  47778  isclatd  50060