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

Theorem dfss2 3952
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 3950 . . 3 (𝐴𝐵𝐴 = (𝐴𝐵))
2 df-in 3940 . . . 4 (𝐴𝐵) = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
32eqeq2i 2831 . . 3 (𝐴 = (𝐴𝐵) ↔ 𝐴 = {𝑥 ∣ (𝑥𝐴𝑥𝐵)})
4 abeq2 2942 . . 3 (𝐴 = {𝑥 ∣ (𝑥𝐴𝑥𝐵)} ↔ ∀𝑥(𝑥𝐴 ↔ (𝑥𝐴𝑥𝐵)))
51, 3, 43bitri 298 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴 ↔ (𝑥𝐴𝑥𝐵)))
6 pm4.71 558 . . 3 ((𝑥𝐴𝑥𝐵) ↔ (𝑥𝐴 ↔ (𝑥𝐴𝑥𝐵)))
76albii 1811 . 2 (∀𝑥(𝑥𝐴𝑥𝐵) ↔ ∀𝑥(𝑥𝐴 ↔ (𝑥𝐴𝑥𝐵)))
85, 7bitr4i 279 1 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wal 1526   = wceq 1528  wcel 2105  {cab 2796  cin 3932  wss 3933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-in 3940  df-ss 3949
This theorem is referenced by:  dfss3  3953  dfss6  3954  dfss2f  3955  ssel  3958  ssriv  3968  ssrdv  3970  sstr2  3971  eqss  3979  nss  4026  rabss2  4051  ssconb  4111  ssequn1  4153  unss  4157  ssin  4204  ssdif0  4320  difin0ss  4325  inssdif0  4326  reldisj  4398  ssundif  4429  sbcssg  4459  pwss  4555  snssg  4709  pwpw0  4738  pwsnALT  4823  ssuni  4852  unissb  4861  iunss  4960  dftr2  5165  axpweq  5256  axpow2  5259  ssextss  5337  ssrel  5650  ssrel2  5652  ssrelrel  5662  reliun  5682  relop  5714  idrefALT  5966  funimass4  6723  dfom2  7571  inf2  9074  grothprim  10244  psslinpr  10441  ltaddpr  10444  isprm2  16014  vdwmc2  16303  acsmapd  17776  dfconn2  21955  iskgen3  22085  metcld  23836  metcld2  23837  isch2  28927  pjnormssi  29872  ssiun3  30238  ssrelf  30294  bnj1361  31999  bnj978  32120  dffr5  32886  brsset  33247  sscoid  33271  relowlpssretop  34527  fvineqsneq  34575  rp-fakeinunass  39759  rababg  39811  ss2iundf  39882  dfhe3  39999  snhesn  40010  dffrege76  40163  ntrneiiso  40319  ntrneik2  40320  ntrneix2  40321  ntrneikb  40322  expanduniss  40506  ismnuprim  40507  onfrALTlem2  40757  trsspwALT  41029  trsspwALT2  41030  snssiALTVD  41038  snssiALT  41039  sstrALT2VD  41045  sstrALT2  41046  sbcssgVD  41094  onfrALTlem2VD  41100  sspwimp  41129  sspwimpVD  41130  sspwimpcf  41131  sspwimpcfVD  41132  sspwimpALT  41136  unisnALT  41137  iunssf  41229  icccncfext  42046
  Copyright terms: Public domain W3C validator