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

Theorem dfss2 3556
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 3554 . . 3 (𝐴𝐵𝐴 = (𝐴𝐵))
2 df-in 3546 . . . 4 (𝐴𝐵) = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
32eqeq2i 2621 . . 3 (𝐴 = (𝐴𝐵) ↔ 𝐴 = {𝑥 ∣ (𝑥𝐴𝑥𝐵)})
4 abeq2 2718 . . 3 (𝐴 = {𝑥 ∣ (𝑥𝐴𝑥𝐵)} ↔ ∀𝑥(𝑥𝐴 ↔ (𝑥𝐴𝑥𝐵)))
51, 3, 43bitri 284 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴 ↔ (𝑥𝐴𝑥𝐵)))
6 pm4.71 659 . . 3 ((𝑥𝐴𝑥𝐵) ↔ (𝑥𝐴 ↔ (𝑥𝐴𝑥𝐵)))
76albii 1736 . 2 (∀𝑥(𝑥𝐴𝑥𝐵) ↔ ∀𝑥(𝑥𝐴 ↔ (𝑥𝐴𝑥𝐵)))
85, 7bitr4i 265 1 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  wal 1472   = wceq 1474  wcel 1976  {cab 2595  cin 3538  wss 3539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-in 3546  df-ss 3553
This theorem is referenced by:  dfss3  3557  dfss2f  3558  ssel  3561  ssriv  3571  ssrdv  3573  sstr2  3574  eqss  3582  nss  3625  rabss2  3647  ssconb  3704  ssequn1  3744  unss  3748  ssin  3796  ssdif0  3895  difin0ss  3899  inssdif0  3900  reldisj  3971  ssundif  4003  sbcssg  4034  pwss  4122  snss  4258  pwpw0  4283  pwsnALT  4361  ssuni  4389  ssuniOLD  4390  unissb  4399  iunss  4491  dftr2  4676  axpweq  4762  axpow2  4765  ssextss  4842  ssrel  5119  ssrel2  5121  ssrelrel  5131  reliun  5150  relop  5181  issref  5414  funimass4  6141  dfom2  6936  inf2  8380  grothpw  9504  grothprim  9512  psslinpr  9709  ltaddpr  9712  isprm2  15181  vdwmc2  15469  acsmapd  16949  dfcon2  20979  iskgen3  21109  metcld  22856  metcld2  22857  isch2  27257  pjnormssi  28204  ssiun3  28552  ssrelf  28598  bnj1361  29946  bnj978  30066  dffr5  30689  brsset  30959  sscoid  30983  relowlpssretop  32171  rp-fakeinunass  36663  rababg  36681  ss2iundf  36753  dfss6  36865  dfhe3  36872  snhesn  36883  dffrege76  37036  ntrneiiso  37192  ntrneik2  37193  ntrneix2  37194  ntrneikb  37195  conss34OLD  37450  sbcssOLD  37560  onfrALTlem2  37565  trsspwALT  37850  trsspwALT2  37851  snssiALTVD  37867  snssiALT  37868  sstrALT2VD  37874  sstrALT2  37875  sbcssgVD  37924  onfrALTlem2VD  37930  sspwimp  37959  sspwimpVD  37960  sspwimpcf  37961  sspwimpcfVD  37962  sspwimpALT  37966  unisnALT  37967  iunssf  38073  icccncfext  38556
  Copyright terms: Public domain W3C validator