Home | Metamath
Proof Explorer Theorem List (p. 44 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | n0f 4301 | A class is nonempty if and only if it has at least one element. Proposition 5.17(1) of [TakeutiZaring] p. 20. This version of n0 4305 requires only that 𝑥 not be free in, rather than not occur in, 𝐴. (Contributed by NM, 17-Oct-2003.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴) | ||
Theorem | eq0 4302* | A class is equal to the empty set if and only if it has no elements. Theorem 2 of [Suppes] p. 22. (Contributed by NM, 29-Aug-1993.) Avoid ax-11 2155, ax-12 2172. (Revised by Gino Giotto and Steven Nguyen, 28-Jun-2024.) Avoid ax-8 2109, df-clel 2816. (Revised by Gino Giotto, 6-Sep-2024.) |
⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴) | ||
Theorem | eq0ALT 4303* | Alternate proof of eq0 4302. Shorter, but requiring df-clel 2816, ax-8 2109. (Contributed by NM, 29-Aug-1993.) Avoid ax-11 2155, ax-12 2172. (Revised by Gino Giotto and Steven Nguyen, 28-Jun-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴) | ||
Theorem | neq0 4304* | A class is not empty if and only if it has at least one element. Proposition 5.17(1) of [TakeutiZaring] p. 20. (Contributed by NM, 21-Jun-1993.) Avoid ax-11 2155, ax-12 2172. (Revised by Gino Giotto, 28-Jun-2024.) |
⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴) | ||
Theorem | n0 4305* | A class is nonempty if and only if it has at least one element. Proposition 5.17(1) of [TakeutiZaring] p. 20. (Contributed by NM, 29-Sep-2006.) Avoid ax-11 2155, ax-12 2172. (Revised by Gino Giotto, 28-Jun-2024.) |
⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴) | ||
Theorem | eq0OLDOLD 4306* | Obsolete version of eq0 4302 as of 28-Jun-2024. (Contributed by NM, 29-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴) | ||
Theorem | neq0OLD 4307* | Obsolete version of neq0 4304 as of 28-Jun-2024. (Contributed by NM, 21-Jun-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴) | ||
Theorem | n0OLD 4308* | Obsolete version of n0 4305 as of 28-Jun-2024. (Contributed by NM, 29-Sep-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴) | ||
Theorem | nel0 4309* | From the general negation of membership in 𝐴, infer that 𝐴 is the empty set. (Contributed by BJ, 6-Oct-2018.) |
⊢ ¬ 𝑥 ∈ 𝐴 ⇒ ⊢ 𝐴 = ∅ | ||
Theorem | reximdva0 4310* | Restricted existence deduced from nonempty class. (Contributed by NM, 1-Feb-2012.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓) ⇒ ⊢ ((𝜑 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 𝜓) | ||
Theorem | rspn0 4311* | Specialization for restricted generalization with a nonempty class. (Contributed by Alexander van der Vekens, 6-Sep-2018.) Avoid ax-10 2138, ax-12 2172. (Revised by Gino Giotto, 28-Jun-2024.) |
⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 𝜑 → 𝜑)) | ||
Theorem | rspn0OLD 4312* | Obsolete version of rspn0 4311 as of 28-Jun-2024. (Contributed by Alexander van der Vekens, 6-Sep-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 𝜑 → 𝜑)) | ||
Theorem | n0rex 4313* | There is an element in a nonempty class which is an element of the class. (Contributed by AV, 17-Dec-2020.) |
⊢ (𝐴 ≠ ∅ → ∃𝑥 ∈ 𝐴 𝑥 ∈ 𝐴) | ||
Theorem | ssn0rex 4314* | There is an element in a class with a nonempty subclass which is an element of the subclass. (Contributed by AV, 17-Dec-2020.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐵 𝑥 ∈ 𝐴) | ||
Theorem | n0moeu 4315* | A case of equivalence of "at most one" and "only one". (Contributed by FL, 6-Dec-2010.) |
⊢ (𝐴 ≠ ∅ → (∃*𝑥 𝑥 ∈ 𝐴 ↔ ∃!𝑥 𝑥 ∈ 𝐴)) | ||
Theorem | rex0 4316 | Vacuous restricted existential quantification is false. (Contributed by NM, 15-Oct-2003.) |
⊢ ¬ ∃𝑥 ∈ ∅ 𝜑 | ||
Theorem | reu0 4317 | Vacuous restricted uniqueness is always false. (Contributed by AV, 3-Apr-2023.) |
⊢ ¬ ∃!𝑥 ∈ ∅ 𝜑 | ||
Theorem | rmo0 4318 | Vacuous restricted at-most-one quantifier is always true. (Contributed by AV, 3-Apr-2023.) |
⊢ ∃*𝑥 ∈ ∅ 𝜑 | ||
Theorem | 0el 4319* | Membership of the empty set in another class. (Contributed by NM, 29-Jun-2004.) |
⊢ (∅ ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ¬ 𝑦 ∈ 𝑥) | ||
Theorem | n0el 4320* | Negated membership of the empty set in another class. (Contributed by Rodolfo Medina, 25-Sep-2010.) |
⊢ (¬ ∅ ∈ 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃𝑢 𝑢 ∈ 𝑥) | ||
Theorem | eqeuel 4321* | A condition which implies the existence of a unique element of a class. (Contributed by AV, 4-Jan-2022.) |
⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → 𝑥 = 𝑦)) → ∃!𝑥 𝑥 ∈ 𝐴) | ||
Theorem | ssdif0 4322 | Subclass expressed in terms of difference. Exercise 7 of [TakeutiZaring] p. 22. (Contributed by NM, 29-Apr-1994.) |
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∖ 𝐵) = ∅) | ||
Theorem | difn0 4323 | If the difference of two sets is not empty, then the sets are not equal. (Contributed by Thierry Arnoux, 28-Feb-2017.) |
⊢ ((𝐴 ∖ 𝐵) ≠ ∅ → 𝐴 ≠ 𝐵) | ||
Theorem | pssdifn0 4324 | A proper subclass has a nonempty difference. (Contributed by NM, 3-May-1994.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵) → (𝐵 ∖ 𝐴) ≠ ∅) | ||
Theorem | pssdif 4325 | A proper subclass has a nonempty difference. (Contributed by Mario Carneiro, 27-Apr-2016.) |
⊢ (𝐴 ⊊ 𝐵 → (𝐵 ∖ 𝐴) ≠ ∅) | ||
Theorem | ndisj 4326* | Express that an intersection is not empty. (Contributed by RP, 16-Apr-2020.) |
⊢ ((𝐴 ∩ 𝐵) ≠ ∅ ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) | ||
Theorem | difin0ss 4327 | Difference, intersection, and subclass relationship. (Contributed by NM, 30-Apr-1994.) (Proof shortened by Wolf Lammen, 30-Sep-2014.) |
⊢ (((𝐴 ∖ 𝐵) ∩ 𝐶) = ∅ → (𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵)) | ||
Theorem | inssdif0 4328 | Intersection, subclass, and difference relationship. (Contributed by NM, 27-Oct-1996.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) (Proof shortened by Wolf Lammen, 30-Sep-2014.) |
⊢ ((𝐴 ∩ 𝐵) ⊆ 𝐶 ↔ (𝐴 ∩ (𝐵 ∖ 𝐶)) = ∅) | ||
Theorem | difid 4329 | The difference between a class and itself is the empty set. Proposition 5.15 of [TakeutiZaring] p. 20. Also Theorem 32 of [Suppes] p. 28. (Contributed by NM, 22-Apr-2004.) (Revised by David Abernethy, 17-Jun-2012.) |
⊢ (𝐴 ∖ 𝐴) = ∅ | ||
Theorem | difidALT 4330 | Alternate proof of difid 4329. Shorter, but requiring ax-8 2109, df-clel 2816. (Contributed by NM, 22-Apr-2004.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∖ 𝐴) = ∅ | ||
Theorem | dif0 4331 | The difference between a class and the empty set. Part of Exercise 4.4 of [Stoll] p. 16. (Contributed by NM, 17-Aug-2004.) |
⊢ (𝐴 ∖ ∅) = 𝐴 | ||
Theorem | ab0w 4332* | The class of sets verifying a property is the empty class if and only if that property is a contradiction. Version of ab0 4333 using implicit substitution, which requires fewer axioms. (Contributed by Gino Giotto, 3-Oct-2024.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ({𝑥 ∣ 𝜑} = ∅ ↔ ∀𝑦 ¬ 𝜓) | ||
Theorem | ab0 4333 | The class of sets verifying a property is the empty class if and only if that property is a contradiction. See also abn0 4339 (from which it could be proved using as many essential proof steps but one fewer syntactic step, at the cost of depending on df-ne 2943). (Contributed by BJ, 19-Mar-2021.) Avoid df-clel 2816, ax-8 2109. (Revised by Gino Giotto, 30-Aug-2024.) (Proof shortened by SN, 8-Sep-2024.) |
⊢ ({𝑥 ∣ 𝜑} = ∅ ↔ ∀𝑥 ¬ 𝜑) | ||
Theorem | ab0OLD 4334 | Obsolete version of ab0 4333 as of 8-Sep-2024. (Contributed by BJ, 19-Mar-2021.) Avoid df-clel 2816, ax-8 2109. (Revised by Gino Giotto, 30-Aug-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ({𝑥 ∣ 𝜑} = ∅ ↔ ∀𝑥 ¬ 𝜑) | ||
Theorem | ab0ALT 4335 | Alternate proof of ab0 4333, shorter but using more axioms. (Contributed by BJ, 19-Mar-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ({𝑥 ∣ 𝜑} = ∅ ↔ ∀𝑥 ¬ 𝜑) | ||
Theorem | dfnf5 4336 | Characterization of nonfreeness in a formula in terms of its extension. (Contributed by BJ, 19-Mar-2021.) |
⊢ (Ⅎ𝑥𝜑 ↔ ({𝑥 ∣ 𝜑} = V ∨ {𝑥 ∣ 𝜑} = ∅)) | ||
Theorem | ab0orv 4337* | The class abstraction defined by a formula not containing the abstraction variable is either the empty set or the universal class. (Contributed by Mario Carneiro, 29-Aug-2013.) (Revised by BJ, 22-Mar-2020.) Reduce axiom usage. (Revised by Gino Giotto, 30-Aug-2024.) |
⊢ ({𝑥 ∣ 𝜑} = V ∨ {𝑥 ∣ 𝜑} = ∅) | ||
Theorem | ab0orvALT 4338* | Alternate proof of ab0orv 4337, shorter but using more axioms. (Contributed by Mario Carneiro, 29-Aug-2013.) (Revised by BJ, 22-Mar-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ({𝑥 ∣ 𝜑} = V ∨ {𝑥 ∣ 𝜑} = ∅) | ||
Theorem | abn0 4339 | Nonempty class abstraction. See also ab0 4333. (Contributed by NM, 26-Dec-1996.) (Proof shortened by Mario Carneiro, 11-Nov-2016.) Avoid df-clel 2816, ax-8 2109. (Revised by Gino Giotto, 30-Aug-2024.) |
⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥𝜑) | ||
Theorem | abn0OLD 4340 | Obsolete version of abn0 4339 as of 30-Aug-2024. (Contributed by NM, 26-Dec-1996.) (Proof shortened by Mario Carneiro, 11-Nov-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥𝜑) | ||
Theorem | rab0 4341 | Any restricted class abstraction restricted to the empty set is empty. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) (Proof shortened by JJ, 14-Jul-2021.) |
⊢ {𝑥 ∈ ∅ ∣ 𝜑} = ∅ | ||
Theorem | rabeq0w 4342* | Condition for a restricted class abstraction to be empty. Version of rabeq0 4343 using implicit substitution, which does not require ax-10 2138, ax-11 2155, ax-12 2172, but requires ax-8 2109. (Contributed by Gino Giotto, 30-Sep-2024.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑦 ∈ 𝐴 ¬ 𝜓) | ||
Theorem | rabeq0 4343 | Condition for a restricted class abstraction to be empty. (Contributed by Jeff Madsen, 7-Jun-2010.) (Revised by BJ, 16-Jul-2021.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑) | ||
Theorem | rabn0 4344 | Nonempty restricted class abstraction. (Contributed by NM, 29-Aug-1999.) (Revised by BJ, 16-Jul-2021.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rabxm 4345* | Law of excluded middle, in terms of restricted class abstractions. (Contributed by Jeff Madsen, 20-Jun-2011.) |
⊢ 𝐴 = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}) | ||
Theorem | rabnc 4346 | Law of noncontradiction, in terms of restricted class abstractions. (Contributed by Jeff Madsen, 20-Jun-2011.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}) = ∅ | ||
Theorem | elneldisj 4347* | The set of elements 𝑠 determining classes 𝐶 (which may depend on 𝑠) containing a special element and the set of elements 𝑠 determining classes 𝐶 not containing the special element are disjoint. (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 9-Nov-2020.) (Revised by AV, 17-Dec-2021.) |
⊢ 𝐸 = {𝑠 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶} & ⊢ 𝑁 = {𝑠 ∈ 𝐴 ∣ 𝐵 ∉ 𝐶} ⇒ ⊢ (𝐸 ∩ 𝑁) = ∅ | ||
Theorem | elnelun 4348* | The union of the set of elements 𝑠 determining classes 𝐶 (which may depend on 𝑠) containing a special element and the set of elements 𝑠 determining classes 𝐶 not containing the special element yields the original set. (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 9-Nov-2020.) (Revised by AV, 17-Dec-2021.) |
⊢ 𝐸 = {𝑠 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶} & ⊢ 𝑁 = {𝑠 ∈ 𝐴 ∣ 𝐵 ∉ 𝐶} ⇒ ⊢ (𝐸 ∪ 𝑁) = 𝐴 | ||
Theorem | un0 4349 | The union of a class with the empty set is itself. Theorem 24 of [Suppes] p. 27. (Contributed by NM, 15-Jul-1993.) |
⊢ (𝐴 ∪ ∅) = 𝐴 | ||
Theorem | in0 4350 | The intersection of a class with the empty set is the empty set. Theorem 16 of [Suppes] p. 26. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝐴 ∩ ∅) = ∅ | ||
Theorem | 0un 4351 | The union of the empty set with a class is itself. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (∅ ∪ 𝐴) = 𝐴 | ||
Theorem | 0in 4352 | The intersection of the empty set with a class is the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (∅ ∩ 𝐴) = ∅ | ||
Theorem | inv1 4353 | The intersection of a class with the universal class is itself. Exercise 4.10(k) of [Mendelson] p. 231. (Contributed by NM, 17-May-1998.) |
⊢ (𝐴 ∩ V) = 𝐴 | ||
Theorem | unv 4354 | The union of a class with the universal class is the universal class. Exercise 4.10(l) of [Mendelson] p. 231. (Contributed by NM, 17-May-1998.) |
⊢ (𝐴 ∪ V) = V | ||
Theorem | 0ss 4355 | The null set is a subset of any class. Part of Exercise 1 of [TakeutiZaring] p. 22. (Contributed by NM, 21-Jun-1993.) |
⊢ ∅ ⊆ 𝐴 | ||
Theorem | ss0b 4356 | Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23 and its converse. (Contributed by NM, 17-Sep-2003.) |
⊢ (𝐴 ⊆ ∅ ↔ 𝐴 = ∅) | ||
Theorem | ss0 4357 | Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23. (Contributed by NM, 13-Aug-1994.) |
⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅) | ||
Theorem | sseq0 4358 | A subclass of an empty class is empty. (Contributed by NM, 7-Mar-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅) | ||
Theorem | ssn0 4359 | A class with a nonempty subclass is nonempty. (Contributed by NM, 17-Feb-2007.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → 𝐵 ≠ ∅) | ||
Theorem | 0dif 4360 | The difference between the empty set and a class. Part of Exercise 4.4 of [Stoll] p. 16. (Contributed by NM, 17-Aug-2004.) |
⊢ (∅ ∖ 𝐴) = ∅ | ||
Theorem | abf 4361 | A class abstraction determined by a false formula is empty. (Contributed by NM, 20-Jan-2012.) Avoid ax-8 2109, ax-10 2138, ax-11 2155, ax-12 2172. (Revised by Gino Giotto, 30-Jun-2024.) |
⊢ ¬ 𝜑 ⇒ ⊢ {𝑥 ∣ 𝜑} = ∅ | ||
Theorem | abfOLD 4362 | Obsolete version of abf 4361 as of 28-Jun-2024. (Contributed by NM, 20-Jan-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ¬ 𝜑 ⇒ ⊢ {𝑥 ∣ 𝜑} = ∅ | ||
Theorem | eq0rdv 4363* | Deduction for equality to the empty set. (Contributed by NM, 11-Jul-2014.) Avoid ax-8 2109, df-clel 2816. (Revised by Gino Giotto, 6-Sep-2024.) |
⊢ (𝜑 → ¬ 𝑥 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 = ∅) | ||
Theorem | eq0rdvALT 4364* | Alternate proof of eq0rdv 4363. Shorter, but requiring df-clel 2816, ax-8 2109. (Contributed by NM, 11-Jul-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → ¬ 𝑥 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 = ∅) | ||
Theorem | csbprc 4365 | The proper substitution of a proper class for a set into a class results in the empty set. (Contributed by NM, 17-Aug-2018.) (Proof shortened by JJ, 27-Aug-2021.) |
⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 = ∅) | ||
Theorem | csb0 4366 | The proper substitution of a class into the empty set is the empty set. (Contributed by NM, 18-Aug-2018.) |
⊢ ⦋𝐴 / 𝑥⦌∅ = ∅ | ||
Theorem | sbcel12 4367 | Distribute proper substitution through a membership relation. (Contributed by NM, 10-Nov-2005.) (Revised by NM, 18-Aug-2018.) |
⊢ ([𝐴 / 𝑥]𝐵 ∈ 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 ∈ ⦋𝐴 / 𝑥⦌𝐶) | ||
Theorem | sbceqg 4368 | Distribute proper substitution through an equality relation. (Contributed by NM, 10-Nov-2005.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)) | ||
Theorem | sbceqi 4369 | Distribution of class substitution over equality, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.) |
⊢ 𝐴 ∈ V & ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐷 & ⊢ ⦋𝐴 / 𝑥⦌𝐶 = 𝐸 ⇒ ⊢ ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ 𝐷 = 𝐸) | ||
Theorem | sbcnel12g 4370 | Distribute proper substitution through negated membership. (Contributed by Andrew Salmon, 18-Jun-2011.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 ∉ 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 ∉ ⦋𝐴 / 𝑥⦌𝐶)) | ||
Theorem | sbcne12 4371 | Distribute proper substitution through an inequality. (Contributed by Andrew Salmon, 18-Jun-2011.) (Revised by NM, 18-Aug-2018.) |
⊢ ([𝐴 / 𝑥]𝐵 ≠ 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 ≠ ⦋𝐴 / 𝑥⦌𝐶) | ||
Theorem | sbcel1g 4372* | Move proper substitution in and out of a membership relation. Note that the scope of [𝐴 / 𝑥] is the wff 𝐵 ∈ 𝐶, whereas the scope of ⦋𝐴 / 𝑥⦌ is the class 𝐵. (Contributed by NM, 10-Nov-2005.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 ∈ 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 ∈ 𝐶)) | ||
Theorem | sbceq1g 4373* | Move proper substitution to first argument of an equality. (Contributed by NM, 30-Nov-2005.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)) | ||
Theorem | sbcel2 4374* | Move proper substitution in and out of a membership relation. (Contributed by NM, 14-Nov-2005.) (Revised by NM, 18-Aug-2018.) |
⊢ ([𝐴 / 𝑥]𝐵 ∈ 𝐶 ↔ 𝐵 ∈ ⦋𝐴 / 𝑥⦌𝐶) | ||
Theorem | sbceq2g 4375* | Move proper substitution to second argument of an equality. (Contributed by NM, 30-Nov-2005.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ 𝐵 = ⦋𝐴 / 𝑥⦌𝐶)) | ||
Theorem | csbcom 4376* | Commutative law for double substitution into a class. (Contributed by NM, 14-Nov-2005.) (Revised by NM, 18-Aug-2018.) |
⊢ ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = ⦋𝐵 / 𝑦⦌⦋𝐴 / 𝑥⦌𝐶 | ||
Theorem | sbcnestgfw 4377* | Nest the composition of two substitutions. Version of sbcnestgf 4382 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by Mario Carneiro, 11-Nov-2016.) Avoid ax-13 2372. (Revised by Gino Giotto, 26-Jan-2024.) |
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑦Ⅎ𝑥𝜑) → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦]𝜑)) | ||
Theorem | csbnestgfw 4378* | Nest the composition of two substitutions. Version of csbnestgf 4383 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by NM, 23-Nov-2005.) Avoid ax-13 2372. (Revised by Gino Giotto, 26-Jan-2024.) |
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑦Ⅎ𝑥𝐶) → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = ⦋⦋𝐴 / 𝑥⦌𝐵 / 𝑦⦌𝐶) | ||
Theorem | sbcnestgw 4379* | Nest the composition of two substitutions. Version of sbcnestg 4384 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by NM, 27-Nov-2005.) Avoid ax-13 2372. (Revised by Gino Giotto, 26-Jan-2024.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦]𝜑)) | ||
Theorem | csbnestgw 4380* | Nest the composition of two substitutions. Version of csbnestg 4385 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by NM, 23-Nov-2005.) Avoid ax-13 2372. (Revised by Gino Giotto, 26-Jan-2024.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = ⦋⦋𝐴 / 𝑥⦌𝐵 / 𝑦⦌𝐶) | ||
Theorem | sbcco3gw 4381* | Composition of two substitutions. Version of sbcco3g 4386 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by NM, 27-Nov-2005.) Avoid ax-13 2372. (Revised by Gino Giotto, 26-Jan-2024.) |
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [𝐶 / 𝑦]𝜑)) | ||
Theorem | sbcnestgf 4382 | Nest the composition of two substitutions. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker sbcnestgfw 4377 when possible. (Contributed by Mario Carneiro, 11-Nov-2016.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑦Ⅎ𝑥𝜑) → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦]𝜑)) | ||
Theorem | csbnestgf 4383 | Nest the composition of two substitutions. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker csbnestgfw 4378 when possible. (Contributed by NM, 23-Nov-2005.) (Proof shortened by Mario Carneiro, 10-Nov-2016.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑦Ⅎ𝑥𝐶) → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = ⦋⦋𝐴 / 𝑥⦌𝐵 / 𝑦⦌𝐶) | ||
Theorem | sbcnestg 4384* | Nest the composition of two substitutions. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker sbcnestgw 4379 when possible. (Contributed by NM, 27-Nov-2005.) (Proof shortened by Mario Carneiro, 11-Nov-2016.) (New usage is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦]𝜑)) | ||
Theorem | csbnestg 4385* | Nest the composition of two substitutions. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker csbnestgw 4380 when possible. (Contributed by NM, 23-Nov-2005.) (Proof shortened by Mario Carneiro, 10-Nov-2016.) (New usage is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = ⦋⦋𝐴 / 𝑥⦌𝐵 / 𝑦⦌𝐶) | ||
Theorem | sbcco3g 4386* | Composition of two substitutions. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker sbcco3gw 4381 when possible. (Contributed by NM, 27-Nov-2005.) (Revised by Mario Carneiro, 11-Nov-2016.) (New usage is discouraged.) |
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [𝐶 / 𝑦]𝜑)) | ||
Theorem | csbco3g 4387* | Composition of two class substitutions. Usage of this theorem is discouraged because it depends on ax-13 2372. (Contributed by NM, 27-Nov-2005.) (Revised by Mario Carneiro, 11-Nov-2016.) (New usage is discouraged.) |
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐷 = ⦋𝐶 / 𝑦⦌𝐷) | ||
Theorem | csbnest1g 4388 | Nest the composition of two substitutions. (Contributed by NM, 23-May-2006.) (Proof shortened by Mario Carneiro, 11-Nov-2016.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑥⦌𝐶 = ⦋⦋𝐴 / 𝑥⦌𝐵 / 𝑥⦌𝐶) | ||
Theorem | csbidm 4389* | Idempotent law for class substitutions. (Contributed by NM, 1-Mar-2008.) (Revised by NM, 18-Aug-2018.) |
⊢ ⦋𝐴 / 𝑥⦌⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵 | ||
Theorem | csbvarg 4390 | The proper substitution of a class for setvar variable results in the class (if the class exists). (Contributed by NM, 10-Nov-2005.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝑥 = 𝐴) | ||
Theorem | csbvargi 4391 | The proper substitution of a class for a setvar variable results in the class (if the class exists), in inference form of csbvarg 4390. (Contributed by Giovanni Mascellani, 30-May-2019.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ⦋𝐴 / 𝑥⦌𝑥 = 𝐴 | ||
Theorem | sbccsb 4392* | Substitution into a wff expressed in terms of substitution into a class. (Contributed by NM, 15-Aug-2007.) (Revised by NM, 18-Aug-2018.) |
⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝜑}) | ||
Theorem | sbccsb2 4393 | Substitution into a wff expressed in using substitution into a class. (Contributed by NM, 27-Nov-2005.) (Revised by NM, 18-Aug-2018.) |
⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ ⦋𝐴 / 𝑥⦌{𝑥 ∣ 𝜑}) | ||
Theorem | rspcsbela 4394* | Special case related to rspsbc 3834. (Contributed by NM, 10-Dec-2005.) (Proof shortened by Eric Schmidt, 17-Jan-2007.) |
⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝐶 ∈ 𝐷) → ⦋𝐴 / 𝑥⦌𝐶 ∈ 𝐷) | ||
Theorem | sbnfc2 4395* | Two ways of expressing "𝑥 is (effectively) not free in 𝐴". (Contributed by Mario Carneiro, 14-Oct-2016.) |
⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦∀𝑧⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑧 / 𝑥⦌𝐴) | ||
Theorem | csbab 4396* | Move substitution into a class abstraction. (Contributed by NM, 13-Dec-2005.) (Revised by NM, 19-Aug-2018.) |
⊢ ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝜑} = {𝑦 ∣ [𝐴 / 𝑥]𝜑} | ||
Theorem | csbun 4397 | Distribution of class substitution over union of two classes. (Contributed by Drahflow, 23-Sep-2015.) (Revised by Mario Carneiro, 11-Dec-2016.) (Revised by NM, 13-Sep-2018.) |
⊢ ⦋𝐴 / 𝑥⦌(𝐵 ∪ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∪ ⦋𝐴 / 𝑥⦌𝐶) | ||
Theorem | csbin 4398 | Distribute proper substitution into a class through an intersection relation. (Contributed by Alan Sare, 22-Jul-2012.) (Revised by NM, 18-Aug-2018.) |
⊢ ⦋𝐴 / 𝑥⦌(𝐵 ∩ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∩ ⦋𝐴 / 𝑥⦌𝐶) | ||
Theorem | csbie2df 4399* | Conversion of implicit substitution to explicit class substitution. This version of csbiedf 3885 avoids a disjointness condition on 𝑥, 𝐴 and 𝑥, 𝐷 by substituting twice. Deduction form of csbie2 3896. (Contributed by AV, 29-Mar-2024.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝐶) & ⊢ (𝜑 → Ⅎ𝑥𝐷) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶) & ⊢ ((𝜑 ∧ 𝑦 = 𝐴) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐷) | ||
Theorem | 2nreu 4400* | If there are two different sets fulfilling a wff (by implicit substitution), then there is no unique set fulfilling the wff. (Contributed by AV, 20-Jun-2023.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) ⇒ ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) → ((𝜓 ∧ 𝜒) → ¬ ∃!𝑥 ∈ 𝑋 𝜑)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |