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

Theorem dfss2 3954
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 3952 . . 3 (𝐴𝐵𝐴 = (𝐴𝐵))
2 df-in 3942 . . . 4 (𝐴𝐵) = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
32eqeq2i 2834 . . 3 (𝐴 = (𝐴𝐵) ↔ 𝐴 = {𝑥 ∣ (𝑥𝐴𝑥𝐵)})
4 abeq2 2945 . . 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 2799  cin 3934  wss 3935
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 2793
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 2800  df-cleq 2814  df-clel 2893  df-in 3942  df-ss 3951
This theorem is referenced by:  dfss3  3955  dfss6  3956  dfss2f  3957  ssel  3960  ssriv  3970  ssrdv  3972  sstr2  3973  eqss  3981  nss  4028  rabss2  4053  ssconb  4113  ssequn1  4155  unss  4159  ssin  4206  ssdif0  4322  difin0ss  4327  inssdif0  4328  reldisj  4400  ssundif  4431  sbcssg  4461  pwss  4557  snssg  4711  pwpw0  4740  pwsnALT  4825  ssuni  4854  unissb  4863  iunss  4961  dftr2  5166  axpweq  5257  axpow2  5260  ssextss  5338  ssrel  5651  ssrel2  5653  ssrelrel  5663  reliun  5683  relop  5715  idrefALT  5967  funimass4  6724  dfom2  7570  inf2  9075  grothprim  10245  psslinpr  10442  ltaddpr  10445  isprm2  16016  vdwmc2  16305  acsmapd  17778  dfconn2  21957  iskgen3  22087  metcld  23838  metcld2  23839  isch2  28928  pjnormssi  29873  ssiun3  30239  ssrelf  30295  bnj1361  32000  bnj978  32121  dffr5  32887  brsset  33248  sscoid  33272  relowlpssretop  34528  fvineqsneq  34576  rp-fakeinunass  39761  rababg  39813  ss2iundf  39884  dfhe3  40001  snhesn  40012  dffrege76  40165  ntrneiiso  40321  ntrneik2  40322  ntrneix2  40323  ntrneikb  40324  expanduniss  40509  ismnuprim  40510  onfrALTlem2  40760  trsspwALT  41032  trsspwALT2  41033  snssiALTVD  41041  snssiALT  41042  sstrALT2VD  41048  sstrALT2  41049  sbcssgVD  41097  onfrALTlem2VD  41103  sspwimp  41132  sspwimpVD  41133  sspwimpcf  41134  sspwimpcfVD  41135  sspwimpALT  41139  unisnALT  41140  iunssf  41232  icccncfext  42050
  Copyright terms: Public domain W3C validator