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

Theorem dfss2 3146
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 3145 . . 3 (𝐴𝐵𝐴 = (𝐴𝐵))
2 df-in 3137 . . . 4 (𝐴𝐵) = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
32eqeq2i 2188 . . 3 (𝐴 = (𝐴𝐵) ↔ 𝐴 = {𝑥 ∣ (𝑥𝐴𝑥𝐵)})
4 abeq2 2286 . . 3 (𝐴 = {𝑥 ∣ (𝑥𝐴𝑥𝐵)} ↔ ∀𝑥(𝑥𝐴 ↔ (𝑥𝐴𝑥𝐵)))
51, 3, 43bitri 206 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴 ↔ (𝑥𝐴𝑥𝐵)))
6 pm4.71 389 . . 3 ((𝑥𝐴𝑥𝐵) ↔ (𝑥𝐴 ↔ (𝑥𝐴𝑥𝐵)))
76albii 1470 . 2 (∀𝑥(𝑥𝐴𝑥𝐵) ↔ ∀𝑥(𝑥𝐴 ↔ (𝑥𝐴𝑥𝐵)))
85, 7bitr4i 187 1 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105  wal 1351   = wceq 1353  wcel 2148  {cab 2163  cin 3130  wss 3131
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3137  df-ss 3144
This theorem is referenced by:  dfss3  3147  dfss2f  3148  ssel  3151  ssriv  3161  ssrdv  3163  sstr2  3164  eqss  3172  nssr  3217  rabss2  3240  ssconb  3270  ssequn1  3307  unss  3311  ssin  3359  ssddif  3371  reldisj  3476  ssdif0im  3489  inssdif0im  3492  ssundifim  3508  sbcssg  3534  pwss  3593  snssOLD  3720  snssb  3727  snsssn  3763  ssuni  3833  unissb  3841  intss  3867  iunss  3929  dftr2  4105  axpweq  4173  axpow2  4178  ssextss  4222  ordunisuc2r  4515  setind  4540  zfregfr  4575  tfi  4583  ssrel  4716  ssrel2  4718  ssrelrel  4728  reliun  4749  relop  4779  issref  5013  funimass4  5568  isprm2  12119  bj-inf2vnlem3  14763  bj-inf2vnlem4  14764
  Copyright terms: Public domain W3C validator