Home | New
Foundations Explorer Theorem List (p. 25 of 64) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > NFE Home Page > Theorem List Contents This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | syl6eq 2401 | An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.) |
⊢ (φ → A = B) & ⊢ B = C ⇒ ⊢ (φ → A = C) | ||
Theorem | syl6req 2402 | An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.) |
⊢ (φ → A = B) & ⊢ B = C ⇒ ⊢ (φ → C = A) | ||
Theorem | syl6eqr 2403 | An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.) |
⊢ (φ → A = B) & ⊢ C = B ⇒ ⊢ (φ → A = C) | ||
Theorem | syl6reqr 2404 | An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.) |
⊢ (φ → A = B) & ⊢ C = B ⇒ ⊢ (φ → C = A) | ||
Theorem | sylan9eq 2405 | An equality transitivity deduction. (Contributed by NM, 8-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ (φ → A = B) & ⊢ (ψ → B = C) ⇒ ⊢ ((φ ∧ ψ) → A = C) | ||
Theorem | sylan9req 2406 | An equality transitivity deduction. (Contributed by NM, 23-Jun-2007.) |
⊢ (φ → B = A) & ⊢ (ψ → B = C) ⇒ ⊢ ((φ ∧ ψ) → A = C) | ||
Theorem | sylan9eqr 2407 | An equality transitivity deduction. (Contributed by NM, 8-May-1994.) |
⊢ (φ → A = B) & ⊢ (ψ → B = C) ⇒ ⊢ ((ψ ∧ φ) → A = C) | ||
Theorem | 3eqtr3g 2408 | A chained equality inference, useful for converting from definitions. (Contributed by NM, 15-Nov-1994.) |
⊢ (φ → A = B) & ⊢ A = C & ⊢ B = D ⇒ ⊢ (φ → C = D) | ||
Theorem | 3eqtr3a 2409 | A chained equality inference, useful for converting from definitions. (Contributed by Mario Carneiro, 6-Nov-2015.) |
⊢ A = B & ⊢ (φ → A = C) & ⊢ (φ → B = D) ⇒ ⊢ (φ → C = D) | ||
Theorem | 3eqtr4g 2410 | A chained equality inference, useful for converting to definitions. (Contributed by NM, 5-Aug-1993.) |
⊢ (φ → A = B) & ⊢ C = A & ⊢ D = B ⇒ ⊢ (φ → C = D) | ||
Theorem | 3eqtr4a 2411 | A chained equality inference, useful for converting to definitions. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ A = B & ⊢ (φ → C = A) & ⊢ (φ → D = B) ⇒ ⊢ (φ → C = D) | ||
Theorem | eq2tri 2412 | A compound transitive inference for class equality. (Contributed by NM, 22-Jan-2004.) |
⊢ (A = C → D = F) & ⊢ (B = D → C = G) ⇒ ⊢ ((A = C ∧ B = F) ↔ (B = D ∧ A = G)) | ||
Theorem | eleq1 2413 | Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.) |
⊢ (A = B → (A ∈ C ↔ B ∈ C)) | ||
Theorem | eleq2 2414 | Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.) |
⊢ (A = B → (C ∈ A ↔ C ∈ B)) | ||
Theorem | eleq12 2415 | Equality implies equivalence of membership. (Contributed by NM, 31-May-1999.) |
⊢ ((A = B ∧ C = D) → (A ∈ C ↔ B ∈ D)) | ||
Theorem | eleq1i 2416 | Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.) |
⊢ A = B ⇒ ⊢ (A ∈ C ↔ B ∈ C) | ||
Theorem | eleq2i 2417 | Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.) |
⊢ A = B ⇒ ⊢ (C ∈ A ↔ C ∈ B) | ||
Theorem | eleq12i 2418 | Inference from equality to equivalence of membership. (Contributed by NM, 31-May-1994.) |
⊢ A = B & ⊢ C = D ⇒ ⊢ (A ∈ C ↔ B ∈ D) | ||
Theorem | eleq1d 2419 | Deduction from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.) |
⊢ (φ → A = B) ⇒ ⊢ (φ → (A ∈ C ↔ B ∈ C)) | ||
Theorem | eleq2d 2420 | Deduction from equality to equivalence of membership. (Contributed by NM, 27-Dec-1993.) |
⊢ (φ → A = B) ⇒ ⊢ (φ → (C ∈ A ↔ C ∈ B)) | ||
Theorem | eleq12d 2421 | Deduction from equality to equivalence of membership. (Contributed by NM, 31-May-1994.) |
⊢ (φ → A = B) & ⊢ (φ → C = D) ⇒ ⊢ (φ → (A ∈ C ↔ B ∈ D)) | ||
Theorem | eleq1a 2422 | A transitive-type law relating membership and equality. (Contributed by NM, 9-Apr-1994.) |
⊢ (A ∈ B → (C = A → C ∈ B)) | ||
Theorem | eqeltri 2423 | Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.) |
⊢ A = B & ⊢ B ∈ C ⇒ ⊢ A ∈ C | ||
Theorem | eqeltrri 2424 | Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.) |
⊢ A = B & ⊢ A ∈ C ⇒ ⊢ B ∈ C | ||
Theorem | eleqtri 2425 | Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.) |
⊢ A ∈ B & ⊢ B = C ⇒ ⊢ A ∈ C | ||
Theorem | eleqtrri 2426 | Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.) |
⊢ A ∈ B & ⊢ C = B ⇒ ⊢ A ∈ C | ||
Theorem | eqeltrd 2427 | Substitution of equal classes into membership relation, deduction form. (Contributed by Raph Levien, 10-Dec-2002.) |
⊢ (φ → A = B) & ⊢ (φ → B ∈ C) ⇒ ⊢ (φ → A ∈ C) | ||
Theorem | eqeltrrd 2428 | Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.) |
⊢ (φ → A = B) & ⊢ (φ → A ∈ C) ⇒ ⊢ (φ → B ∈ C) | ||
Theorem | eleqtrd 2429 | Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.) |
⊢ (φ → A ∈ B) & ⊢ (φ → B = C) ⇒ ⊢ (φ → A ∈ C) | ||
Theorem | eleqtrrd 2430 | Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.) |
⊢ (φ → A ∈ B) & ⊢ (φ → C = B) ⇒ ⊢ (φ → A ∈ C) | ||
Theorem | 3eltr3i 2431 | Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ A ∈ B & ⊢ A = C & ⊢ B = D ⇒ ⊢ C ∈ D | ||
Theorem | 3eltr4i 2432 | Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ A ∈ B & ⊢ C = A & ⊢ D = B ⇒ ⊢ C ∈ D | ||
Theorem | 3eltr3d 2433 | Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (φ → A ∈ B) & ⊢ (φ → A = C) & ⊢ (φ → B = D) ⇒ ⊢ (φ → C ∈ D) | ||
Theorem | 3eltr4d 2434 | Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (φ → A ∈ B) & ⊢ (φ → C = A) & ⊢ (φ → D = B) ⇒ ⊢ (φ → C ∈ D) | ||
Theorem | 3eltr3g 2435 | Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (φ → A ∈ B) & ⊢ A = C & ⊢ B = D ⇒ ⊢ (φ → C ∈ D) | ||
Theorem | 3eltr4g 2436 | Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.) |
⊢ (φ → A ∈ B) & ⊢ C = A & ⊢ D = B ⇒ ⊢ (φ → C ∈ D) | ||
Theorem | syl5eqel 2437 | B membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
⊢ A = B & ⊢ (φ → B ∈ C) ⇒ ⊢ (φ → A ∈ C) | ||
Theorem | syl5eqelr 2438 | B membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
⊢ B = A & ⊢ (φ → B ∈ C) ⇒ ⊢ (φ → A ∈ C) | ||
Theorem | syl5eleq 2439 | B membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
⊢ A ∈ B & ⊢ (φ → B = C) ⇒ ⊢ (φ → A ∈ C) | ||
Theorem | syl5eleqr 2440 | B membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
⊢ A ∈ B & ⊢ (φ → C = B) ⇒ ⊢ (φ → A ∈ C) | ||
Theorem | syl6eqel 2441 | A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
⊢ (φ → A = B) & ⊢ B ∈ C ⇒ ⊢ (φ → A ∈ C) | ||
Theorem | syl6eqelr 2442 | A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
⊢ (φ → B = A) & ⊢ B ∈ C ⇒ ⊢ (φ → A ∈ C) | ||
Theorem | syl6eleq 2443 | A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
⊢ (φ → A ∈ B) & ⊢ B = C ⇒ ⊢ (φ → A ∈ C) | ||
Theorem | syl6eleqr 2444 | A membership and equality inference. (Contributed by NM, 24-Apr-2005.) |
⊢ (φ → A ∈ B) & ⊢ C = B ⇒ ⊢ (φ → A ∈ C) | ||
Theorem | eleq2s 2445 | Substitution of equal classes into a membership antecedent. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ (A ∈ B → φ) & ⊢ C = B ⇒ ⊢ (A ∈ C → φ) | ||
Theorem | eqneltrd 2446 | 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.) |
⊢ (φ → A = B) & ⊢ (φ → ¬ B ∈ C) ⇒ ⊢ (φ → ¬ A ∈ C) | ||
Theorem | eqneltrrd 2447 | 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.) |
⊢ (φ → A = B) & ⊢ (φ → ¬ A ∈ C) ⇒ ⊢ (φ → ¬ B ∈ C) | ||
Theorem | neleqtrd 2448 | 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.) |
⊢ (φ → ¬ C ∈ A) & ⊢ (φ → A = B) ⇒ ⊢ (φ → ¬ C ∈ B) | ||
Theorem | neleqtrrd 2449 | 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.) |
⊢ (φ → ¬ C ∈ B) & ⊢ (φ → A = B) ⇒ ⊢ (φ → ¬ C ∈ A) | ||
Theorem | cleqh 2450* | Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 5-Aug-1993.) |
⊢ (y ∈ A → ∀x y ∈ A) & ⊢ (y ∈ B → ∀x y ∈ B) ⇒ ⊢ (A = B ↔ ∀x(x ∈ A ↔ x ∈ B)) | ||
Theorem | nelneq 2451 | A way of showing two classes are not equal. (Contributed by NM, 1-Apr-1997.) |
⊢ ((A ∈ C ∧ ¬ B ∈ C) → ¬ A = B) | ||
Theorem | nelneq2 2452 | A way of showing two classes are not equal. (Contributed by NM, 12-Jan-2002.) |
⊢ ((A ∈ B ∧ ¬ A ∈ C) → ¬ B = C) | ||
Theorem | eqsb3lem 2453* | Lemma for eqsb3 2454. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) |
⊢ ([y / x]x = A ↔ y = A) | ||
Theorem | eqsb3 2454* | Substitution applied to an atomic wff (class version of equsb3 2102). (Contributed by Rodolfo Medina, 28-Apr-2010.) |
⊢ ([y / x]x = A ↔ y = A) | ||
Theorem | clelsb3 2455* | Substitution applied to an atomic wff (class version of elsb3 2103). (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) |
⊢ ([y / x]x ∈ A ↔ y ∈ A) | ||
Theorem | hbxfreq 2456 | A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfrbi 1568 for equivalence version. (Contributed by NM, 21-Aug-2007.) |
⊢ A = B & ⊢ (y ∈ B → ∀x y ∈ B) ⇒ ⊢ (y ∈ A → ∀x y ∈ A) | ||
Theorem | hblem 2457* | Change the free variable of a hypothesis builder. Lemma for nfcrii 2482. (Contributed by NM, 5-Aug-1993.) (Revised by Andrew Salmon, 11-Jul-2011.) |
⊢ (y ∈ A → ∀x y ∈ A) ⇒ ⊢ (z ∈ A → ∀x z ∈ A) | ||
Theorem | abeq2 2458* |
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 2463 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 x) to a theorem with a class variable A, we substitute x ∈ A for φ throughout and simplify, where A is a new class variable not already in the wff. An example is the conversion of zfauscl in set.mm to inex1 in set.mm (look at the instance of zfauscl that occurs in the proof of inex1 ). Conversely, to convert a theorem with a class variable A to one with φ, we substitute {x ∣ φ} for A throughout and simplify, where x and φ are new setvar and wff variables not already in the wff. An example is cp in set.mm , which derives a formula containing wff variables from substitution instances of the class variables in its equivalent formulation cplem2 in set.mm. 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.) |
⊢ (A = {x ∣ φ} ↔ ∀x(x ∈ A ↔ φ)) | ||
Theorem | abeq1 2459* | Equality of a class variable and a class abstraction. (Contributed by NM, 20-Aug-1993.) |
⊢ ({x ∣ φ} = A ↔ ∀x(φ ↔ x ∈ A)) | ||
Theorem | abeq2i 2460 | Equality of a class variable and a class abstraction (inference rule). (Contributed by NM, 3-Apr-1996.) |
⊢ A = {x ∣ φ} ⇒ ⊢ (x ∈ A ↔ φ) | ||
Theorem | abeq1i 2461 | Equality of a class variable and a class abstraction (inference rule). (Contributed by NM, 31-Jul-1994.) |
⊢ {x ∣ φ} = A ⇒ ⊢ (φ ↔ x ∈ A) | ||
Theorem | abeq2d 2462 | Equality of a class variable and a class abstraction (deduction). (Contributed by NM, 16-Nov-1995.) |
⊢ (φ → A = {x ∣ ψ}) ⇒ ⊢ (φ → (x ∈ A ↔ ψ)) | ||
Theorem | abbi 2463 | Equivalent wff's correspond to equal class abstractions. (Contributed by NM, 25-Nov-2013.) (Revised by Mario Carneiro, 11-Aug-2016.) |
⊢ (∀x(φ ↔ ψ) ↔ {x ∣ φ} = {x ∣ ψ}) | ||
Theorem | abbi2i 2464* | Equality of a class variable and a class abstraction (inference rule). (Contributed by NM, 5-Aug-1993.) |
⊢ (x ∈ A ↔ φ) ⇒ ⊢ A = {x ∣ φ} | ||
Theorem | abbii 2465 | Equivalent wff's yield equal class abstractions (inference rule). (Contributed by NM, 5-Aug-1993.) |
⊢ (φ ↔ ψ) ⇒ ⊢ {x ∣ φ} = {x ∣ ψ} | ||
Theorem | abbid 2466 | Equivalent wff's yield equal class abstractions (deduction rule). (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 7-Oct-2016.) |
⊢ Ⅎxφ & ⊢ (φ → (ψ ↔ χ)) ⇒ ⊢ (φ → {x ∣ ψ} = {x ∣ χ}) | ||
Theorem | abbidv 2467* | Equivalent wff's yield equal class abstractions (deduction rule). (Contributed by NM, 10-Aug-1993.) |
⊢ (φ → (ψ ↔ χ)) ⇒ ⊢ (φ → {x ∣ ψ} = {x ∣ χ}) | ||
Theorem | abbi2dv 2468* | Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.) |
⊢ (φ → (x ∈ A ↔ ψ)) ⇒ ⊢ (φ → A = {x ∣ ψ}) | ||
Theorem | abbi1dv 2469* | Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.) |
⊢ (φ → (ψ ↔ x ∈ A)) ⇒ ⊢ (φ → {x ∣ ψ} = A) | ||
Theorem | abid2 2470* | A simplification of class abstraction. Theorem 5.2 of [Quine] p. 35. (Contributed by NM, 26-Dec-1993.) |
⊢ {x ∣ x ∈ A} = A | ||
Theorem | cbvab 2471 | Rule used to change bound variables, using implicit substitution. (Contributed by Andrew Salmon, 11-Jul-2011.) |
⊢ Ⅎyφ & ⊢ Ⅎxψ & ⊢ (x = y → (φ ↔ ψ)) ⇒ ⊢ {x ∣ φ} = {y ∣ ψ} | ||
Theorem | cbvabv 2472* | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 26-May-1999.) |
⊢ (x = y → (φ ↔ ψ)) ⇒ ⊢ {x ∣ φ} = {y ∣ ψ} | ||
Theorem | clelab 2473* | Membership of a class variable in a class abstraction. (Contributed by NM, 23-Dec-1993.) |
⊢ (A ∈ {x ∣ φ} ↔ ∃x(x = A ∧ φ)) | ||
Theorem | clabel 2474* | Membership of a class abstraction in another class. (Contributed by NM, 17-Jan-2006.) |
⊢ ({x ∣ φ} ∈ A ↔ ∃y(y ∈ A ∧ ∀x(x ∈ y ↔ φ))) | ||
Theorem | sbab 2475* | The right-hand side of the second equality is a way of representing proper substitution of y for x into a class variable. (Contributed by NM, 14-Sep-2003.) |
⊢ (x = y → A = {z ∣ [y / x]z ∈ A}) | ||
Syntax | wnfc 2476 | Extend wff definition to include the not-free predicate for classes. |
wff ℲxA | ||
Theorem | nfcjust 2477* | Justification theorem for df-nfc 2478. (Contributed by Mario Carneiro, 13-Oct-2016.) |
⊢ (∀yℲx y ∈ A ↔ ∀zℲx z ∈ A) | ||
Definition | df-nfc 2478* | Define the not-free predicate for classes. This is read "x is not free in A". Not-free means that the value of x cannot affect the value of A, e.g., any occurrence of x in A is effectively bound by a "for all" or something that expands to one (such as "there exists"). It is defined in terms of the not-free predicate df-nf 1545 for wffs; see that definition for more information. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ (ℲxA ↔ ∀yℲx y ∈ A) | ||
Theorem | nfci 2479* | Deduce that a class A does not have x free in it. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎx y ∈ A ⇒ ⊢ ℲxA | ||
Theorem | nfcii 2480* | Deduce that a class A does not have x free in it. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ (y ∈ A → ∀x y ∈ A) ⇒ ⊢ ℲxA | ||
Theorem | nfcr 2481* | Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ (ℲxA → Ⅎx y ∈ A) | ||
Theorem | nfcrii 2482* | Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ ℲxA ⇒ ⊢ (y ∈ A → ∀x y ∈ A) | ||
Theorem | nfcri 2483* | Consequence of the not-free predicate. (Note that unlike nfcr 2481, this does not require y and A to be disjoint.) (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ ℲxA ⇒ ⊢ Ⅎx y ∈ A | ||
Theorem | nfcd 2484* | Deduce that a class A does not have x free in it. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎyφ & ⊢ (φ → Ⅎx y ∈ A) ⇒ ⊢ (φ → ℲxA) | ||
Theorem | nfceqi 2485 | Equality theorem for class not-free. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ A = B ⇒ ⊢ (ℲxA ↔ ℲxB) | ||
Theorem | nfcxfr 2486 | A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ A = B & ⊢ ℲxB ⇒ ⊢ ℲxA | ||
Theorem | nfcxfrd 2487 | A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ A = B & ⊢ (φ → ℲxB) ⇒ ⊢ (φ → ℲxA) | ||
Theorem | nfceqdf 2488 | An equality theorem for effectively not free. (Contributed by Mario Carneiro, 14-Oct-2016.) |
⊢ Ⅎxφ & ⊢ (φ → A = B) ⇒ ⊢ (φ → (ℲxA ↔ ℲxB)) | ||
Theorem | nfcv 2489* | If x is disjoint from A, then x is not free in A. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ ℲxA | ||
Theorem | nfcvd 2490* | If x is disjoint from A, then x is not free in A. (Contributed by Mario Carneiro, 7-Oct-2016.) |
⊢ (φ → ℲxA) | ||
Theorem | nfab1 2491 | Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎx{x ∣ φ} | ||
Theorem | nfnfc1 2492 | x is bound in ℲxA. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ ℲxℲxA | ||
Theorem | nfab 2493 | Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎxφ ⇒ ⊢ Ⅎx{y ∣ φ} | ||
Theorem | nfaba1 2494 | Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 14-Oct-2016.) |
⊢ Ⅎx{y ∣ ∀xφ} | ||
Theorem | nfnfc 2495 | Hypothesis builder for ℲyA. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ ℲxA ⇒ ⊢ ℲxℲyA | ||
Theorem | nfeq 2496 | Hypothesis builder for equality. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ ℲxA & ⊢ ℲxB ⇒ ⊢ Ⅎx A = B | ||
Theorem | nfel 2497 | Hypothesis builder for elementhood. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ ℲxA & ⊢ ℲxB ⇒ ⊢ Ⅎx A ∈ B | ||
Theorem | nfeq1 2498* | Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.) |
⊢ ℲxA ⇒ ⊢ Ⅎx A = B | ||
Theorem | nfel1 2499* | Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.) |
⊢ ℲxA ⇒ ⊢ Ⅎx A ∈ B | ||
Theorem | nfeq2 2500* | Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.) |
⊢ ℲxB ⇒ ⊢ Ⅎx A = B |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |