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

Theorem dfss3 3057
Description: Alternate definition of subclass relationship. (Contributed by NM, 14-Oct-1999.)
Assertion
Ref Expression
dfss3 (𝐴𝐵 ↔ ∀𝑥𝐴 𝑥𝐵)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem dfss3
StepHypRef Expression
1 dfss2 3056 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
2 df-ral 2398 . 2 (∀𝑥𝐴 𝑥𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
31, 2bitr4i 186 1 (𝐴𝐵 ↔ ∀𝑥𝐴 𝑥𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104  wal 1314  wcel 1465  wral 2393  wss 3041
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 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-11 1469  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-ral 2398  df-in 3047  df-ss 3054
This theorem is referenced by:  ssrab  3145  eqsnm  3652  uni0b  3731  uni0c  3732  ssint  3757  ssiinf  3832  sspwuni  3867  dftr3  4000  tfis  4467  rninxp  4952  fnres  5209  eqfnfv3  5488  funimass3  5504  ffvresb  5551  tfrlemibxssdm  6192  tfr1onlembxssdm  6208  tfrcllembxssdm  6221  suplocsr  7585  isbasis2g  12139  tgval2  12147  eltg2b  12150  tgss2  12175  basgen2  12177  bastop1  12179  unicld  12212  neipsm  12250  ssidcn  12306  bdss  12989
  Copyright terms: Public domain W3C validator