HomeHome Intuitionistic Logic Explorer
Theorem List (p. 92 of 94)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 9101-9200   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremcjcli 9101 Closure law for complex conjugate. (Contributed by NM, 11-May-1999.)
 CC   =>     * `  CC
 
Theoremreplimi 9102 Construct a complex number from its real and imaginary parts. (Contributed by NM, 1-Oct-1999.)
 CC   =>     Re `  +  _i  x.  Im `
 
Theoremcjcji 9103 The conjugate of the conjugate is the original complex number. Proposition 10-3.4(e) of [Gleason] p. 133. (Contributed by NM, 11-May-1999.)
 CC   =>     * `  * `
 
Theoremreim0bi 9104 A number is real iff its imaginary part is 0. (Contributed by NM, 29-May-1999.)
 CC   =>     RR  Im `  0
 
Theoremrerebi 9105 A real number equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 27-Oct-1999.)
 CC   =>     RR  Re `
 
Theoremcjrebi 9106 A number is real iff it equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 11-Oct-1999.)
 CC   =>     RR  * `
 
Theoremrecji 9107 Real part of a complex conjugate. (Contributed by NM, 2-Oct-1999.)
 CC   =>     Re `  * `  Re `
 
Theoremimcji 9108 Imaginary part of a complex conjugate. (Contributed by NM, 2-Oct-1999.)
 CC   =>     Im `  * `  -u Im `
 
Theoremcjmulrcli 9109 A complex number times its conjugate is real. (Contributed by NM, 11-May-1999.)
 CC   =>     x.  * `  RR
 
Theoremcjmulvali 9110 A complex number times its conjugate. (Contributed by NM, 2-Oct-1999.)
 CC   =>     x.  * `  Re ` 
 ^ 2  +  Im `  ^ 2
 
Theoremcjmulge0i 9111 A complex number times its conjugate is nonnegative. (Contributed by NM, 28-May-1999.)
 CC   =>     0  <_  x.  * `
 
Theoremrenegi 9112 Real part of negative. (Contributed by NM, 2-Aug-1999.)
 CC   =>     Re `  -u  -u Re
 `
 
Theoremimnegi 9113 Imaginary part of negative. (Contributed by NM, 2-Aug-1999.)
 CC   =>     Im `  -u  -u Im
 `
 
Theoremcjnegi 9114 Complex conjugate of negative. (Contributed by NM, 2-Aug-1999.)
 CC   =>     * `  -u  -u * `
 
Theoremaddcji 9115 A number plus its conjugate is twice its real part. Compare Proposition 10-3.4(h) of [Gleason] p. 133. (Contributed by NM, 2-Oct-1999.)
 CC   =>     +  * `  2  x.  Re `
 
Theoremreaddi 9116 Real part distributes over addition. (Contributed by NM, 28-Jul-1999.)
 CC   &     CC   =>     Re `  +  Re
 `  +  Re `
 
Theoremimaddi 9117 Imaginary part distributes over addition. (Contributed by NM, 28-Jul-1999.)
 CC   &     CC   =>     Im `  +  Im
 `  +  Im `
 
Theoremremuli 9118 Real part of a product. (Contributed by NM, 28-Jul-1999.)
 CC   &     CC   =>     Re `  x.  Re `  x.  Re `  -  Im `  x.  Im `
 
Theoremimmuli 9119 Imaginary part of a product. (Contributed by NM, 28-Jul-1999.)
 CC   &     CC   =>     Im `  x.  Re `  x.  Im `  +  Im `  x.  Re `
 
Theoremcjaddi 9120 Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.)
 CC   &     CC   =>     * `  +  * `
  +  * `
 
Theoremcjmuli 9121 Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.)
 CC   &     CC   =>     * `  x.  * `
  x.  * `
 
Theoremipcni 9122 Standard inner product on complex numbers. (Contributed by NM, 2-Oct-1999.)
 CC   &     CC   =>     Re `  x.  * `  Re
 `  x.  Re `  +  Im `  x.  Im `
 
Theoremcjdivapi 9123 Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.)
 CC   &     CC   =>    #  0  * `  * `  * `
 
