![]() |
Metamath
Proof Explorer Theorem List (p. 45 of 479) | < 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: | ![]() (1-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ssn0 4401 | A class with a nonempty subclass is nonempty. (Contributed by NM, 17-Feb-2007.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → 𝐵 ≠ ∅) | ||
Theorem | 0dif 4402 | 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 4403 | 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 4404 | Obsolete version of abf 4403 as of 28-Jun-2024. (Contributed by NM, 20-Jan-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ¬ 𝜑 ⇒ ⊢ {𝑥 ∣ 𝜑} = ∅ | ||
Theorem | eq0rdv 4405* | Deduction for equality to the empty set. (Contributed by NM, 11-Jul-2014.) Avoid ax-8 2109, df-clel 2811. (Revised by Gino Giotto, 6-Sep-2024.) |
⊢ (𝜑 → ¬ 𝑥 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 = ∅) | ||
Theorem | eq0rdvALT 4406* | Alternate proof of eq0rdv 4405. Shorter, but requiring df-clel 2811, ax-8 2109. (Contributed by NM, 11-Jul-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → ¬ 𝑥 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 = ∅) | ||
Theorem | csbprc 4407 | 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 4408 | The proper substitution of a class into the empty set is the empty set. (Contributed by NM, 18-Aug-2018.) |
⊢ ⦋𝐴 / 𝑥⦌∅ = ∅ | ||
Theorem | sbcel12 4409 | Distribute proper substitution through a membership relation. (Contributed by NM, 10-Nov-2005.) (Revised by NM, 18-Aug-2018.) |
⊢ ([𝐴 / 𝑥]𝐵 ∈ 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 ∈ ⦋𝐴 / 𝑥⦌𝐶) | ||
Theorem | sbceqg 4410 | Distribute proper substitution through an equality relation. (Contributed by NM, 10-Nov-2005.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)) | ||
Theorem | sbceqi 4411 | Distribution of class substitution over equality, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.) |
⊢ 𝐴 ∈ V & ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐷 & ⊢ ⦋𝐴 / 𝑥⦌𝐶 = 𝐸 ⇒ ⊢ ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ 𝐷 = 𝐸) | ||
Theorem | sbcnel12g 4412 | Distribute proper substitution through negated membership. (Contributed by Andrew Salmon, 18-Jun-2011.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 ∉ 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 ∉ ⦋𝐴 / 𝑥⦌𝐶)) | ||
Theorem | sbcne12 4413 | Distribute proper substitution through an inequality. (Contributed by Andrew Salmon, 18-Jun-2011.) (Revised by NM, 18-Aug-2018.) |
⊢ ([𝐴 / 𝑥]𝐵 ≠ 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 ≠ ⦋𝐴 / 𝑥⦌𝐶) | ||
Theorem | sbcel1g 4414* | 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 4415* | Move proper substitution to first argument of an equality. (Contributed by NM, 30-Nov-2005.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶)) | ||
Theorem | sbcel2 4416* | Move proper substitution in and out of a membership relation. (Contributed by NM, 14-Nov-2005.) (Revised by NM, 18-Aug-2018.) |
⊢ ([𝐴 / 𝑥]𝐵 ∈ 𝐶 ↔ 𝐵 ∈ ⦋𝐴 / 𝑥⦌𝐶) | ||
Theorem | sbceq2g 4417* | Move proper substitution to second argument of an equality. (Contributed by NM, 30-Nov-2005.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ 𝐵 = ⦋𝐴 / 𝑥⦌𝐶)) | ||
Theorem | csbcom 4418* | Commutative law for double substitution into a class. (Contributed by NM, 14-Nov-2005.) (Revised by NM, 18-Aug-2018.) |
⊢ ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = ⦋𝐵 / 𝑦⦌⦋𝐴 / 𝑥⦌𝐶 | ||
Theorem | sbcnestgfw 4419* | Nest the composition of two substitutions. Version of sbcnestgf 4424 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 4420* | Nest the composition of two substitutions. Version of csbnestgf 4425 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 4421* | Nest the composition of two substitutions. Version of sbcnestg 4426 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 4422* | Nest the composition of two substitutions. Version of csbnestg 4427 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 4423* | Composition of two substitutions. Version of sbcco3g 4428 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 4424 | Nest the composition of two substitutions. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker sbcnestgfw 4419 when possible. (Contributed by Mario Carneiro, 11-Nov-2016.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑦Ⅎ𝑥𝜑) → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦]𝜑)) | ||
Theorem | csbnestgf 4425 | Nest the composition of two substitutions. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker csbnestgfw 4420 when possible. (Contributed by NM, 23-Nov-2005.) (Proof shortened by Mario Carneiro, 10-Nov-2016.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑦Ⅎ𝑥𝐶) → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = ⦋⦋𝐴 / 𝑥⦌𝐵 / 𝑦⦌𝐶) | ||
Theorem | sbcnestg 4426* | Nest the composition of two substitutions. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker sbcnestgw 4421 when possible. (Contributed by NM, 27-Nov-2005.) (Proof shortened by Mario Carneiro, 11-Nov-2016.) (New usage is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦]𝜑)) | ||
Theorem | csbnestg 4427* | Nest the composition of two substitutions. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker csbnestgw 4422 when possible. (Contributed by NM, 23-Nov-2005.) (Proof shortened by Mario Carneiro, 10-Nov-2016.) (New usage is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐶 = ⦋⦋𝐴 / 𝑥⦌𝐵 / 𝑦⦌𝐶) | ||
Theorem | sbcco3g 4428* | Composition of two substitutions. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker sbcco3gw 4423 when possible. (Contributed by NM, 27-Nov-2005.) (Revised by Mario Carneiro, 11-Nov-2016.) (New usage is discouraged.) |
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [𝐶 / 𝑦]𝜑)) | ||
Theorem | csbco3g 4429* | 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 4430 | Nest the composition of two substitutions. (Contributed by NM, 23-May-2006.) (Proof shortened by Mario Carneiro, 11-Nov-2016.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑥⦌𝐶 = ⦋⦋𝐴 / 𝑥⦌𝐵 / 𝑥⦌𝐶) | ||
Theorem | csbidm 4431* | Idempotent law for class substitutions. (Contributed by NM, 1-Mar-2008.) (Revised by NM, 18-Aug-2018.) |
⊢ ⦋𝐴 / 𝑥⦌⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵 | ||
Theorem | csbvarg 4432 | 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 4433 | The proper substitution of a class for a setvar variable results in the class (if the class exists), in inference form of csbvarg 4432. (Contributed by Giovanni Mascellani, 30-May-2019.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ⦋𝐴 / 𝑥⦌𝑥 = 𝐴 | ||
Theorem | sbccsb 4434* | 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 4435 | 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 4436* | Special case related to rspsbc 3874. (Contributed by NM, 10-Dec-2005.) (Proof shortened by Eric Schmidt, 17-Jan-2007.) |
⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝐶 ∈ 𝐷) → ⦋𝐴 / 𝑥⦌𝐶 ∈ 𝐷) | ||
Theorem | sbnfc2 4437* | Two ways of expressing "𝑥 is (effectively) not free in 𝐴". (Contributed by Mario Carneiro, 14-Oct-2016.) |
⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦∀𝑧⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑧 / 𝑥⦌𝐴) | ||
Theorem | csbab 4438* | Move substitution into a class abstraction. (Contributed by NM, 13-Dec-2005.) (Revised by NM, 19-Aug-2018.) |
⊢ ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝜑} = {𝑦 ∣ [𝐴 / 𝑥]𝜑} | ||
Theorem | csbun 4439 | 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 4440 | 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 4441* | Conversion of implicit substitution to explicit class substitution. This version of csbiedf 3925 avoids a disjointness condition on 𝑥, 𝐴 and 𝑥, 𝐷 by substituting twice. Deduction form of csbie2 3936. (Contributed by AV, 29-Mar-2024.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝐶) & ⊢ (𝜑 → Ⅎ𝑥𝐷) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶) & ⊢ ((𝜑 ∧ 𝑦 = 𝐴) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐷) | ||
Theorem | 2nreu 4442* | 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.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) ⇒ ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵) → ((𝜓 ∧ 𝜒) → ¬ ∃!𝑥 ∈ 𝑋 𝜑)) | ||
Theorem | un00 4443 | Two classes are empty iff their union is empty. (Contributed by NM, 11-Aug-2004.) |
⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ (𝐴 ∪ 𝐵) = ∅) | ||
Theorem | vss 4444 | Only the universal class has the universal class as a subclass. (Contributed by NM, 17-Sep-2003.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (V ⊆ 𝐴 ↔ 𝐴 = V) | ||
Theorem | 0pss 4445 | The null set is a proper subset of any nonempty set. (Contributed by NM, 27-Feb-1996.) |
⊢ (∅ ⊊ 𝐴 ↔ 𝐴 ≠ ∅) | ||
Theorem | npss0 4446 | No set is a proper subset of the empty set. (Contributed by NM, 17-Jun-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) (Proof shortened by JJ, 14-Jul-2021.) |
⊢ ¬ 𝐴 ⊊ ∅ | ||
Theorem | pssv 4447 | Any non-universal class is a proper subclass of the universal class. (Contributed by NM, 17-May-1998.) |
⊢ (𝐴 ⊊ V ↔ ¬ 𝐴 = V) | ||
Theorem | disj 4448* | Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 17-Feb-2004.) Avoid ax-10 2138, ax-11 2155, ax-12 2172. (Revised by Gino Giotto, 28-Jun-2024.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵) | ||
Theorem | disjOLD 4449* | Obsolete version of disj 4448 as of 28-Jun-2024. (Contributed by NM, 17-Feb-2004.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵) | ||
Theorem | disjr 4450* | Two ways of saying that two classes are disjoint. (Contributed by Jeff Madsen, 19-Jun-2011.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥 ∈ 𝐵 ¬ 𝑥 ∈ 𝐴) | ||
Theorem | disj1 4451* | Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 19-Aug-1993.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵)) | ||
Theorem | reldisj 4452 | Two ways of saying that two classes are disjoint, using the complement of 𝐵 relative to a universe 𝐶. (Contributed by NM, 15-Feb-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) Avoid ax-12 2172. (Revised by Gino Giotto, 28-Jun-2024.) |
⊢ (𝐴 ⊆ 𝐶 → ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐴 ⊆ (𝐶 ∖ 𝐵))) | ||
Theorem | reldisjOLD 4453 | Obsolete version of reldisj 4452 as of 28-Jun-2024. (Contributed by NM, 15-Feb-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ⊆ 𝐶 → ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐴 ⊆ (𝐶 ∖ 𝐵))) | ||
Theorem | disj3 4454 | Two ways of saying that two classes are disjoint. (Contributed by NM, 19-May-1998.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐴 = (𝐴 ∖ 𝐵)) | ||
Theorem | disjne 4455 | Members of disjoint sets are not equal. (Contributed by NM, 28-Mar-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → 𝐶 ≠ 𝐷) | ||
Theorem | disjeq0 4456 | Two disjoint sets are equal iff both are empty. (Contributed by AV, 19-Jun-2022.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ → (𝐴 = 𝐵 ↔ (𝐴 = ∅ ∧ 𝐵 = ∅))) | ||
Theorem | disjel 4457 | A set can't belong to both members of disjoint classes. (Contributed by NM, 28-Feb-2015.) |
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝐶 ∈ 𝐴) → ¬ 𝐶 ∈ 𝐵) | ||
Theorem | disj2 4458 | Two ways of saying that two classes are disjoint. (Contributed by NM, 17-May-1998.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐴 ⊆ (V ∖ 𝐵)) | ||
Theorem | disj4 4459 | Two ways of saying that two classes are disjoint. (Contributed by NM, 21-Mar-2004.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ¬ (𝐴 ∖ 𝐵) ⊊ 𝐴) | ||
Theorem | ssdisj 4460 | Intersection with a subclass of a disjoint class. (Contributed by FL, 24-Jan-2007.) (Proof shortened by JJ, 14-Jul-2021.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ (𝐵 ∩ 𝐶) = ∅) → (𝐴 ∩ 𝐶) = ∅) | ||
Theorem | disjpss 4461 | A class is a proper subset of its union with a disjoint nonempty class. (Contributed by NM, 15-Sep-2004.) |
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝐵 ≠ ∅) → 𝐴 ⊊ (𝐴 ∪ 𝐵)) | ||
Theorem | undisj1 4462 | The union of disjoint classes is disjoint. (Contributed by NM, 26-Sep-2004.) |
⊢ (((𝐴 ∩ 𝐶) = ∅ ∧ (𝐵 ∩ 𝐶) = ∅) ↔ ((𝐴 ∪ 𝐵) ∩ 𝐶) = ∅) | ||
Theorem | undisj2 4463 | The union of disjoint classes is disjoint. (Contributed by NM, 13-Sep-2004.) |
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ (𝐴 ∩ 𝐶) = ∅) ↔ (𝐴 ∩ (𝐵 ∪ 𝐶)) = ∅) | ||
Theorem | ssindif0 4464 | Subclass expressed in terms of intersection with difference from the universal class. (Contributed by NM, 17-Sep-2003.) |
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ (V ∖ 𝐵)) = ∅) | ||
Theorem | inelcm 4465 | The intersection of classes with a common member is nonempty. (Contributed by NM, 7-Apr-1994.) |
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → (𝐵 ∩ 𝐶) ≠ ∅) | ||
Theorem | minel 4466 | A minimum element of a class has no elements in common with the class. (Contributed by NM, 22-Jun-1994.) (Proof shortened by JJ, 14-Jul-2021.) |
⊢ ((𝐴 ∈ 𝐵 ∧ (𝐶 ∩ 𝐵) = ∅) → ¬ 𝐴 ∈ 𝐶) | ||
Theorem | undif4 4467 | Distribute union over difference. (Contributed by NM, 17-May-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ((𝐴 ∩ 𝐶) = ∅ → (𝐴 ∪ (𝐵 ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ 𝐶)) | ||
Theorem | disjssun 4468 | Subset relation for disjoint classes. (Contributed by NM, 25-Oct-2005.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ → (𝐴 ⊆ (𝐵 ∪ 𝐶) ↔ 𝐴 ⊆ 𝐶)) | ||
Theorem | vdif0 4469 | Universal class equality in terms of empty difference. (Contributed by NM, 17-Sep-2003.) |
⊢ (𝐴 = V ↔ (V ∖ 𝐴) = ∅) | ||
Theorem | difrab0eq 4470* | If the difference between the restricting class of a restricted class abstraction and the restricted class abstraction is empty, the restricting class is equal to this restricted class abstraction. (Contributed by Alexander van der Vekens, 31-Dec-2017.) |
⊢ ((𝑉 ∖ {𝑥 ∈ 𝑉 ∣ 𝜑}) = ∅ ↔ 𝑉 = {𝑥 ∈ 𝑉 ∣ 𝜑}) | ||
Theorem | pssnel 4471* | A proper subclass has a member in one argument that's not in both. (Contributed by NM, 29-Feb-1996.) |
⊢ (𝐴 ⊊ 𝐵 → ∃𝑥(𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴)) | ||
Theorem | disjdif 4472 | A class and its relative complement are disjoint. Theorem 38 of [Suppes] p. 29. (Contributed by NM, 24-Mar-1998.) |
⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅ | ||
Theorem | disjdifr 4473 | A class and its relative complement are disjoint. (Contributed by Thierry Arnoux, 29-Nov-2023.) |
⊢ ((𝐵 ∖ 𝐴) ∩ 𝐴) = ∅ | ||
Theorem | difin0 4474 | The difference of a class from its intersection is empty. Theorem 37 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ((𝐴 ∩ 𝐵) ∖ 𝐵) = ∅ | ||
Theorem | unvdif 4475 | The union of a class and its complement is the universe. Theorem 5.1(5) of [Stoll] p. 17. (Contributed by NM, 17-Aug-2004.) |
⊢ (𝐴 ∪ (V ∖ 𝐴)) = V | ||
Theorem | undif1 4476 | Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4472). Theorem 35 of [Suppes] p. 29. (Contributed by NM, 19-May-1998.) |
⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵) | ||
Theorem | undif2 4477 | Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4472). Part of proof of Corollary 6K of [Enderton] p. 144. (Contributed by NM, 19-May-1998.) |
⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵) | ||
Theorem | undifabs 4478 | Absorption of difference by union. (Contributed by NM, 18-Aug-2013.) |
⊢ (𝐴 ∪ (𝐴 ∖ 𝐵)) = 𝐴 | ||
Theorem | inundif 4479 | The intersection and class difference of a class with another class unite to give the original class. (Contributed by Paul Chapman, 5-Jun-2009.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ ((𝐴 ∩ 𝐵) ∪ (𝐴 ∖ 𝐵)) = 𝐴 | ||
Theorem | disjdif2 4480 | The difference of a class and a class disjoint from it is the original class. (Contributed by BJ, 21-Apr-2019.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ → (𝐴 ∖ 𝐵) = 𝐴) | ||
Theorem | difun2 4481 | Absorption of union by difference. Theorem 36 of [Suppes] p. 29. (Contributed by NM, 19-May-1998.) |
⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵) | ||
Theorem | undif 4482 | Union of complementary parts into whole. (Contributed by NM, 22-Mar-1998.) |
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵) | ||
Theorem | undifr 4483 | Union of complementary parts into whole. (Contributed by Thierry Arnoux, 21-Nov-2023.) (Proof shortened by SN, 11-Mar-2025.) |
⊢ (𝐴 ⊆ 𝐵 ↔ ((𝐵 ∖ 𝐴) ∪ 𝐴) = 𝐵) | ||
Theorem | undifrOLD 4484 | Obsolete version of undifr 4483 as of 11-Mar-2025. (Contributed by Thierry Arnoux, 21-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ⊆ 𝐵 ↔ ((𝐵 ∖ 𝐴) ∪ 𝐴) = 𝐵) | ||
Theorem | undif5 4485 | An equality involving class union and class difference. (Contributed by Thierry Arnoux, 26-Jun-2024.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐴 ∪ 𝐵) ∖ 𝐵) = 𝐴) | ||
Theorem | ssdifin0 4486 | A subset of a difference does not intersect the subtrahend. (Contributed by Jeff Hankins, 1-Sep-2013.) (Proof shortened by Mario Carneiro, 24-Aug-2015.) |
⊢ (𝐴 ⊆ (𝐵 ∖ 𝐶) → (𝐴 ∩ 𝐶) = ∅) | ||
Theorem | ssdifeq0 4487 | A class is a subclass of itself subtracted from another iff it is the empty set. (Contributed by Steve Rodriguez, 20-Nov-2015.) |
⊢ (𝐴 ⊆ (𝐵 ∖ 𝐴) ↔ 𝐴 = ∅) | ||
Theorem | ssundif 4488 | A condition equivalent to inclusion in the union of two classes. (Contributed by NM, 26-Mar-2007.) |
⊢ (𝐴 ⊆ (𝐵 ∪ 𝐶) ↔ (𝐴 ∖ 𝐵) ⊆ 𝐶) | ||
Theorem | difcom 4489 | Swap the arguments of a class difference. (Contributed by NM, 29-Mar-2007.) |
⊢ ((𝐴 ∖ 𝐵) ⊆ 𝐶 ↔ (𝐴 ∖ 𝐶) ⊆ 𝐵) | ||
Theorem | pssdifcom1 4490 | Two ways to express overlapping subsets. (Contributed by Stefan O'Rear, 31-Oct-2014.) |
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → ((𝐶 ∖ 𝐴) ⊊ 𝐵 ↔ (𝐶 ∖ 𝐵) ⊊ 𝐴)) | ||
Theorem | pssdifcom2 4491 | Two ways to express non-covering pairs of subsets. (Contributed by Stefan O'Rear, 31-Oct-2014.) |
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → (𝐵 ⊊ (𝐶 ∖ 𝐴) ↔ 𝐴 ⊊ (𝐶 ∖ 𝐵))) | ||
Theorem | difdifdir 4492 | Distributive law for class difference. Exercise 4.8 of [Stoll] p. 16. (Contributed by NM, 18-Aug-2004.) |
⊢ ((𝐴 ∖ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∖ (𝐵 ∖ 𝐶)) | ||
Theorem | uneqdifeq 4493 | Two ways to say that 𝐴 and 𝐵 partition 𝐶 (when 𝐴 and 𝐵 don't overlap and 𝐴 is a part of 𝐶). (Contributed by FL, 17-Nov-2008.) (Proof shortened by JJ, 14-Jul-2021.) |
⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐴 ∪ 𝐵) = 𝐶 ↔ (𝐶 ∖ 𝐴) = 𝐵)) | ||
Theorem | raldifeq 4494* | Equality theorem for restricted universal quantifier. (Contributed by Thierry Arnoux, 6-Jul-2019.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → ∀𝑥 ∈ (𝐵 ∖ 𝐴)𝜓) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | r19.2z 4495* | Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1981). The restricted version is valid only when the domain of quantification is not empty. (Contributed by NM, 15-Nov-2003.) |
⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑥 ∈ 𝐴 𝜑) | ||
Theorem | r19.2zb 4496* | A response to the notion that the condition 𝐴 ≠ ∅ can be removed in r19.2z 4495. Interestingly enough, 𝜑 does not figure in the left-hand side. (Contributed by Jeff Hankins, 24-Aug-2009.) |
⊢ (𝐴 ≠ ∅ ↔ (∀𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜑)) | ||
Theorem | r19.3rz 4497* | Restricted quantification of wff not containing quantified variable. (Contributed by FL, 3-Jan-2008.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (𝐴 ≠ ∅ → (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑)) | ||
Theorem | r19.28z 4498* | Restricted quantifier version of Theorem 19.28 of [Margaris] p. 90. It is valid only when the domain of quantification is not empty. (Contributed by NM, 26-Oct-2010.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓))) | ||
Theorem | r19.3rzv 4499* | Restricted quantification of wff not containing quantified variable. (Contributed by NM, 10-Mar-1997.) |
⊢ (𝐴 ≠ ∅ → (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑)) | ||
Theorem | r19.9rzv 4500* | Restricted quantification of wff not containing quantified variable. (Contributed by NM, 27-May-1998.) |
⊢ (𝐴 ≠ ∅ → (𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜑)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |