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

Theorem dfss2 3003
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 3002 . . 3 (𝐴𝐵𝐴 = (𝐴𝐵))
2 df-in 2994 . . . 4 (𝐴𝐵) = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
32eqeq2i 2095 . . 3 (𝐴 = (𝐴𝐵) ↔ 𝐴 = {𝑥 ∣ (𝑥𝐴𝑥𝐵)})
4 abeq2 2193 . . 3 (𝐴 = {𝑥 ∣ (𝑥𝐴𝑥𝐵)} ↔ ∀𝑥(𝑥𝐴 ↔ (𝑥𝐴𝑥𝐵)))
51, 3, 43bitri 204 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴 ↔ (𝑥𝐴𝑥𝐵)))
6 pm4.71 381 . . 3 ((𝑥𝐴𝑥𝐵) ↔ (𝑥𝐴 ↔ (𝑥𝐴𝑥𝐵)))
76albii 1402 . 2 (∀𝑥(𝑥𝐴𝑥𝐵) ↔ ∀𝑥(𝑥𝐴 ↔ (𝑥𝐴𝑥𝐵)))
85, 7bitr4i 185 1 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103  wal 1285   = wceq 1287  wcel 1436  {cab 2071  cin 2987  wss 2988
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-11 1440  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-in 2994  df-ss 3001
This theorem is referenced by:  dfss3  3004  dfss2f  3005  ssel  3008  ssriv  3018  ssrdv  3020  sstr2  3021  eqss  3029  nssr  3073  rabss2  3093  ssconb  3122  ssequn1  3159  unss  3163  ssin  3211  ssddif  3222  reldisj  3322  ssdif0im  3335  inssdif0im  3338  ssundifim  3353  sbcssg  3378  pwss  3430  snss  3549  snsssn  3588  ssuni  3658  unissb  3666  intss  3692  iunss  3754  dftr2  3913  axpweq  3981  axpow2  3986  ssextss  4021  ordunisuc2r  4304  setind  4328  zfregfr  4362  tfi  4370  ssrel  4494  ssrel2  4496  ssrelrel  4506  reliun  4526  relop  4554  issref  4781  funimass4  5318  isprm2  10974  bj-inf2vnlem3  11305  bj-inf2vnlem4  11306
  Copyright terms: Public domain W3C validator