Theoremcrrei 9124 The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.)
 RR   &     RR   =>     Re `  +  _i  x.
 
Theoremcrimi 9125 The imaginary part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.)
 RR   &     RR   =>     Im `  +  _i  x.
 
Theoremrecld 9126 The real part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.)
 CC   =>     Re ` 
 RR
 
Theoremimcld 9127 The imaginary part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.)
 CC   =>     Im ` 
 RR
 
Theoremcjcld 9128 Closure law for complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
 CC   =>     * ` 
 CC
 
Theoremreplimd 9129 Construct a complex number from its real and imaginary parts. (Contributed by Mario Carneiro, 29-May-2016.)
 CC   =>     Re `  +  _i  x.  Im `
 
Theoremremimd 9130 Value of the conjugate of a complex number. The value is the real part minus  _i times the imaginary part. Definition 10-3.2 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.)
 CC   =>     * `  Re `  -  _i  x.  Im `
 
Theoremcjcjd 9131 The conjugate of the conjugate is the original complex number. Proposition 10-3.4(e) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
 CC   =>     * `  * `
 
Theoremreim0bd 9132 A number is real iff its imaginary part is 0. (Contributed by Mario Carneiro, 29-May-2016.)
 CC   &     Im `  0   =>     RR
 
Theoremrerebd 9133 A real number equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
 CC   &     Re `    =>     RR
 
Theoremcjrebd 9134 A number is real iff it equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
 CC   &     * `    =>     RR
 
Theoremcjne0d 9135 A number is nonzero iff its complex conjugate is nonzero. (Contributed by Mario Carneiro, 29-May-2016.)
 CC   &     =/=  0   =>     * `  =/=  0
 
Theoremrecjd 9136 Real part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
 CC   =>     Re `  * `  Re `
 
Theoremimcjd 9137 Imaginary part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
 CC   =>     Im `  * `  -u Im `
 
Theoremcjmulrcld 9138 A complex number times its conjugate is real. (Contributed by Mario Carneiro, 29-May-2016.)
 CC   =>     x.  * `  RR
 
Theoremcjmulvald 9139 A complex number times its conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
 CC   =>     x.  * `  Re `  ^ 2  +  Im
 `  ^
 2
 
Theoremcjmulge0d 9140 A complex number times its conjugate is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.)
 CC   =>     0  <_  x.  * `
 
Theoremrenegd 9141 Real part of negative. (Contributed by Mario Carneiro, 29-May-2016.)
 CC   =>     Re `  -u  -u Re `
 
Theoremimnegd 9142 Imaginary part of negative. (Contributed by Mario Carneiro, 29-May-2016.)
 CC   =>     Im `  -u  -u Im `
 
Theoremcjnegd 9143 Complex conjugate of negative. (Contributed by Mario Carneiro, 29-May-2016.)
 CC   =>     * `  -u  -u * `
 
Theoremaddcjd 9144 A number plus its conjugate is twice its real part. Compare Proposition 10-3.4(h) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
 CC   =>     +  * `  2  x.  Re
 `
 
Theoremcjexpd 9145 Complex conjugate of positive integer exponentiation. (Contributed by Mario Carneiro, 29-May-2016.)
 CC   &     N  NN0   =>     * `  ^ N  * `  ^ N
 
Theoremreaddd 9146 Real part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.)
 CC   &     CC   =>     Re `  +  Re `  +  Re `
 
Theoremimaddd 9147 Imaginary part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.)
 CC   &     CC   =>     Im `  +  Im `  +  Im `
 
Theoremresubd 9148 Real part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.)
 CC   &     CC   =>     Re `  -  Re `  -  Re `
 
Theoremimsubd 9149 Imaginary part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.)
 CC   &     CC   =>     Im `  -  Im `  -  Im `
 
Theoremremuld 9150 Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
 CC   &     CC   =>     Re `  x.  Re `  x.  Re ` 
 -  Im
 `  x.  Im `
 
Theoremimmuld 9151 Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
 CC   &     CC   =>     Im `  x.  Re `  x.  Im `  +  Im
 `  x.  Re `
 
Theoremcjaddd 9152 Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
 CC   &     CC   =>     * `  +  * `  +  * `
 
Theoremcjmuld 9153 Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
 CC   &     CC   =>     * `  x.  * `  x.  * `
 
Theoremipcnd 9154 Standard inner product on complex numbers. (Contributed by Mario Carneiro, 29-May-2016.)
 CC   &     CC   =>     Re `  x.  * `  Re `  x.  Re `  +  Im
 `  x.  Im `
 
Theoremcjdivapd 9155 Complex conjugate distributes over division. (Contributed by Jim Kingdon, 15-Jun-2020.)
 CC   &     CC   &    #  0   =>     * `  * `  * `
 
Theoremrered 9156 A real number equals its real part. One direction of Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
 RR   =>     Re `
 
Theoremreim0d 9157 The imaginary part of a real number is 0. (Contributed by Mario Carneiro, 29-May-2016.)
 RR   =>     Im `  0
 
Theoremcjred 9158 A real number equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
 RR   =>     * `
 
Theoremremul2d 9159 Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
 RR   &     CC   =>     Re `  x.  x.  Re
 `
 
Theoremimmul2d 9160 Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
 RR   &     CC   =>     Im `  x.  x.  Im
 `
 
Theoremredivapd 9161 Real part of a division. Related to remul2 9061. (Contributed by Jim Kingdon, 15-Jun-2020.)
 RR   &     CC   &    #  0   =>     Re `  Re `
 
Theoremimdivapd 9162 Imaginary part of a division. Related to remul2 9061. (Contributed by Jim Kingdon, 15-Jun-2020.)
 RR   &     CC   &    #  0   =>     Im `  Im `
 
Theoremcrred 9163 The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.)
 RR   &     RR   =>     Re `  +  _i  x.
 
Theoremcrimd 9164 The imaginary part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.)
 RR   &     RR   =>     Im `  +  _i  x.
 
PART 4  GUIDES AND MISCELLANEA
 
4.1  Guides (conventions, explanations, and examples)
 
4.1.1  Conventions

This section describes the conventions we use. However, these conventions often refer to existing mathematical practices, which are discussed in more detail in other references. The following sources lay out how mathematics is developed without the law of the excluded middle. Of course, there are a greater number of sources which assume excluded middle and most of what is in them applies here too (especially in a treatment such as ours which is built on first order logic and set theory, rather than, say, type theory). Studying how a topic is treated in the Metamath Proof Explorer and the references therein is often a good place to start (and is easy to compare with the Intuitionistic Logic Explorer). The textbooks provide a motivation for what we are doing, whereas Metamath lets you see in detail all hidden and implicit steps. Most standard theorems are accompanied by citations. Some closely followed texts include the following:

  • Axioms of propositional calculus - Stanford Encyclopedia of Philosophy or [Heyting].
  • Axioms of predicate calculus - our axioms are adapted from the ones in the Metamath Proof Explorer.
  • Theorems of propositional calculus - [Heyting].
  • Theorems of pure predicate calculus - Metamath Proof Explorer.
  • Theorems of equality and substitution - Metamath Proof Explorer.
  • Axioms of set theory - [Crosilla].
  • Development of set theory - Chapter 10 of [HoTT].
  • Construction of real and complex numbers - Chapter 11 of [HoTT]; [BauerTaylor].
  • Theorems about real numbers - [Geuvers].
 
Theoremconventions 9165 Unless there is a reason to diverge, we follow the conventions of the Metamath Proof Explorer (aka "set.mm"). This list of conventions is intended to be read in conjunction with the corresponding conventions in the Metamath Proof Explorer, and only the differences are described below.

  • Minimizing axioms and the axiom of choice. We prefer proofs that depend on fewer and/or weaker axioms, even if the proofs are longer. In particular, our choice of IZF (Intuitionistic Zermelo-Fraenkel) over CZF (Constructive Zermelo-Fraenkel, a weaker system) was just an expedient choice because IZF is easier to formalize in metamath. You can find some development using CZF in BJ's mathbox starting at ax-bd0 9202 (and the section header just above it). As for the axiom of choice, the full axiom of choice implies excluded middle as seen at acexmid 5454, although some authors will use countable choice or dependent choice. For example, countable choice or excluded middle is needed to show that the Cauchy reals coincide with the Dedekind reals - Corollary 11.4.3 of [HoTT], p. (varies).
  • Junk/undefined results. Much of the discussion of this topic in the Metamath Proof Explorer applies except that certain techniques are not available to us. For example, the Metamath Proof Explorer will often say "if a function is evaluated within its domain, a certain result follows; if the function is evaluated outside its domain, the same result follows. Since the function must be evaluated within its domain or outside it, the result follows unconditionally" (the use of excluded middle in this argument is perhaps obvious when stated this way). For this reason, we generally need to prove we are evaluating functions within their domains and avoid the reverse closure theorems of the Metamath Proof Explorer.
  • Bibliography references. The bibliography for the Intuitionistic Logic Explorer is separate from the one for the Metamath Proof Explorer but feel free to copy-paste a citation in either direction in order to cite it.

Label naming conventions

Here are a few of the label naming conventions:

  • Suffixes. We follow the conventions of the Metamath Proof Explorer with a few additions. A biconditional in set.mm which is an implication in iset.mm should have a "r" (for the reverse direction), or "i"/"im" (for the forward direction) appended. A theorem in set.mm which has a decidability condition added should add "dc" to the theorem name. A theorem in set.mm where "nonempty class" is changed to "inhabited class" should add "m" (for member) to the theorem name.

The following table shows some commonly-used abbreviations in labels which are not found in the Metamath Proof Explorer, in alphabetical order. For each abbreviation we provide a mnenomic to help you remember it, the source theorem/assumption defining it, an expression showing what it looks like, whether or not it is a "syntax fragment" (an abbreviation that indicates a particular kind of syntax), and hyperlinks to label examples that use the abbreviation. The abbreviation is bolded if there is a df-NAME definition but the label fragment is not NAME.

AbbreviationMnenomicSource ExpressionSyntax?Example(s)
apapart df-ap 7326 Yes apadd1 7352, apne 7367

  • Community. The Metamath mailing list also covers the Intuitionistic Logic Explorer and is at: https://groups.google.com/forum/#!forum/metamath.
  • (Contributed by Jim Kingdon, 24-Feb-2020.)

       =>   
     
    PART 5  SUPPLEMENTARY MATERIAL (USER'S MATHBOXES)
     
    5.1  Mathboxes for user contributions
     
    5.1.1  Mathbox guidelines
     
    Theoremmathbox 9166 (This theorem is a dummy placeholder for these guidelines. The name of this theorem, "mathbox", is hard-coded into the Metamath program to identify the start of the mathbox section for web page generation.)

    A "mathbox" is a user-contributed section that is maintained by its contributor independently from the main part of set.mm.

    For contributors:

    By making a contribution, you agree to release it into the public domain, according to the statement at the beginning of set.mm.

    Mathboxes are provided to help keep your work synchronized with changes in set.mm, but they shouldn't be depended on as a permanent archive. If you want to preserve your original contribution, it is your responsibility to keep your own copy of it along with the version of set.mm that works with it.

    Guidelines:

    1. If at all possible, please use only 0-ary class constants for new definitions.

    2. Try to follow the style of the rest of set.mm. Each $p and $a statement must be immediately preceded with the comment that will be shown on its web page description. The metamath program command "write source set.mm /rewrap" will take care of wrapping comment lines and indentation conventions. All mathbox content will be on public display and should hopefully reflect the overall quality of the website.

    3. Before submitting a revised mathbox, please make sure it verifies against the current set.mm.

    4. Mathboxes should be independent i.e. the proofs should verify with all other mathboxes removed. If you need a theorem from another mathbox, that is fine (and encouraged), but let me know, so I can move the theorem to the main section. One way avoid undesired accidental use of other mathbox theorems is to develop your mathbox using a modified set.mm that has mathboxes removed.

    Notes:

    1. We may decide to move some theorems to the main part of set.mm for general use.

    2. We may make changes to mathboxes to maintain the overall quality of set.mm. Normally we will let you know if a change might impact what you are working on.

    3. If you use theorems from another user's mathbox, we don't provide assurance that they are based on correct or consistent $a statements. (If you find such a problem, please let us know so it can be corrected.) (Contributed by NM, 20-Feb-2007.) (New usage is discouraged.)

     
    5.2  Mathbox for Mykola Mostovenko
     
    Theoremax1hfs 9167 Heyting's formal system Axiom #1 from [Heyting] p. 127. (Contributed by MM, 11-Aug-2018.)
     
    5.3  Mathbox for BJ
     
    5.3.1  Propositional calculus
     
    Theoremnnexmid 9168 Double negation of excluded middle. Intuitionistic logic refutes the negation of excluded middle (but, of course, does not prove excluded middle) for any formula. (Contributed by BJ, 9-Oct-2019.)
     
    Theoremnndc 9169 Double negation of decidability of a formula. Intuitionistic logic refutes undecidability (but, of course, does not prove decidability) of any formula. (Contributed by BJ, 9-Oct-2019.)
    DECID
     
    Theoremdcdc 9170 Decidability of a proposition is decidable if and only if that proposition is decidable. DECID is idempotent. (Contributed by BJ, 9-Oct-2019.)
    DECID DECID DECID
     
    5.3.2  Predicate calculus
     
    Theorembj-ex 9171* Existential generalization. (Contributed by BJ, 8-Dec-2019.) Proof modification is discouraged because there are shorter proofs, but using less basic results (like exlimiv 1486 and 19.9ht 1529 or 19.23ht 1383). (Proof modification is discouraged.)
     
    Theorembj-hbalt 9172 Closed form of hbal 1363 (copied from set.mm). (Contributed by BJ, 2-May-2019.)
     
    Theorembj-nfalt 9173 Closed form of nfal 1465 (copied from set.mm). (Contributed by BJ, 2-May-2019.)
     F/  F/
     
    Theoremspimd 9174 Deduction form of spim 1623. (Contributed by BJ, 17-Oct-2019.)
     F/   &       =>   
     
    Theorem2spim 9175* Double substitution, as in spim 1623. (Contributed by BJ, 17-Oct-2019.)
     F/   &     F/   &     t    =>   
     
    Theoremch2var 9176* Implicit substitution of for and  t for into a theorem. (Contributed by BJ, 17-Oct-2019.)
     F/   &     F/   &     t    &       =>   
     
    Theoremch2varv 9177* Version of ch2var 9176 with non-freeness hypotheses replaced by DV conditions. (Contributed by BJ, 17-Oct-2019.)
     t    &       =>   
     
    Theorembj-exlimmp 9178 Lemma for bj-vtoclgf 9184. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
     F/   &       =>   
     
    Theorembj-exlimmpi 9179 Lemma for bj-vtoclgf 9184. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
     F/   &       &       =>   
     
    Theorembj-sbimedh 9180 A strengthening of sbiedh 1667 (same proof). (Contributed by BJ, 16-Dec-2019.)
       &       &       =>   
     
    Theorembj-sbimeh 9181 A strengthening of sbieh 1670 (same proof). (Contributed by BJ, 16-Dec-2019.)
       &       =>   
     
    Theorembj-sbime 9182 A strengthening of sbie 1671 (same proof). (Contributed by BJ, 16-Dec-2019.)
     F/   &       =>   
     
    5.3.3  Extensionality

    Various utility theorems using FOL and extensionality.

     
    Theorembj-vtoclgft 9183 Weakening two hypotheses of vtoclgf 2606. (Contributed by BJ, 21-Nov-2019.)
     F/_   &    
 F/   &       =>     V
     
    Theorembj-vtoclgf 9184 Weakening two hypotheses of vtoclgf 2606. (Contributed by BJ, 21-Nov-2019.)
     F/_   &    
 F/   &       &       =>     V
     
    Theoremelabgf0 9185 Lemma for elabgf 2679. (Contributed by BJ, 21-Nov-2019.)
     {  |  }
     
    Theoremelabgft1 9186 One implication of elabgf 2679, in closed form. (Contributed by BJ, 21-Nov-2019.)
     F/_   &    
 F/   =>     {  |  }
     
    Theoremelabgf1 9187 One implication of elabgf 2679. (Contributed by BJ, 21-Nov-2019.)
     F/_   &    
 F/   &       =>     {  |  }
     
    Theoremelabgf2 9188 One implication of elabgf 2679. (Contributed by BJ, 21-Nov-2019.)
     F/_   &    
 F/   &       =>     {  |  }
     
    Theoremelabf1 9189* One implication of elabf 2680. (Contributed by BJ, 21-Nov-2019.)
     F/   &       =>     {  |  }
     
    Theoremelabf2 9190* One implication of elabf 2680. (Contributed by BJ, 21-Nov-2019.)
     F/   &     _V   &       =>     {  |  }
     
    Theoremelab1 9191* One implication of elab 2681. (Contributed by BJ, 21-Nov-2019.)
       =>     {  |  }
     
    Theoremelab2a 9192* One implication of elab 2681. (Contributed by BJ, 21-Nov-2019.)
     _V   &       =>     {  |  }
     
    Theoremelabg2 9193* One implication of elabg 2682. (Contributed by BJ, 21-Nov-2019.)
       =>     V  {  |  }
     
    Theorembj-rspgt 9194 Restricted specialization, generalized. Weakens a hypothesis of rspccv 2647 and seems to have a shorter proof. (Contributed by BJ, 21-Nov-2019.)
     F/_   &     F/_   &     F/   =>   
     
    Theorembj-rspg 9195 Restricted specialization, generalized. Weakens a hypothesis of rspccv 2647 and seems to have a shorter proof. (Contributed by BJ, 21-Nov-2019.)
     F/_   &     F/_   &     F/   &       =>   
     
    Theoremcbvrald 9196* Rule used to change bound variables, using implicit substitution. (Contributed by BJ, 22-Nov-2019.)
     F/   &     F/   &     F/   &     F/   &       =>   
     
    Theorembj-intabssel 9197 Version of intss1 3621 using a class abstraction and explicit substitution. (Contributed by BJ, 29-Nov-2019.)
     F/_   =>     V  [.  ].  |^| {  |  }  C_
     
    Theorembj-intabssel1 9198 Version of intss1 3621 using a class abstraction and implicit substitution. Closed form of intmin3 3633. (Contributed by BJ, 29-Nov-2019.)
     F/_   &    
 F/   &       =>     V  |^| {  |  }  C_
     
    Theorembj-elssuniab 9199 Version of elssuni 3599 using a class abstraction and explicit substitution. (Contributed by BJ, 29-Nov-2019.)
     F/_   =>     V  [.  ].  C_  U.
 {  |  }
     
    Theorembj-sseq 9200 If two converse inclusions are characterized each by a formula, then equality is characterized by the conjunction of these formulas. (Contributed by BJ, 30-Nov-2019.)
     C_    &     C_    =>   
        < Previous  Next >

    Page List
    Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9381
      Copyright terms: Public domain < Previous  Next >