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

Theorem dfss2 3127
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 3126 . . 3 (𝐴𝐵𝐴 = (𝐴𝐵))
2 df-in 3118 . . . 4 (𝐴𝐵) = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
32eqeq2i 2175 . . 3 (𝐴 = (𝐴𝐵) ↔ 𝐴 = {𝑥 ∣ (𝑥𝐴𝑥𝐵)})
4 abeq2 2273 . . 3 (𝐴 = {𝑥 ∣ (𝑥𝐴𝑥𝐵)} ↔ ∀𝑥(𝑥𝐴 ↔ (𝑥𝐴𝑥𝐵)))
51, 3, 43bitri 205 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴 ↔ (𝑥𝐴𝑥𝐵)))
6 pm4.71 387 . . 3 ((𝑥𝐴𝑥𝐵) ↔ (𝑥𝐴 ↔ (𝑥𝐴𝑥𝐵)))
76albii 1457 . 2 (∀𝑥(𝑥𝐴𝑥𝐵) ↔ ∀𝑥(𝑥𝐴 ↔ (𝑥𝐴𝑥𝐵)))
85, 7bitr4i 186 1 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  wal 1340   = wceq 1342  wcel 2135  {cab 2150  cin 3111  wss 3112
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 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-11 1493  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146
This theorem depends on definitions:  df-bi 116  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-in 3118  df-ss 3125
This theorem is referenced by:  dfss3  3128  dfss2f  3129  ssel  3132  ssriv  3142  ssrdv  3144  sstr2  3145  eqss  3153  nssr  3198  rabss2  3221  ssconb  3251  ssequn1  3288  unss  3292  ssin  3340  ssddif  3352  reldisj  3456  ssdif0im  3469  inssdif0im  3472  ssundifim  3488  sbcssg  3514  pwss  3570  snss  3697  snsssn  3736  ssuni  3806  unissb  3814  intss  3840  iunss  3902  dftr2  4077  axpweq  4145  axpow2  4150  ssextss  4193  ordunisuc2r  4486  setind  4511  zfregfr  4546  tfi  4554  ssrel  4687  ssrel2  4689  ssrelrel  4699  reliun  4720  relop  4749  issref  4981  funimass4  5532  isprm2  12038  bj-inf2vnlem3  13716  bj-inf2vnlem4  13717
  Copyright terms: Public domain W3C validator