ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  dfss2 GIF version

Theorem dfss2 3054
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 3053 . . 3 (𝐴𝐵𝐴 = (𝐴𝐵))
2 df-in 3045 . . . 4 (𝐴𝐵) = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
32eqeq2i 2126 . . 3 (𝐴 = (𝐴𝐵) ↔ 𝐴 = {𝑥 ∣ (𝑥𝐴𝑥𝐵)})
4 abeq2 2224 . . 3 (𝐴 = {𝑥 ∣ (𝑥𝐴𝑥𝐵)} ↔ ∀𝑥(𝑥𝐴 ↔ (𝑥𝐴𝑥𝐵)))
51, 3, 43bitri 205 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴 ↔ (𝑥𝐴𝑥𝐵)))
6 pm4.71 384 . . 3 ((𝑥𝐴𝑥𝐵) ↔ (𝑥𝐴 ↔ (𝑥𝐴𝑥𝐵)))
76albii 1429 . 2 (∀𝑥(𝑥𝐴𝑥𝐵) ↔ ∀𝑥(𝑥𝐴 ↔ (𝑥𝐴𝑥𝐵)))
85, 7bitr4i 186 1 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  wal 1312   = wceq 1314  wcel 1463  {cab 2101  cin 3038  wss 3039
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-11 1467  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-in 3045  df-ss 3052
This theorem is referenced by:  dfss3  3055  dfss2f  3056  ssel  3059  ssriv  3069  ssrdv  3071  sstr2  3072  eqss  3080  nssr  3125  rabss2  3148  ssconb  3177  ssequn1  3214  unss  3218  ssin  3266  ssddif  3278  reldisj  3382  ssdif0im  3395  inssdif0im  3398  ssundifim  3414  sbcssg  3440  pwss  3494  snss  3617  snsssn  3656  ssuni  3726  unissb  3734  intss  3760  iunss  3822  dftr2  3996  axpweq  4063  axpow2  4068  ssextss  4110  ordunisuc2r  4398  setind  4422  zfregfr  4456  tfi  4464  ssrel  4595  ssrel2  4597  ssrelrel  4607  reliun  4628  relop  4657  issref  4889  funimass4  5438  isprm2  11694  bj-inf2vnlem3  12981  bj-inf2vnlem4  12982
  Copyright terms: Public domain W3C validator