MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfss2 Structured version   Visualization version   GIF version

Theorem dfss2 3939
Description: Alternate definition of the subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. (Contributed by NM, 8-Jan-2002.) Avoid ax-10 2146, ax-11 2162, ax-12 2179. (Revised by SN, 16-May-2024.)
Assertion
Ref Expression
dfss2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem dfss2
StepHypRef Expression
1 dfcleq 2818 . 2 (𝐴 = (𝐴𝐵) ↔ ∀𝑥(𝑥𝐴𝑥 ∈ (𝐴𝐵)))
2 dfss 3937 . 2 (𝐴𝐵𝐴 = (𝐴𝐵))
3 pm4.71 561 . . . 4 ((𝑥𝐴𝑥𝐵) ↔ (𝑥𝐴 ↔ (𝑥𝐴𝑥𝐵)))
4 elin 3935 . . . . 5 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
54bibi2i 341 . . . 4 ((𝑥𝐴𝑥 ∈ (𝐴𝐵)) ↔ (𝑥𝐴 ↔ (𝑥𝐴𝑥𝐵)))
63, 5bitr4i 281 . . 3 ((𝑥𝐴𝑥𝐵) ↔ (𝑥𝐴𝑥 ∈ (𝐴𝐵)))
76albii 1821 . 2 (∀𝑥(𝑥𝐴𝑥𝐵) ↔ ∀𝑥(𝑥𝐴𝑥 ∈ (𝐴𝐵)))
81, 2, 73bitr4i 306 1 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wal 1536   = wceq 1538  wcel 2115  cin 3918  wss 3919
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3482  df-in 3926  df-ss 3936
This theorem is referenced by:  dfss3  3941  dfss6  3942  dfss2f  3943  ssel  3946  sselOLD  3947  ssriv  3957  ssrdv  3959  sstr2  3960  eqss  3968  nss  4015  rabss2  4040  ssconb  4100  ssequn1  4142  unss  4146  ssin  4192  ssdif0  4306  difin0ss  4311  inssdif0  4312  reldisj  4385  ssundif  4416  sbcssg  4446  pwss  4547  snssg  4702  pwpw0  4730  pwsnOLD  4817  ssuni  4849  unissb  4856  iunss  4955  dftr2  5160  axpweq  5252  axpow2  5255  ssextss  5333  ssrel  5644  ssrel2  5646  ssrelrel  5656  reliun  5676  relop  5708  idrefALT  5960  funimass4  6721  dfom2  7576  inf2  9083  grothprim  10254  psslinpr  10451  ltaddpr  10454  isprm2  16024  vdwmc2  16313  acsmapd  17788  dfconn2  22027  iskgen3  22157  metcld  23913  metcld2  23914  isch2  29009  pjnormssi  29954  ssiun3  30321  ssrelf  30377  bnj1361  32157  bnj978  32278  dffr5  33046  brsset  33407  sscoid  33431  relowlpssretop  34726  fvineqsneq  34774  rp-fakeinunass  40139  rababg  40189  ss2iundf  40276  dfhe3  40393  snhesn  40404  dffrege76  40557  ntrneiiso  40713  ntrneik2  40714  ntrneix2  40715  ntrneikb  40716  expanduniss  40921  ismnuprim  40922  onfrALTlem2  41172  trsspwALT  41444  trsspwALT2  41445  snssiALTVD  41453  snssiALT  41454  sstrALT2VD  41460  sstrALT2  41461  sbcssgVD  41509  onfrALTlem2VD  41515  sspwimp  41544  sspwimpVD  41545  sspwimpcf  41546  sspwimpcfVD  41547  sspwimpALT  41551  unisnALT  41552  iunssf  41644  icccncfext  42455
  Copyright terms: Public domain W3C validator