Home | Intuitionistic Logic Explorer Theorem List (p. 23 of 132) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 3eltr4d 2201 | Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐴) & ⊢ (𝜑 → 𝐷 = 𝐵) ⇒ ⊢ (𝜑 → 𝐶 ∈ 𝐷) | ||
Theorem | 3eltr3g 2202 | Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ 𝐴 = 𝐶 & ⊢ 𝐵 = 𝐷 ⇒ ⊢ (𝜑 → 𝐶 ∈ 𝐷) | ||
Theorem | 3eltr4g 2203 | Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ 𝐶 = 𝐴 & ⊢ 𝐷 = 𝐵 ⇒ ⊢ (𝜑 → 𝐶 ∈ 𝐷) | ||
Theorem | eqeltrid 2204 | B membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
⊢ 𝐴 = 𝐵 & ⊢ (𝜑 → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐶) | ||
Theorem | eqeltrrid 2205 | B membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
⊢ 𝐵 = 𝐴 & ⊢ (𝜑 → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐶) | ||
Theorem | eleqtrid 2206 | B membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
⊢ 𝐴 ∈ 𝐵 & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐶) | ||
Theorem | eleqtrrid 2207 | B membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
⊢ 𝐴 ∈ 𝐵 & ⊢ (𝜑 → 𝐶 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐶) | ||
Theorem | syl6eqel 2208 | A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ 𝐵 ∈ 𝐶 ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐶) | ||
Theorem | syl6eqelr 2209 | A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
⊢ (𝜑 → 𝐵 = 𝐴) & ⊢ 𝐵 ∈ 𝐶 ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐶) | ||
Theorem | eleqtrdi 2210 | A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ 𝐵 = 𝐶 ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐶) | ||
Theorem | eleqtrrdi 2211 | A membership and equality inference. (Contributed by NM, 24-Apr-2005.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ 𝐶 = 𝐵 ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐶) | ||
Theorem | eleq2s 2212 | Substitution of equal classes into a membership antecedent. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ (𝐴 ∈ 𝐵 → 𝜑) & ⊢ 𝐶 = 𝐵 ⇒ ⊢ (𝐴 ∈ 𝐶 → 𝜑) | ||
Theorem | eqneltrd 2213 | If a class is not an element of another class, an equal class is also not an element. Deduction form. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → ¬ 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶) | ||
Theorem | eqneltrrd 2214 | If a class is not an element of another class, an equal class is also not an element. Deduction form. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶) ⇒ ⊢ (𝜑 → ¬ 𝐵 ∈ 𝐶) | ||
Theorem | neleqtrd 2215 | If a class is not an element of another class, it is also not an element of an equal class. Deduction form. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐵) | ||
Theorem | neleqtrrd 2216 | If a class is not an element of another class, it is also not an element of an equal class. Deduction form. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → ¬ 𝐶 ∈ 𝐵) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴) | ||
Theorem | cleqh 2217* | Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions. See also cleqf 2282. (Contributed by NM, 5-Aug-1993.) |
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) & ⊢ (𝑦 ∈ 𝐵 → ∀𝑥 𝑦 ∈ 𝐵) ⇒ ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | ||
Theorem | nelneq 2218 | A way of showing two classes are not equal. (Contributed by NM, 1-Apr-1997.) |
⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → ¬ 𝐴 = 𝐵) | ||
Theorem | nelneq2 2219 | A way of showing two classes are not equal. (Contributed by NM, 12-Jan-2002.) |
⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → ¬ 𝐵 = 𝐶) | ||
Theorem | eqsb3lem 2220* | Lemma for eqsb3 2221. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) |
⊢ ([𝑦 / 𝑥]𝑥 = 𝐴 ↔ 𝑦 = 𝐴) | ||
Theorem | eqsb3 2221* | Substitution applied to an atomic wff (class version of equsb3 1902). (Contributed by Rodolfo Medina, 28-Apr-2010.) |
⊢ ([𝑦 / 𝑥]𝑥 = 𝐴 ↔ 𝑦 = 𝐴) | ||
Theorem | clelsb3 2222* | Substitution applied to an atomic wff (class version of elsb3 1929). (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) |
⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴) | ||
Theorem | clelsb4 2223* | Substitution applied to an atomic wff (class version of elsb4 1930). (Contributed by Jim Kingdon, 22-Nov-2018.) |
⊢ ([𝑦 / 𝑥]𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦) | ||
Theorem | hbxfreq 2224 | A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfrbi 1433 for equivalence version. (Contributed by NM, 21-Aug-2007.) |
⊢ 𝐴 = 𝐵 & ⊢ (𝑦 ∈ 𝐵 → ∀𝑥 𝑦 ∈ 𝐵) ⇒ ⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) | ||
Theorem | hblem 2225* | Change the free variable of a hypothesis builder. (Contributed by NM, 5-Aug-1993.) (Revised by Andrew Salmon, 11-Jul-2011.) |
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) ⇒ ⊢ (𝑧 ∈ 𝐴 → ∀𝑥 𝑧 ∈ 𝐴) | ||
Theorem | abeq2 2226* |
Equality of a class variable and a class abstraction (also called a
class builder). Theorem 5.1 of [Quine] p.
34. This theorem shows the
relationship between expressions with class abstractions and expressions
with class variables. Note that abbi 2231 and its relatives are among
those useful for converting theorems with class variables to equivalent
theorems with wff variables, by first substituting a class abstraction
for each class variable.
Class variables can always be eliminated from a theorem to result in an equivalent theorem with wff variables, and vice-versa. The idea is roughly as follows. To convert a theorem with a wff variable 𝜑 (that has a free variable 𝑥) to a theorem with a class variable 𝐴, we substitute 𝑥 ∈ 𝐴 for 𝜑 throughout and simplify, where 𝐴 is a new class variable not already in the wff. Conversely, to convert a theorem with a class variable 𝐴 to one with 𝜑, we substitute {𝑥 ∣ 𝜑} for 𝐴 throughout and simplify, where 𝑥 and 𝜑 are new set and wff variables not already in the wff. For more information on class variables, see Quine pp. 15-21 and/or Takeuti and Zaring pp. 10-13. (Contributed by NM, 5-Aug-1993.) |
⊢ (𝐴 = {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝜑)) | ||
Theorem | abeq1 2227* | Equality of a class variable and a class abstraction. (Contributed by NM, 20-Aug-1993.) |
⊢ ({𝑥 ∣ 𝜑} = 𝐴 ↔ ∀𝑥(𝜑 ↔ 𝑥 ∈ 𝐴)) | ||
Theorem | abeq2i 2228 | Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 3-Apr-1996.) |
⊢ 𝐴 = {𝑥 ∣ 𝜑} ⇒ ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑) | ||
Theorem | abeq1i 2229 | Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 31-Jul-1994.) |
⊢ {𝑥 ∣ 𝜑} = 𝐴 ⇒ ⊢ (𝜑 ↔ 𝑥 ∈ 𝐴) | ||
Theorem | abeq2d 2230 | Equality of a class variable and a class abstraction (deduction). (Contributed by NM, 16-Nov-1995.) |
⊢ (𝜑 → 𝐴 = {𝑥 ∣ 𝜓}) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝜓)) | ||
Theorem | abbi 2231 | Equivalent wff's correspond to equal class abstractions. (Contributed by NM, 25-Nov-2013.) (Revised by Mario Carneiro, 11-Aug-2016.) |
⊢ (∀𝑥(𝜑 ↔ 𝜓) ↔ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓}) | ||
Theorem | abbi2i 2232* | Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 5-Aug-1993.) |
⊢ (𝑥 ∈ 𝐴 ↔ 𝜑) ⇒ ⊢ 𝐴 = {𝑥 ∣ 𝜑} | ||
Theorem | abbii 2233 | Equivalent wff's yield equal class abstractions (inference form). (Contributed by NM, 5-Aug-1993.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓} | ||
Theorem | abbid 2234 | Equivalent wff's yield equal class abstractions (deduction form). (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 7-Oct-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒}) | ||
Theorem | abbidv 2235* | Equivalent wff's yield equal class abstractions (deduction form). (Contributed by NM, 10-Aug-1993.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒}) | ||
Theorem | abbi2dv 2236* | Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝜓)) ⇒ ⊢ (𝜑 → 𝐴 = {𝑥 ∣ 𝜓}) | ||
Theorem | abbi1dv 2237* | Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.) |
⊢ (𝜑 → (𝜓 ↔ 𝑥 ∈ 𝐴)) ⇒ ⊢ (𝜑 → {𝑥 ∣ 𝜓} = 𝐴) | ||
Theorem | abid2 2238* | A simplification of class abstraction. Theorem 5.2 of [Quine] p. 35. (Contributed by NM, 26-Dec-1993.) |
⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴 | ||
Theorem | sb8ab 2239 | Substitution of variable in class abstraction. (Contributed by Jim Kingdon, 27-Sep-2018.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ [𝑦 / 𝑥]𝜑} | ||
Theorem | cbvab 2240 | Rule used to change bound variables, using implicit substitution. (Contributed by Andrew Salmon, 11-Jul-2011.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓} | ||
Theorem | cbvabv 2241* | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 26-May-1999.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓} | ||
Theorem | clelab 2242* | Membership of a class variable in a class abstraction. (Contributed by NM, 23-Dec-1993.) |
⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) | ||
Theorem | clabel 2243* | Membership of a class abstraction in another class. (Contributed by NM, 17-Jan-2006.) |
⊢ ({𝑥 ∣ 𝜑} ∈ 𝐴 ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ ∀𝑥(𝑥 ∈ 𝑦 ↔ 𝜑))) | ||
Theorem | sbab 2244* | The right-hand side of the second equality is a way of representing proper substitution of 𝑦 for 𝑥 into a class variable. (Contributed by NM, 14-Sep-2003.) |
⊢ (𝑥 = 𝑦 → 𝐴 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐴}) | ||
Syntax | wnfc 2245 | Extend wff definition to include the not-free predicate for classes. |
wff Ⅎ𝑥𝐴 | ||
Theorem | nfcjust 2246* | Justification theorem for df-nfc 2247. (Contributed by Mario Carneiro, 13-Oct-2016.) |
⊢ (∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴 ↔ ∀𝑧Ⅎ𝑥 𝑧 ∈ 𝐴) | ||
Definition | df-nfc 2247* | Define the not-free predicate for classes. This is read "𝑥 is not free in 𝐴". Not-free means that the value of 𝑥 cannot affect the value of 𝐴, e.g., any occurrence of 𝑥 in 𝐴 is effectively bound by a quantifier or something that expands to one (such as "there exists at most one"). It is defined in terms of the not-free predicate df-nf 1422 for wffs; see that definition for more information. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴) | ||
Theorem | nfci 2248* | Deduce that a class 𝐴 does not have 𝑥 free in it. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 ⇒ ⊢ Ⅎ𝑥𝐴 | ||
Theorem | nfcii 2249* | Deduce that a class 𝐴 does not have 𝑥 free in it. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) ⇒ ⊢ Ⅎ𝑥𝐴 | ||
Theorem | nfcr 2250* | Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ (Ⅎ𝑥𝐴 → Ⅎ𝑥 𝑦 ∈ 𝐴) | ||
Theorem | nfcrii 2251* | Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) | ||
Theorem | nfcri 2252* | Consequence of the not-free predicate. (Note that unlike nfcr 2250, this does not require 𝑦 and 𝐴 to be disjoint.) (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 | ||
Theorem | nfcd 2253* | Deduce that a class 𝐴 does not have 𝑥 free in it. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥𝐴) | ||
Theorem | nfceqi 2254 | Equality theorem for class not-free. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (Ⅎ𝑥𝐴 ↔ Ⅎ𝑥𝐵) | ||
Theorem | nfcxfr 2255 | A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ 𝐴 = 𝐵 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥𝐴 | ||
Theorem | nfcxfrd 2256 | A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ 𝐴 = 𝐵 & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥𝐴) | ||
Theorem | nfceqdf 2257 | An equality theorem for effectively not free. (Contributed by Mario Carneiro, 14-Oct-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (Ⅎ𝑥𝐴 ↔ Ⅎ𝑥𝐵)) | ||
Theorem | nfcv 2258* | If 𝑥 is disjoint from 𝐴, then 𝑥 is not free in 𝐴. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑥𝐴 | ||
Theorem | nfcvd 2259* | If 𝑥 is disjoint from 𝐴, then 𝑥 is not free in 𝐴. (Contributed by Mario Carneiro, 7-Oct-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) | ||
Theorem | nfab1 2260 | Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑥{𝑥 ∣ 𝜑} | ||
Theorem | nfnfc1 2261 | 𝑥 is bound in Ⅎ𝑥𝐴. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑥Ⅎ𝑥𝐴 | ||
Theorem | clelsb3f 2262 | Substitution applied to an atomic wff (class version of elsb3 1929). (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (Revised by Thierry Arnoux, 13-Mar-2017.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴) | ||
Theorem | nfab 2263 | Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥{𝑦 ∣ 𝜑} | ||
Theorem | nfaba1 2264 | Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 14-Oct-2016.) |
⊢ Ⅎ𝑥{𝑦 ∣ ∀𝑥𝜑} | ||
Theorem | nfnfc 2265 | Hypothesis builder for Ⅎ𝑦𝐴. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥Ⅎ𝑦𝐴 | ||
Theorem | nfeq 2266 | Hypothesis builder for equality. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐴 = 𝐵 | ||
Theorem | nfel 2267 | Hypothesis builder for elementhood. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵 | ||
Theorem | nfeq1 2268* | Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝐴 = 𝐵 | ||
Theorem | nfel1 2269* | Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵 | ||
Theorem | nfeq2 2270* | Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.) |
⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐴 = 𝐵 | ||
Theorem | nfel2 2271* | Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.) |
⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵 | ||
Theorem | nfcrd 2272* | Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐴) | ||
Theorem | nfeqd 2273 | Hypothesis builder for equality. (Contributed by Mario Carneiro, 7-Oct-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥 𝐴 = 𝐵) | ||
Theorem | nfeld 2274 | Hypothesis builder for elementhood. (Contributed by Mario Carneiro, 7-Oct-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥 𝐴 ∈ 𝐵) | ||
Theorem | drnfc1 2275 | Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 8-Oct-2016.) |
⊢ (∀𝑥 𝑥 = 𝑦 → 𝐴 = 𝐵) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑥𝐴 ↔ Ⅎ𝑦𝐵)) | ||
Theorem | drnfc2 2276 | Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 8-Oct-2016.) |
⊢ (∀𝑥 𝑥 = 𝑦 → 𝐴 = 𝐵) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑧𝐴 ↔ Ⅎ𝑧𝐵)) | ||
Theorem | nfabd 2277 | Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 8-Oct-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥{𝑦 ∣ 𝜓}) | ||
Theorem | dvelimdc 2278 | Deduction form of dvelimc 2279. (Contributed by Mario Carneiro, 8-Oct-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑧𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑧𝐵) & ⊢ (𝜑 → (𝑧 = 𝑦 → 𝐴 = 𝐵)) ⇒ ⊢ (𝜑 → (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝐵)) | ||
Theorem | dvelimc 2279 | Version of dvelim 1970 for classes. (Contributed by Mario Carneiro, 8-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑧𝐵 & ⊢ (𝑧 = 𝑦 → 𝐴 = 𝐵) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝐵) | ||
Theorem | nfcvf 2280 | If 𝑥 and 𝑦 are distinct, then 𝑥 is not free in 𝑦. (Contributed by Mario Carneiro, 8-Oct-2016.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦) | ||
Theorem | nfcvf2 2281 | If 𝑥 and 𝑦 are distinct, then 𝑦 is not free in 𝑥. (Contributed by Mario Carneiro, 5-Dec-2016.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑥) | ||
Theorem | cleqf 2282 | Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions. See also cleqh 2217. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 7-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | ||
Theorem | abid2f 2283 | A simplification of class abstraction. Theorem 5.2 of [Quine] p. 35. (Contributed by NM, 5-Sep-2011.) (Revised by Mario Carneiro, 7-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴 | ||
Theorem | sbabel 2284* | Theorem to move a substitution in and out of a class abstraction. (Contributed by NM, 27-Sep-2003.) (Revised by Mario Carneiro, 7-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ ([𝑦 / 𝑥]{𝑧 ∣ 𝜑} ∈ 𝐴 ↔ {𝑧 ∣ [𝑦 / 𝑥]𝜑} ∈ 𝐴) | ||
Syntax | wne 2285 | Extend wff notation to include inequality. |
wff 𝐴 ≠ 𝐵 | ||
Definition | df-ne 2286 | Define inequality. (Contributed by NM, 5-Aug-1993.) |
⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | ||
Theorem | neii 2287 | Inference associated with df-ne 2286. (Contributed by BJ, 7-Jul-2018.) |
⊢ 𝐴 ≠ 𝐵 ⇒ ⊢ ¬ 𝐴 = 𝐵 | ||
Theorem | neir 2288 | Inference associated with df-ne 2286. (Contributed by BJ, 7-Jul-2018.) |
⊢ ¬ 𝐴 = 𝐵 ⇒ ⊢ 𝐴 ≠ 𝐵 | ||
Theorem | nner 2289 | Negation of inequality. (Contributed by Jim Kingdon, 23-Dec-2018.) |
⊢ (𝐴 = 𝐵 → ¬ 𝐴 ≠ 𝐵) | ||
Theorem | nnedc 2290 | Negation of inequality where equality is decidable. (Contributed by Jim Kingdon, 15-May-2018.) |
⊢ (DECID 𝐴 = 𝐵 → (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵)) | ||
Theorem | dcned 2291 | Decidable equality implies decidable negated equality. (Contributed by Jim Kingdon, 3-May-2020.) |
⊢ (𝜑 → DECID 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → DECID 𝐴 ≠ 𝐵) | ||
Theorem | neqned 2292 | If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2306. One-way deduction form of df-ne 2286. (Contributed by David Moews, 28-Feb-2017.) Allow a shortening of necon3bi 2335. (Revised by Wolf Lammen, 22-Nov-2019.) |
⊢ (𝜑 → ¬ 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) | ||
Theorem | neqne 2293 | From non-equality to inequality. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (¬ 𝐴 = 𝐵 → 𝐴 ≠ 𝐵) | ||
Theorem | neirr 2294 | No class is unequal to itself. (Contributed by Stefan O'Rear, 1-Jan-2015.) (Proof rewritten by Jim Kingdon, 15-May-2018.) |
⊢ ¬ 𝐴 ≠ 𝐴 | ||
Theorem | eqneqall 2295 | A contradiction concerning equality implies anything. (Contributed by Alexander van der Vekens, 25-Jan-2018.) |
⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝜑)) | ||
Theorem | dcne 2296 | Decidable equality expressed in terms of ≠. Basically the same as df-dc 805. (Contributed by Jim Kingdon, 14-Mar-2020.) |
⊢ (DECID 𝐴 = 𝐵 ↔ (𝐴 = 𝐵 ∨ 𝐴 ≠ 𝐵)) | ||
Theorem | nonconne 2297 | Law of noncontradiction with equality and inequality. (Contributed by NM, 3-Feb-2012.) |
⊢ ¬ (𝐴 = 𝐵 ∧ 𝐴 ≠ 𝐵) | ||
Theorem | neeq1 2298 | Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.) |
⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶)) | ||
Theorem | neeq2 2299 | Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.) |
⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵)) | ||
Theorem | neeq1i 2300 | Inference for inequality. (Contributed by NM, 29-Apr-2005.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |