Home | Metamath
Proof Explorer Theorem List (p. 43 of 465) | < 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-29259) |
Hilbert Space Explorer
(29260-30782) |
Users' Mathboxes
(30783-46465) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ssdifim 4201 | Implication of a class difference with a subclass. (Contributed by AV, 3-Jan-2022.) |
⊢ ((𝐴 ⊆ 𝑉 ∧ 𝐵 = (𝑉 ∖ 𝐴)) → 𝐴 = (𝑉 ∖ 𝐵)) | ||
Theorem | ssdifsym 4202 | Symmetric class differences for subclasses. (Contributed by AV, 3-Jan-2022.) |
⊢ ((𝐴 ⊆ 𝑉 ∧ 𝐵 ⊆ 𝑉) → (𝐵 = (𝑉 ∖ 𝐴) ↔ 𝐴 = (𝑉 ∖ 𝐵))) | ||
Theorem | dfss5 4203* | Alternate definition of subclass relationship: a class 𝐴 is a subclass of another class 𝐵 iff each element of 𝐴 is equal to an element of 𝐵. (Contributed by AV, 13-Nov-2020.) |
⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝑦) | ||
Theorem | dfun3 4204 | Union defined in terms of intersection (De Morgan's law). Definition of union in [Mendelson] p. 231. (Contributed by NM, 8-Jan-2002.) |
⊢ (𝐴 ∪ 𝐵) = (V ∖ ((V ∖ 𝐴) ∩ (V ∖ 𝐵))) | ||
Theorem | dfin3 4205 | Intersection defined in terms of union (De Morgan's law). Similar to Exercise 4.10(n) of [Mendelson] p. 231. (Contributed by NM, 8-Jan-2002.) |
⊢ (𝐴 ∩ 𝐵) = (V ∖ ((V ∖ 𝐴) ∪ (V ∖ 𝐵))) | ||
Theorem | dfin4 4206 | Alternate definition of the intersection of two classes. Exercise 4.10(q) of [Mendelson] p. 231. (Contributed by NM, 25-Nov-2003.) |
⊢ (𝐴 ∩ 𝐵) = (𝐴 ∖ (𝐴 ∖ 𝐵)) | ||
Theorem | invdif 4207 | Intersection with universal complement. Remark in [Stoll] p. 20. (Contributed by NM, 17-Aug-2004.) |
⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵) | ||
Theorem | indif 4208 | Intersection with class difference. Theorem 34 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.) |
⊢ (𝐴 ∩ (𝐴 ∖ 𝐵)) = (𝐴 ∖ 𝐵) | ||
Theorem | indif2 4209 | Bring an intersection in and out of a class difference. (Contributed by Jeff Hankins, 15-Jul-2009.) |
⊢ (𝐴 ∩ (𝐵 ∖ 𝐶)) = ((𝐴 ∩ 𝐵) ∖ 𝐶) | ||
Theorem | indif1 4210 | Bring an intersection in and out of a class difference. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ ((𝐴 ∖ 𝐶) ∩ 𝐵) = ((𝐴 ∩ 𝐵) ∖ 𝐶) | ||
Theorem | indifcom 4211 | Commutation law for intersection and difference. (Contributed by Scott Fenton, 18-Feb-2013.) |
⊢ (𝐴 ∩ (𝐵 ∖ 𝐶)) = (𝐵 ∩ (𝐴 ∖ 𝐶)) | ||
Theorem | indi 4212 | Distributive law for intersection over union. Exercise 10 of [TakeutiZaring] p. 17. (Contributed by NM, 30-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝐴 ∩ (𝐵 ∪ 𝐶)) = ((𝐴 ∩ 𝐵) ∪ (𝐴 ∩ 𝐶)) | ||
Theorem | undi 4213 | Distributive law for union over intersection. Exercise 11 of [TakeutiZaring] p. 17. (Contributed by NM, 30-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝐴 ∪ (𝐵 ∩ 𝐶)) = ((𝐴 ∪ 𝐵) ∩ (𝐴 ∪ 𝐶)) | ||
Theorem | indir 4214 | Distributive law for intersection over union. Theorem 28 of [Suppes] p. 27. (Contributed by NM, 30-Sep-2002.) |
⊢ ((𝐴 ∪ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∪ (𝐵 ∩ 𝐶)) | ||
Theorem | undir 4215 | Distributive law for union over intersection. Theorem 29 of [Suppes] p. 27. (Contributed by NM, 30-Sep-2002.) |
⊢ ((𝐴 ∩ 𝐵) ∪ 𝐶) = ((𝐴 ∪ 𝐶) ∩ (𝐵 ∪ 𝐶)) | ||
Theorem | unineq 4216 | Infer equality from equalities of union and intersection. Exercise 20 of [Enderton] p. 32 and its converse. (Contributed by NM, 10-Aug-2004.) |
⊢ (((𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶) ∧ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)) ↔ 𝐴 = 𝐵) | ||
Theorem | uneqin 4217 | Equality of union and intersection implies equality of their arguments. (Contributed by NM, 16-Apr-2006.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ((𝐴 ∪ 𝐵) = (𝐴 ∩ 𝐵) ↔ 𝐴 = 𝐵) | ||
Theorem | difundi 4218 | Distributive law for class difference. Theorem 39 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.) |
⊢ (𝐴 ∖ (𝐵 ∪ 𝐶)) = ((𝐴 ∖ 𝐵) ∩ (𝐴 ∖ 𝐶)) | ||
Theorem | difundir 4219 | Distributive law for class difference. (Contributed by NM, 17-Aug-2004.) |
⊢ ((𝐴 ∪ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶)) | ||
Theorem | difindi 4220 | Distributive law for class difference. Theorem 40 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.) |
⊢ (𝐴 ∖ (𝐵 ∩ 𝐶)) = ((𝐴 ∖ 𝐵) ∪ (𝐴 ∖ 𝐶)) | ||
Theorem | difindir 4221 | Distributive law for class difference. (Contributed by NM, 17-Aug-2004.) |
⊢ ((𝐴 ∩ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∩ (𝐵 ∖ 𝐶)) | ||
Theorem | indifdi 4222 | Distribute intersection over difference. (Contributed by BTernaryTau, 14-Aug-2024.) |
⊢ (𝐴 ∩ (𝐵 ∖ 𝐶)) = ((𝐴 ∩ 𝐵) ∖ (𝐴 ∩ 𝐶)) | ||
Theorem | indifdir 4223 | Distribute intersection over difference. (Contributed by Scott Fenton, 14-Apr-2011.) (Revised by BTernaryTau, 14-Aug-2024.) |
⊢ ((𝐴 ∖ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∖ (𝐵 ∩ 𝐶)) | ||
Theorem | indifdirOLD 4224 | Obsolete version of indifdir 4223 as of 14-Aug-2024. (Contributed by Scott Fenton, 14-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∖ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∖ (𝐵 ∩ 𝐶)) | ||
Theorem | difdif2 4225 | Class difference by a class difference. (Contributed by Thierry Arnoux, 18-Dec-2017.) |
⊢ (𝐴 ∖ (𝐵 ∖ 𝐶)) = ((𝐴 ∖ 𝐵) ∪ (𝐴 ∩ 𝐶)) | ||
Theorem | undm 4226 | De Morgan's law for union. Theorem 5.2(13) of [Stoll] p. 19. (Contributed by NM, 18-Aug-2004.) |
⊢ (V ∖ (𝐴 ∪ 𝐵)) = ((V ∖ 𝐴) ∩ (V ∖ 𝐵)) | ||
Theorem | indm 4227 | De Morgan's law for intersection. Theorem 5.2(13') of [Stoll] p. 19. (Contributed by NM, 18-Aug-2004.) |
⊢ (V ∖ (𝐴 ∩ 𝐵)) = ((V ∖ 𝐴) ∪ (V ∖ 𝐵)) | ||
Theorem | difun1 4228 | A relationship involving double difference and union. (Contributed by NM, 29-Aug-2004.) |
⊢ (𝐴 ∖ (𝐵 ∪ 𝐶)) = ((𝐴 ∖ 𝐵) ∖ 𝐶) | ||
Theorem | undif3 4229 | An equality involving class union and class difference. The first equality of Exercise 13 of [TakeutiZaring] p. 22. (Contributed by Alan Sare, 17-Apr-2012.) (Proof shortened by JJ, 13-Jul-2021.) |
⊢ (𝐴 ∪ (𝐵 ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ (𝐶 ∖ 𝐴)) | ||
Theorem | difin2 4230 | Represent a class difference as an intersection with a larger difference. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝐴 ⊆ 𝐶 → (𝐴 ∖ 𝐵) = ((𝐶 ∖ 𝐵) ∩ 𝐴)) | ||
Theorem | dif32 4231 | Swap second and third argument of double difference. (Contributed by NM, 18-Aug-2004.) |
⊢ ((𝐴 ∖ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∖ 𝐵) | ||
Theorem | difabs 4232 | Absorption-like law for class difference: you can remove a class only once. (Contributed by FL, 2-Aug-2009.) |
⊢ ((𝐴 ∖ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵) | ||
Theorem | sscon34b 4233 | Relative complementation reverses inclusion of subclasses. Relativized version of complss 4085. (Contributed by RP, 3-Jun-2021.) |
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → (𝐴 ⊆ 𝐵 ↔ (𝐶 ∖ 𝐵) ⊆ (𝐶 ∖ 𝐴))) | ||
Theorem | rcompleq 4234 | Two subclasses are equal if and only if their relative complements are equal. Relativized version of compleq 4086. (Contributed by RP, 10-Jun-2021.) |
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → (𝐴 = 𝐵 ↔ (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵))) | ||
Theorem | dfsymdif3 4235 | Alternate definition of the symmetric difference, given in Example 4.1 of [Stoll] p. 262 (the original definition corresponds to [Stoll] p. 13). (Contributed by NM, 17-Aug-2004.) (Revised by BJ, 30-Apr-2020.) |
⊢ (𝐴 △ 𝐵) = ((𝐴 ∪ 𝐵) ∖ (𝐴 ∩ 𝐵)) | ||
Theorem | unabw 4236* | Union of two class abstractions. Version of unab 4237 using implicit substitution, which does not require ax-8 2111, ax-10 2140, ax-12 2174. (Contributed by Gino Giotto, 15-Oct-2024.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃)) ⇒ ⊢ ({𝑥 ∣ 𝜑} ∪ {𝑥 ∣ 𝜓}) = {𝑦 ∣ (𝜒 ∨ 𝜃)} | ||
Theorem | unab 4237 | Union of two class abstractions. (Contributed by NM, 29-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ({𝑥 ∣ 𝜑} ∪ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∨ 𝜓)} | ||
Theorem | inab 4238 | Intersection of two class abstractions. (Contributed by NM, 29-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ({𝑥 ∣ 𝜑} ∩ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∧ 𝜓)} | ||
Theorem | difab 4239 | Difference of two class abstractions. (Contributed by NM, 23-Oct-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ({𝑥 ∣ 𝜑} ∖ {𝑥 ∣ 𝜓}) = {𝑥 ∣ (𝜑 ∧ ¬ 𝜓)} | ||
Theorem | abanssl 4240 | A class abstraction with a conjunction is a subset of the class abstraction with the left conjunct only. (Contributed by AV, 7-Aug-2024.) (Proof shortened by SN, 22-Aug-2024.) |
⊢ {𝑓 ∣ (𝜑 ∧ 𝜓)} ⊆ {𝑓 ∣ 𝜑} | ||
Theorem | abanssr 4241 | A class abstraction with a conjunction is a subset of the class abstraction with the right conjunct only. (Contributed by AV, 7-Aug-2024.) (Proof shortened by SN, 22-Aug-2024.) |
⊢ {𝑓 ∣ (𝜑 ∧ 𝜓)} ⊆ {𝑓 ∣ 𝜓} | ||
Theorem | notabw 4242* | A class abstraction defined by a negation. Version of notab 4243 using implicit substitution, which does not require ax-10 2140, ax-12 2174. (Contributed by Gino Giotto, 15-Oct-2024.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∣ ¬ 𝜑} = (V ∖ {𝑦 ∣ 𝜓}) | ||
Theorem | notab 4243 | A class abstraction defined by a negation. (Contributed by FL, 18-Sep-2010.) |
⊢ {𝑥 ∣ ¬ 𝜑} = (V ∖ {𝑥 ∣ 𝜑}) | ||
Theorem | unrab 4244 | Union of two restricted class abstractions. (Contributed by NM, 25-Mar-2004.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∨ 𝜓)} | ||
Theorem | inrab 4245 | Intersection of two restricted class abstractions. (Contributed by NM, 1-Sep-2006.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)} | ||
Theorem | inrab2 4246* | Intersection with a restricted class abstraction. (Contributed by NM, 19-Nov-2007.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ 𝐵) = {𝑥 ∈ (𝐴 ∩ 𝐵) ∣ 𝜑} | ||
Theorem | difrab 4247 | Difference of two restricted class abstractions. (Contributed by NM, 23-Oct-2004.) |
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∖ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ ¬ 𝜓)} | ||
Theorem | dfrab3 4248* | Alternate definition of restricted class abstraction. (Contributed by Mario Carneiro, 8-Sep-2013.) |
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = (𝐴 ∩ {𝑥 ∣ 𝜑}) | ||
Theorem | dfrab2 4249* | Alternate definition of restricted class abstraction. (Contributed by NM, 20-Sep-2003.) (Proof shortened by BJ, 22-Apr-2019.) |
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = ({𝑥 ∣ 𝜑} ∩ 𝐴) | ||
Theorem | notrab 4250* | Complementation of restricted class abstractions. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝜑}) = {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} | ||
Theorem | dfrab3ss 4251* | Restricted class abstraction with a common superset. (Contributed by Stefan O'Rear, 12-Sep-2015.) (Proof shortened by Mario Carneiro, 8-Nov-2015.) |
⊢ (𝐴 ⊆ 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = (𝐴 ∩ {𝑥 ∈ 𝐵 ∣ 𝜑})) | ||
Theorem | rabun2 4252 | Abstraction restricted to a union. (Contributed by Stefan O'Rear, 5-Feb-2015.) |
⊢ {𝑥 ∈ (𝐴 ∪ 𝐵) ∣ 𝜑} = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐵 ∣ 𝜑}) | ||
Theorem | reuun2 4253 | Transfer uniqueness to a smaller or larger class. (Contributed by NM, 21-Oct-2005.) |
⊢ (¬ ∃𝑥 ∈ 𝐵 𝜑 → (∃!𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜑)) | ||
Theorem | reuss2 4254* | Transfer uniqueness to a smaller subclass. (Contributed by NM, 20-Oct-2005.) |
⊢ (((𝐴 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) ∧ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜓)) → ∃!𝑥 ∈ 𝐴 𝜑) | ||
Theorem | reuss 4255* | Transfer uniqueness to a smaller subclass. (Contributed by NM, 21-Aug-1999.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜑) → ∃!𝑥 ∈ 𝐴 𝜑) | ||
Theorem | reuun1 4256* | Transfer uniqueness to a smaller class. (Contributed by NM, 21-Oct-2005.) |
⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ (𝐴 ∪ 𝐵)(𝜑 ∨ 𝜓)) → ∃!𝑥 ∈ 𝐴 𝜑) | ||
Theorem | reupick 4257* | Restricted uniqueness "picks" a member of a subclass. (Contributed by NM, 21-Aug-1999.) |
⊢ (((𝐴 ⊆ 𝐵 ∧ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜑)) ∧ 𝜑) → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | ||
Theorem | reupick3 4258* | Restricted uniqueness "picks" a member of a subclass. (Contributed by Mario Carneiro, 19-Nov-2016.) |
⊢ ((∃!𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ∧ 𝑥 ∈ 𝐴) → (𝜑 → 𝜓)) | ||
Theorem | reupick2 4259* | Restricted uniqueness "picks" a member of a subclass. (Contributed by Mario Carneiro, 15-Dec-2013.) (Proof shortened by Mario Carneiro, 19-Nov-2016.) |
⊢ (((∀𝑥 ∈ 𝐴 (𝜓 → 𝜑) ∧ ∃𝑥 ∈ 𝐴 𝜓 ∧ ∃!𝑥 ∈ 𝐴 𝜑) ∧ 𝑥 ∈ 𝐴) → (𝜑 ↔ 𝜓)) | ||
Theorem | euelss 4260* | Transfer uniqueness of an element to a smaller subclass. (Contributed by AV, 14-Apr-2020.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 𝑥 ∈ 𝐴 ∧ ∃!𝑥 𝑥 ∈ 𝐵) → ∃!𝑥 𝑥 ∈ 𝐴) | ||
Syntax | c0 4261 | Extend class notation to include the empty set. |
class ∅ | ||
Definition | df-nul 4262 | Define the empty set. More precisely, we should write "empty class". It will be posited in ax-nul 5233 that an empty set exists. Then, by uniqueness among classes (eq0 4282, as opposed to the weaker uniqueness among sets, nulmo 2715), it will follow that ∅ is indeed a set (0ex 5234). Special case of Exercise 4.10(o) of [Mendelson] p. 231. For a more traditional definition, but requiring a dummy variable, see dfnul2 4264. (Contributed by NM, 17-Jun-1993.) Clarify that at this point, it is not established that it is a set. (Revised by BJ, 22-Sep-2022.) |
⊢ ∅ = (V ∖ V) | ||
Theorem | dfnul4 4263 | Alternate definition of the empty class/set. (Contributed by BJ, 30-Nov-2019.) Avoid ax-8 2111, df-clel 2817. (Revised by Gino Giotto, 3-Sep-2024.) Prove directly from definition to allow shortening dfnul2 4264. (Revised by BJ, 23-Sep-2024.) |
⊢ ∅ = {𝑥 ∣ ⊥} | ||
Theorem | dfnul2 4264 | Alternate definition of the empty set. Definition 5.14 of [TakeutiZaring] p. 20. (Contributed by NM, 26-Dec-1996.) Remove dependency on ax-10 2140, ax-11 2157, and ax-12 2174. (Revised by Steven Nguyen, 3-May-2023.) (Proof shortened by BJ, 23-Sep-2024.) |
⊢ ∅ = {𝑥 ∣ ¬ 𝑥 = 𝑥} | ||
Theorem | dfnul3 4265 | Alternate definition of the empty set. (Contributed by NM, 25-Mar-2004.) (Proof shortened by BJ, 23-Sep-2024.) |
⊢ ∅ = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐴} | ||
Theorem | dfnul2OLD 4266 | Obsolete version of dfnul2 4264 as of 23-Sep-2024. (Contributed by NM, 26-Dec-1996.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ∅ = {𝑥 ∣ ¬ 𝑥 = 𝑥} | ||
Theorem | dfnul3OLD 4267 | Obsolete version of dfnul4 4263 as of 23-Sep-2024. (Contributed by NM, 25-Mar-2004.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ∅ = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐴} | ||
Theorem | dfnul4OLD 4268 | Obsolete version of dfnul4 4263 as of 23-Sep-2024. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ∅ = {𝑥 ∣ ⊥} | ||
Theorem | noel 4269 | The empty set has no elements. Theorem 6.14 of [Quine] p. 44. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Mario Carneiro, 1-Sep-2015.) Remove dependency on ax-10 2140, ax-11 2157, and ax-12 2174. (Revised by Steven Nguyen, 3-May-2023.) (Proof shortened by BJ, 23-Sep-2024.) |
⊢ ¬ 𝐴 ∈ ∅ | ||
Theorem | noelOLD 4270 | Obsolete version of noel 4269 as of 18-Sep-2024. (Contributed by NM, 21-Jun-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ¬ 𝐴 ∈ ∅ | ||
Theorem | nel02 4271 | The empty set has no elements. (Contributed by Peter Mazsa, 4-Jan-2018.) |
⊢ (𝐴 = ∅ → ¬ 𝐵 ∈ 𝐴) | ||
Theorem | n0i 4272 | If a class has elements, then it is not empty. (Contributed by NM, 31-Dec-1993.) |
⊢ (𝐵 ∈ 𝐴 → ¬ 𝐴 = ∅) | ||
Theorem | ne0i 4273 | If a class has elements, then it is nonempty. (Contributed by NM, 31-Dec-1993.) |
⊢ (𝐵 ∈ 𝐴 → 𝐴 ≠ ∅) | ||
Theorem | ne0d 4274 | Deduction form of ne0i 4273. If a class has elements, then it is nonempty. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝐵 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ≠ ∅) | ||
Theorem | n0ii 4275 | If a class has elements, then it is not empty. Inference associated with n0i 4272. (Contributed by BJ, 15-Jul-2021.) |
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ ¬ 𝐵 = ∅ | ||
Theorem | ne0ii 4276 | If a class has elements, then it is nonempty. Inference associated with ne0i 4273. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ 𝐵 ≠ ∅ | ||
Theorem | vn0 4277 | The universal class is not equal to the empty set. (Contributed by NM, 11-Sep-2008.) Avoid ax-8 2111, df-clel 2817. (Revised by Gino Giotto, 6-Sep-2024.) |
⊢ V ≠ ∅ | ||
Theorem | vn0ALT 4278 | Alternate proof of vn0 4277. Shorter, but requiring df-clel 2817, ax-8 2111. (Contributed by NM, 11-Sep-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ V ≠ ∅ | ||
Theorem | eq0f 4279 | A class is equal to the empty set if and only if it has no elements. Theorem 2 of [Suppes] p. 22. (Contributed by BJ, 15-Jul-2021.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴) | ||
Theorem | neq0f 4280 | A class is not empty if and only if it has at least one element. Proposition 5.17(1) of [TakeutiZaring] p. 20. This version of neq0 4284 requires only that 𝑥 not be free in, rather than not occur in, 𝐴. (Contributed by BJ, 15-Jul-2021.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴) | ||
Theorem | n0f 4281 | 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 4285 requires only that 𝑥 not be free in, rather than not occur in, 𝐴. (Contributed by NM, 17-Oct-2003.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴) | ||
Theorem | eq0 4282* | 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 2157, ax-12 2174. (Revised by Gino Giotto and Steven Nguyen, 28-Jun-2024.) Avoid ax-8 2111, df-clel 2817. (Revised by Gino Giotto, 6-Sep-2024.) |
⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴) | ||
Theorem | eq0ALT 4283* | Alternate proof of eq0 4282. Shorter, but requiring df-clel 2817, ax-8 2111. (Contributed by NM, 29-Aug-1993.) Avoid ax-11 2157, ax-12 2174. (Revised by Gino Giotto and Steven Nguyen, 28-Jun-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴) | ||
Theorem | neq0 4284* | 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 2157, ax-12 2174. (Revised by Gino Giotto, 28-Jun-2024.) |
⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴) | ||
Theorem | n0 4285* | 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 2157, ax-12 2174. (Revised by Gino Giotto, 28-Jun-2024.) |
⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴) | ||
Theorem | eq0OLDOLD 4286* | Obsolete version of eq0 4282 as of 28-Jun-2024. (Contributed by NM, 29-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴) | ||
Theorem | neq0OLD 4287* | Obsolete version of neq0 4284 as of 28-Jun-2024. (Contributed by NM, 21-Jun-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴) | ||
Theorem | n0OLD 4288* | Obsolete version of n0 4285 as of 28-Jun-2024. (Contributed by NM, 29-Sep-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴) | ||
Theorem | nel0 4289* | From the general negation of membership in 𝐴, infer that 𝐴 is the empty set. (Contributed by BJ, 6-Oct-2018.) |
⊢ ¬ 𝑥 ∈ 𝐴 ⇒ ⊢ 𝐴 = ∅ | ||
Theorem | reximdva0 4290* | Restricted existence deduced from nonempty class. (Contributed by NM, 1-Feb-2012.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓) ⇒ ⊢ ((𝜑 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 𝜓) | ||
Theorem | rspn0 4291* | Specialization for restricted generalization with a nonempty class. (Contributed by Alexander van der Vekens, 6-Sep-2018.) Avoid ax-10 2140, ax-12 2174. (Revised by Gino Giotto, 28-Jun-2024.) |
⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 𝜑 → 𝜑)) | ||
Theorem | rspn0OLD 4292* | Obsolete version of rspn0 4291 as of 28-Jun-2024. (Contributed by Alexander van der Vekens, 6-Sep-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 𝜑 → 𝜑)) | ||
Theorem | n0rex 4293* | There is an element in a nonempty class which is an element of the class. (Contributed by AV, 17-Dec-2020.) |
⊢ (𝐴 ≠ ∅ → ∃𝑥 ∈ 𝐴 𝑥 ∈ 𝐴) | ||
Theorem | ssn0rex 4294* | 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 4295* | A case of equivalence of "at most one" and "only one". (Contributed by FL, 6-Dec-2010.) |
⊢ (𝐴 ≠ ∅ → (∃*𝑥 𝑥 ∈ 𝐴 ↔ ∃!𝑥 𝑥 ∈ 𝐴)) | ||
Theorem | rex0 4296 | Vacuous restricted existential quantification is false. (Contributed by NM, 15-Oct-2003.) |
⊢ ¬ ∃𝑥 ∈ ∅ 𝜑 | ||
Theorem | reu0 4297 | Vacuous restricted uniqueness is always false. (Contributed by AV, 3-Apr-2023.) |
⊢ ¬ ∃!𝑥 ∈ ∅ 𝜑 | ||
Theorem | rmo0 4298 | Vacuous restricted at-most-one quantifier is always true. (Contributed by AV, 3-Apr-2023.) |
⊢ ∃*𝑥 ∈ ∅ 𝜑 | ||
Theorem | 0el 4299* | Membership of the empty set in another class. (Contributed by NM, 29-Jun-2004.) |
⊢ (∅ ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ¬ 𝑦 ∈ 𝑥) | ||
Theorem | n0el 4300* | Negated membership of the empty set in another class. (Contributed by Rodolfo Medina, 25-Sep-2010.) |
⊢ (¬ ∅ ∈ 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃𝑢 𝑢 ∈ 𝑥) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |