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

Theorem dfss2 2928
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 (ABx(x Ax B))
Distinct variable groups:   x,A   x,B

Proof of Theorem dfss2
StepHypRef Expression
1 dfss 2926 . . 3 (ABA = (AB))
2 df-in 2918 . . . 4 (AB) = {x ∣ (x A x B)}
32eqeq2i 2047 . . 3 (A = (AB) ↔ A = {x ∣ (x A x B)})
4 abeq2 2143 . . 3 (A = {x ∣ (x A x B)} ↔ x(x A ↔ (x A x B)))
51, 3, 43bitri 195 . 2 (ABx(x A ↔ (x A x B)))
6 pm4.71 369 . . 3 ((x Ax B) ↔ (x A ↔ (x A x B)))
76albii 1356 . 2 (x(x Ax B) ↔ x(x A ↔ (x A x B)))
85, 7bitr4i 176 1 (ABx(x Ax B))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98  wal 1240   = wceq 1242   wcel 1390  {cab 2023  cin 2910  wss 2911
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-11 1394  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-in 2918  df-ss 2925
This theorem is referenced by:  dfss3  2929  dfss2f  2930  ssel  2933  ssriv  2943  ssrdv  2945  sstr2  2946  eqss  2954  nssr  2997  rabss2  3017  ssconb  3070  ssequn1  3107  unss  3111  ssin  3153  ssddif  3165  reldisj  3265  ssdif0im  3280  inssdif0im  3285  ssundifim  3300  sbcssg  3324  pwss  3366  snss  3485  snsssn  3523  ssuni  3593  unissb  3601  intss  3627  iunss  3689  dftr2  3847  axpweq  3915  axpow2  3920  ssextss  3947  ordunisuc2r  4205  setind  4222  tfi  4248  ssrel  4371  ssrel2  4373  ssrelrel  4383  reliun  4401  relop  4429  issref  4650  funimass4  5167  bj-inf2vnlem3  9402  bj-inf2vnlem4  9403
  Copyright terms: Public domain W3C validator