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

Theorem dfss2 3786
Description: Alternate definition of the subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. (Contributed by NM, 8-Jan-2002.)
Assertion
Ref Expression
dfss2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem dfss2
StepHypRef Expression
1 dfss 3784 . . 3 (𝐴𝐵𝐴 = (𝐴𝐵))
2 df-in 3776 . . . 4 (𝐴𝐵) = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
32eqeq2i 2818 . . 3 (𝐴 = (𝐴𝐵) ↔ 𝐴 = {𝑥 ∣ (𝑥𝐴𝑥𝐵)})
4 abeq2 2916 . . 3 (𝐴 = {𝑥 ∣ (𝑥𝐴𝑥𝐵)} ↔ ∀𝑥(𝑥𝐴 ↔ (𝑥𝐴𝑥𝐵)))
51, 3, 43bitri 288 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴 ↔ (𝑥𝐴𝑥𝐵)))
6 pm4.71 549 . . 3 ((𝑥𝐴𝑥𝐵) ↔ (𝑥𝐴 ↔ (𝑥𝐴𝑥𝐵)))
76albii 1904 . 2 (∀𝑥(𝑥𝐴𝑥𝐵) ↔ ∀𝑥(𝑥𝐴 ↔ (𝑥𝐴𝑥𝐵)))
85, 7bitr4i 269 1 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  wal 1635   = wceq 1637  wcel 2156  {cab 2792  cin 3768  wss 3769
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-in 3776  df-ss 3783
This theorem is referenced by:  dfss3  3787  dfss6  3788  dfss2f  3789  ssel  3792  ssriv  3802  ssrdv  3804  sstr2  3805  eqss  3813  nss  3860  rabss2  3882  ssconb  3942  ssequn1  3982  unss  3986  ssin  4031  ssdif0  4143  difin0ss  4147  inssdif0  4148  reldisj  4217  ssundif  4248  sbcssg  4278  pwss  4368  snssg  4505  pwpw0  4534  pwsnALT  4623  ssuni  4654  unissb  4663  iunss  4753  dftr2  4948  axpweq  5034  axpow2  5037  ssextss  5112  ssrel  5409  ssrelOLD  5410  ssrel2  5412  ssrelrel  5422  reliun  5441  relop  5474  idrefALT  5719  idrefOLD  5720  funimass4  6464  dfom2  7293  inf2  8763  grothpw  9929  grothprim  9937  psslinpr  10134  ltaddpr  10137  isprm2  15609  vdwmc2  15896  acsmapd  17379  dfconn2  21433  iskgen3  21563  metcld  23314  metcld2  23315  isch2  28407  pjnormssi  29354  ssiun3  29700  ssrelf  29751  bnj1361  31220  bnj978  31340  dffr5  31963  brsset  32315  sscoid  32339  relowlpssretop  33526  rp-fakeinunass  38358  rababg  38376  ss2iundf  38448  dfhe3  38566  snhesn  38577  dffrege76  38730  ntrneiiso  38886  ntrneik2  38887  ntrneix2  38888  ntrneikb  38889  sbcssOLD  39251  onfrALTlem2  39256  trsspwALT  39539  trsspwALT2  39540  snssiALTVD  39553  snssiALT  39554  sstrALT2VD  39560  sstrALT2  39561  sbcssgVD  39610  onfrALTlem2VD  39616  sspwimp  39645  sspwimpVD  39646  sspwimpcf  39647  sspwimpcfVD  39648  sspwimpALT  39652  unisnALT  39653  iunssf  39753  icccncfext  40577
  Copyright terms: Public domain W3C validator