Home | Metamath
Proof ExplorerTheorem List
(p. 290 of 322)
| < Previous Next > |

Browser slow? Try the
Unicode version. |

Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs

Color key: | Metamath Proof Explorer
(1-21498) |
Hilbert Space Explorer
(21499-23021) |
Users' Mathboxes
(23022-32154) |

Type | Label | Description |
---|---|---|

Statement | ||

Theorem | bnj118 28901* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |

Theorem | bnj121 28902* | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |

Theorem | bnj124 28903* | Technical lemma for bnj150 28908. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.) |

Theorem | bnj125 28904* | Technical lemma for bnj150 28908. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |

Theorem | bnj126 28905* | Technical lemma for bnj150 28908. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |

Theorem | bnj130 28906* | Technical lemma for bnj151 28909. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |

Theorem | bnj149 28907* | Technical lemma for bnj151 28909. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.) |

Theorem | bnj150 28908* | Technical lemma for bnj151 28909. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |

Theorem | bnj151 28909* | Technical lemma for bnj153 28912. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |

Theorem | bnj154 28910* | Technical lemma for bnj153 28912. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |

Theorem | bnj155 28911* | Technical lemma for bnj153 28912. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |

Theorem | bnj153 28912* | Technical lemma for bnj852 28953. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |

Theorem | bnj207 28913* | Technical lemma for bnj852 28953. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |

Theorem | bnj213 28914 | First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |

Theorem | bnj222 28915* | Technical lemma for bnj229 28916. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |

Theorem | bnj229 28916* | Technical lemma for bnj517 28917. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |

Theorem | bnj517 28917* | Technical lemma for bnj518 28918. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.) |

Theorem | bnj518 28918* | Technical lemma for bnj852 28953. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |

Theorem | bnj523 28919* | |

Theorem | bnj526 28920* | |

Theorem | bnj528 28921 | |

Theorem | bnj535 28922* | |

Theorem | bnj539 28923* | |

Theorem | bnj540 28924* | |

Theorem | bnj543 28925* | |

Theorem | bnj544 28926* | |

Theorem | bnj545 28927 | |

Theorem | bnj546 28928* | |

Theorem | bnj548 28929* | |

Theorem | bnj553 28930* | |

Theorem | bnj554 28931* | |

Theorem | bnj556 28932 | |

Theorem | bnj557 28933* | |

Theorem | bnj558 28934* | |

Theorem | bnj561 28935 | |

Theorem | bnj562 28936 | |

Theorem | bnj570 28937* | |

Theorem | bnj571 28938* | |

Theorem | bnj605 28939* | Technical lemma. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |

Theorem | bnj581 28940* | Technical lemma for bnj580 28945. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Unnecessary distinct variable restrictions were removed by Andrew Salmon, 9-Jul-2011.) (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |

Theorem | bnj589 28941* | |

Theorem | bnj590 28942 | |

Theorem | bnj591 28943* | |

Theorem | bnj594 28944* | |

Theorem | bnj580 28945* | Technical lemma for bnj579 28946. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |

Theorem | bnj579 28946* | |

Theorem | bnj602 28947 | Equality theorem for the function constant. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |

Theorem | bnj607 28948* | |

Theorem | bnj609 28949* | |

Theorem | bnj611 28950* | |

Theorem | bnj600 28951* | |

Theorem | bnj601 28952* | |

Theorem | bnj852 28953* | Technical lemma for bnj69 29040. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |

Theorem | bnj864 28954* | Technical lemma for bnj69 29040. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |

Theorem | bnj865 28955* | Technical lemma for bnj69 29040. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |

Theorem | bnj873 28956* | |

Theorem | bnj849 28957* | Technical lemma for bnj69 29040. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.) |

Theorem | bnj882 28958* | Definition (using hypotheses for readability) of the function giving the transitive closure of in by . (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |

Theorem | bnj18eq1 28959 | Equality theorem for transitive closure. (Contributed by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.) |

Theorem | bnj893 28960 | Property of . Under certain conditions, the transitive closure of in by is a set. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |

Theorem | bnj900 28961* | |

Theorem | bnj906 28962 | Property of . (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |

Theorem | bnj908 28963* | |

Theorem | bnj911 28964* | |

Theorem | bnj916 28965* | |

Theorem | bnj917 28966* | |

Theorem | bnj934 28967* | |

Theorem | bnj929 28968* | |

Theorem | bnj938 28969* | |

Theorem | bnj944 28970* | |

Theorem | bnj953 28971 | |

Theorem | bnj958 28972* | |

Theorem | bnj1000 28973* | |

Theorem | bnj965 28974* | |

Theorem | bnj964 28975* | |

Theorem | bnj966 28976* | |

Theorem | bnj967 28977* | |

Theorem | bnj969 28978* | |

Theorem | bnj970 28979 | |

Theorem | bnj910 28980* | |

Theorem | bnj978 28981* | |

Theorem | bnj981 28982* | |

Theorem | bnj983 28983* | |

Theorem | bnj984 28984 | |

Theorem | bnj985 28985* | |

Theorem | bnj986 28986* | |

Theorem | bnj996 28987* | |

Theorem | bnj998 28988* | |

Theorem | bnj999 28989* | |

Theorem | bnj1001 28990 | |

Theorem | bnj1006 28991* | |

Theorem | bnj1014 28992* | |

Theorem | bnj1015 28993* | |

Theorem | bnj1018 28994* | |

Theorem | bnj1020 28995* | |

Theorem | bnj1021 28996* | |

Theorem | bnj907 28997* | |

Theorem | bnj1029 28998 | Property of . (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |

Theorem | bnj1033 28999* | |

Theorem | bnj1034 29000* | |

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |