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  4220  elpwunsn  4632  eqsn  4776  uni0b  4880  uni0c  4881  ssint  4909  ssiinf  4998  sspwuni  5043  dftr3  5198  wefrc  5605  rninxp  6121  frpoinsg  6285  ordunisssuc  6409  fnres  6603  eqfnfv3  6961  funimass3  6982  ffvresb  7053  tfisg  7779  tfis  7780  smogt  8282  cofonr  8584  naddrid  8593  pwssfi  9081  unifi  9223  unifi2  9224  fissuni  9236  fipreima  9237  cantnf  9578  setinds  9634  frinsg  9639  tz9.12lem3  9677  r1elss  9694  rankval3b  9714  rankonidlem  9716  bndrank  9729  iscard  9863  cfub  10135  cflm  10136  fin1a2s  10300  dcomex  10333  ttukeylem6  10400  unirnfdomd  10453  alephreg  10468  tskord  10666  gruuni  10686  intgru  10700  grudomon  10703  axgroth3  10717  suplem1pr  10938  supexpr  10940  supsr  10998  hashfun  14339  4sqlem19  16870  imasaddfnlem  17427  imasvscafn  17436  setcepi  17990  acsfiindd  18454  sylow2blem3  19529  sylow3lem6  19539  efgval2  19631  iscyggen2  19788  iscyg3  19793  isdomn2  20621  isdomn2OLD  20622  issubdrg  20690  ishil2  21651  rintopn  22819  isbasis2g  22858  tgval2  22866  eltg2b  22869  tgss2  22897  basgen2  22899  bastop1  22903  intcld  22950  unicld  22956  isclo  22997  isclo2  22998  neips  23023  opnnei  23030  neiptopnei  23042  isperf3  23063  ssidcn  23165  ist1-3  23259  cmpcov2  23300  cmpsub  23310  2ndcdisj2  23367  txkgen  23562  xkoinjcn  23597  tgqtop  23622  flimopn  23885  flfnei  23901  tmdcn2  23999  qustgplem  24031  cfil3i  25191  cmetcaulem  25210  ovolfioo  25390  ovolficc  25391  ovolicc2lem4  25443  opnmblALT  25526  xrlimcnp  26900  madebdayim  27828  uvtxnbgrss  29365  iscplgr  29388  vdiscusgrb  29504  ubthlem1  30842  isdrng4  33253  prmidl2  33398  hasheuni  34090  dmvlsiga  34134  ispisys2  34158  omssubadd  34305  eulerpartlemr  34379  eulerpartlemn  34386  cvmlift2lem1  35338  cvmlift2lem12  35350  mclsax  35605  isfne4  36374  isfne2  36376  isfne3  36377  neibastop2lem  36394  filnetlem4  36415  fvineqsneq  37446  fin2so  37647  poimirlem24  37684  poimirlem27  37687  nninfnub  37791  unichnidl  38071  ispridl2  38078  n0elqs  38360  pmapglb  39809  hdmapoc  41970  isnacs2  42739  setindtrs  43058  dford3lem2  43060  dford3  43061  ssunib  43253  ntrneicls00  44122  ntrneixb  44128  ntrneik3  44129  ntrneix3  44130  ntrneik13  44131  ntrneix13  44132  trfr  44995  ssabso  45007  ssdf  45112  ballss3  45130  iunincfi  45131  restuni3  45155  disjf1o  45228  mapss2  45242  difmap  45244  unirnmap  45245  inmap  45246  difmapsn  45249  uzfissfz  45365  iuneqfzuzlem  45373  ssuzfz  45388  iccdificc  45579  iooiinicc  45582  ressiocsup  45594  ressioosup  45595  iooiinioc  45596  ressiooinf  45597  fsumiunss  45615  limciccioolb  45661  limcicciooub  45675  limcresiooub  45680  limsupresxr  45804  liminfresxr  45805  icccncfext  45925  dmvolss  46023  stoweidlem31  46069  stoweidlem39  46077  fourierdlem8  46153  fourierdlem27  46172  fourierdlem38  46183  fourierdlem40  46185  fourierdlem41  46186  fourierdlem46  46190  fourierdlem48  46192  fourierdlem49  46193  fourierdlem51  46195  fourierdlem64  46208  fourierdlem70  46214  fourierdlem71  46215  fourierdlem76  46220  fourierdlem78  46222  fourierdlem79  46223  fourierdlem80  46224  fourierdlem93  46237  fourierdlem97  46241  fourierdlem103  46247  fourierdlem104  46248  salexct  46372  salgencntex  46381  gsumge0cl  46409  sge0fodjrnlem  46454  sge0reuz  46485  iundjiun  46498  icoresmbl  46581  hoicvr  46586  hoidmv1le  46632  hoidmvlelem1  46633  hoidmvlelem3  46635  hoiqssbllem2  46661  hspmbllem2  46665  opnvonmbllem2  46671  iinhoiicc  46712  smfpimbor1lem2  46837  isclatd  49014  setrec1lem2  49720  setrec1lem3  49721