Home | Metamath
Proof Explorer Theorem List (p. 44 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | eqsn 4301* | Two ways to express that a nonempty set equals a singleton. (Contributed by NM, 15-Dec-2007.) (Proof shortened by JJ, 23-Jul-2021.) |
⊢ (𝐴 ≠ ∅ → (𝐴 = {𝐵} ↔ ∀𝑥 ∈ 𝐴 𝑥 = 𝐵)) | ||
Theorem | eqsnOLD 4302* | Obsolete proof of eqsn 4301 as of 23-Jul-2021. (Contributed by NM, 15-Dec-2007.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐴 ≠ ∅ → (𝐴 = {𝐵} ↔ ∀𝑥 ∈ 𝐴 𝑥 = 𝐵)) | ||
Theorem | issn 4303* | A sufficient condition for a (nonempty) set to be a singleton. (Contributed by AV, 20-Sep-2020.) |
⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 = 𝑦 → ∃𝑧 𝐴 = {𝑧}) | ||
Theorem | n0snor2el 4304* | A nonempty set is either a singleton or contains at least two different elements. (Contributed by AV, 20-Sep-2020.) |
⊢ (𝐴 ≠ ∅ → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 ∨ ∃𝑧 𝐴 = {𝑧})) | ||
Theorem | ssunpr 4305 | Possible values for a set sandwiched between another set and it plus a singleton. (Contributed by Mario Carneiro, 2-Jul-2016.) |
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐵 ∪ {𝐶, 𝐷})) ↔ ((𝐴 = 𝐵 ∨ 𝐴 = (𝐵 ∪ {𝐶})) ∨ (𝐴 = (𝐵 ∪ {𝐷}) ∨ 𝐴 = (𝐵 ∪ {𝐶, 𝐷})))) | ||
Theorem | sspr 4306 | The subsets of a pair. (Contributed by NM, 16-Mar-2006.) (Proof shortened by Mario Carneiro, 2-Jul-2016.) |
⊢ (𝐴 ⊆ {𝐵, 𝐶} ↔ ((𝐴 = ∅ ∨ 𝐴 = {𝐵}) ∨ (𝐴 = {𝐶} ∨ 𝐴 = {𝐵, 𝐶}))) | ||
Theorem | sstp 4307 | The subsets of a triple. (Contributed by Mario Carneiro, 2-Jul-2016.) |
⊢ (𝐴 ⊆ {𝐵, 𝐶, 𝐷} ↔ (((𝐴 = ∅ ∨ 𝐴 = {𝐵}) ∨ (𝐴 = {𝐶} ∨ 𝐴 = {𝐵, 𝐶})) ∨ ((𝐴 = {𝐷} ∨ 𝐴 = {𝐵, 𝐷}) ∨ (𝐴 = {𝐶, 𝐷} ∨ 𝐴 = {𝐵, 𝐶, 𝐷})))) | ||
Theorem | tpss 4308 | A triplet of elements of a class is a subset of the class. (Contributed by NM, 9-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) ↔ {𝐴, 𝐵, 𝐶} ⊆ 𝐷) | ||
Theorem | tpssi 4309 | A triple of elements of a class is a subset of the class. (Contributed by Alexander van der Vekens, 1-Feb-2018.) |
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) → {𝐴, 𝐵, 𝐶} ⊆ 𝐷) | ||
Theorem | sneqrg 4310 | Closed form of sneqr 4311. (Contributed by Scott Fenton, 1-Apr-2011.) (Proof shortened by JJ, 23-Jul-2021.) |
⊢ (𝐴 ∈ 𝑉 → ({𝐴} = {𝐵} → 𝐴 = 𝐵)) | ||
Theorem | sneqr 4311 | If the singletons of two sets are equal, the two sets are equal. Part of Exercise 4 of [TakeutiZaring] p. 15. (Contributed by NM, 27-Aug-1993.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ({𝐴} = {𝐵} → 𝐴 = 𝐵) | ||
Theorem | snsssn 4312 | If a singleton is a subset of another, their members are equal. (Contributed by NM, 28-May-2006.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ({𝐴} ⊆ {𝐵} → 𝐴 = 𝐵) | ||
Theorem | sneqrgOLD 4313 | Obsolete proof of sneqrg 4310 as of 23-Jul-2021. (Contributed by Scott Fenton, 1-Apr-2011.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → ({𝐴} = {𝐵} → 𝐴 = 𝐵)) | ||
Theorem | sneqbg 4314 | Two singletons of sets are equal iff their elements are equal. (Contributed by Scott Fenton, 16-Apr-2012.) |
⊢ (𝐴 ∈ 𝑉 → ({𝐴} = {𝐵} ↔ 𝐴 = 𝐵)) | ||
Theorem | snsspw 4315 | The singleton of a class is a subset of its power class. (Contributed by NM, 21-Jun-1993.) |
⊢ {𝐴} ⊆ 𝒫 𝐴 | ||
Theorem | prsspw 4316 | An unordered pair belongs to the power class of a class iff each member belongs to the class. (Contributed by NM, 10-Dec-2003.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) (Proof shortened by OpenAI, 25-Mar-2020.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ({𝐴, 𝐵} ⊆ 𝒫 𝐶 ↔ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶)) | ||
Theorem | preq1b 4317 | Biconditional equality lemma for unordered pairs, deduction form. Two unordered pairs have the same second element iff the first elements are equal. (Contributed by AV, 18-Dec-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ({𝐴, 𝐶} = {𝐵, 𝐶} ↔ 𝐴 = 𝐵)) | ||
Theorem | preq2b 4318 | Biconditional equality lemma for unordered pairs, deduction form. Two unordered pairs have the same first element iff the second elements are equal. (Contributed by AV, 18-Dec-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ({𝐶, 𝐴} = {𝐶, 𝐵} ↔ 𝐴 = 𝐵)) | ||
Theorem | preqr1 4319 | Reverse equality lemma for unordered pairs. If two unordered pairs have the same second element, the first elements are equal. (Contributed by NM, 18-Oct-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ({𝐴, 𝐶} = {𝐵, 𝐶} → 𝐴 = 𝐵) | ||
Theorem | preqr1OLD 4320 | Reverse equality lemma for unordered pairs. If two unordered pairs have the same second element, the first elements are equal. (Contributed by NM, 18-Oct-1995.) Obsolete version of preqr1 4319 as of 18-Dec-2020. (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ({𝐴, 𝐶} = {𝐵, 𝐶} → 𝐴 = 𝐵) | ||
Theorem | preqr2 4321 | Reverse equality lemma for unordered pairs. If two unordered pairs have the same first element, the second elements are equal. (Contributed by NM, 15-Jul-1993.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ({𝐶, 𝐴} = {𝐶, 𝐵} → 𝐴 = 𝐵) | ||
Theorem | preq12b 4322 | Equality relationship for two unordered pairs. (Contributed by NM, 17-Oct-1996.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))) | ||
Theorem | prel12 4323 | Equality of two unordered pairs. (Contributed by NM, 17-Oct-1996.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ (¬ 𝐴 = 𝐵 → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (𝐴 ∈ {𝐶, 𝐷} ∧ 𝐵 ∈ {𝐶, 𝐷}))) | ||
Theorem | opthpr 4324 | An unordered pair has the ordered pair property (compare opth 4871) under certain conditions. (Contributed by NM, 27-Mar-2007.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ (𝐴 ≠ 𝐷 → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) | ||
Theorem | preqr1g 4325 | Reverse equality lemma for unordered pairs. If two unordered pairs have the same second element, the first elements are equal. Closed form of preqr1 4319. (Contributed by AV, 29-Jan-2021.) (Revised by AV, 18-Sep-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴, 𝐶} = {𝐵, 𝐶} → 𝐴 = 𝐵)) | ||
Theorem | preq12bg 4326 | Closed form of preq12b 4322. (Contributed by Scott Fenton, 28-Mar-2014.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))) | ||
Theorem | prel12g 4327 | Closed form of prel12 4323. (Contributed by AV, 9-Dec-2018.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → (¬ 𝐴 = 𝐵 → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (𝐴 ∈ {𝐶, 𝐷} ∧ 𝐵 ∈ {𝐶, 𝐷})))) | ||
Theorem | prneimg 4328 | Two pairs are not equal if at least one element of the first pair is not contained in the second pair. (Contributed by Alexander van der Vekens, 13-Aug-2017.) |
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → (((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∨ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)) → {𝐴, 𝐵} ≠ {𝐶, 𝐷})) | ||
Theorem | prnebg 4329 | A (proper) pair is not equal to another (maybe inproper) pair if and only if an element of the first pair is not contained in the second pair. (Contributed by Alexander van der Vekens, 16-Jan-2018.) |
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) → (((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∨ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)) ↔ {𝐴, 𝐵} ≠ {𝐶, 𝐷})) | ||
Theorem | preqsnd 4330 | Equivalence for a pair equal to a singleton, deduction form. (Contributed by Thierry Arnoux, 27-Dec-2016.) |
⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐶 ∈ V) ⇒ ⊢ (𝜑 → ({𝐴, 𝐵} = {𝐶} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐶))) | ||
Theorem | preqsn 4331 | Equivalence for a pair equal to a singleton. (Contributed by NM, 3-Jun-2008.) (Proof shortened by JJ, 23-Jul-2021.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ ({𝐴, 𝐵} = {𝐶} ↔ (𝐴 = 𝐵 ∧ 𝐵 = 𝐶)) | ||
Theorem | preqsnOLD 4332 | Obsolete proof of preqsn 4331 as of 23-Jul-2021. (Contributed by NM, 3-Jun-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ ({𝐴, 𝐵} = {𝐶} ↔ (𝐴 = 𝐵 ∧ 𝐵 = 𝐶)) | ||
Theorem | elpreqprlem 4333* | Lemma for elpreqpr 4334. (Contributed by Scott Fenton, 7-Dec-2020.) (Revised by AV, 9-Dec-2020.) |
⊢ (𝐵 ∈ 𝑉 → ∃𝑥{𝐵, 𝐶} = {𝐵, 𝑥}) | ||
Theorem | elpreqpr 4334* | Equality and membership rule for pairs. (Contributed by Scott Fenton, 7-Dec-2020.) |
⊢ (𝐴 ∈ {𝐵, 𝐶} → ∃𝑥{𝐵, 𝐶} = {𝐴, 𝑥}) | ||
Theorem | elpreqprb 4335* | A set is an element of an unordered pair iff there is another (maybe the same) set which is an element of the unordered pair. (Proposed by BJ, 8-Dec-2020.) (Contributed by AV, 9-Dec-2020.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵, 𝐶} ↔ ∃𝑥{𝐵, 𝐶} = {𝐴, 𝑥})) | ||
Theorem | elpr2elpr 4336* | For an element of an unordered pair which is a subset of a given set, there is another (maybe the same) element of the given set being an element of the unordered pair. (Contributed by AV, 5-Dec-2020.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝐴 ∈ {𝑋, 𝑌}) → ∃𝑏 ∈ 𝑉 {𝑋, 𝑌} = {𝐴, 𝑏}) | ||
Theorem | dfopif 4337 | Rewrite df-op 4132 using if. When both arguments are sets, it reduces to the standard Kuratowski definition; otherwise, it is defined to be the empty set. Avoid directly depending on this detail so that theorems will not depend on the Kuratowski construction. (Contributed by Mario Carneiro, 26-Apr-2015.) (Avoid depending on this detail.) |
⊢ 〈𝐴, 𝐵〉 = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅) | ||
Theorem | dfopg 4338 | Value of the ordered pair when the arguments are sets. (Contributed by Mario Carneiro, 26-Apr-2015.) (Avoid depending on this detail.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 〈𝐴, 𝐵〉 = {{𝐴}, {𝐴, 𝐵}}) | ||
Theorem | dfop 4339 | Value of an ordered pair when the arguments are sets, with the conclusion corresponding to Kuratowski's original definition. (Contributed by NM, 25-Jun-1998.) (Avoid depending on this detail.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ 〈𝐴, 𝐵〉 = {{𝐴}, {𝐴, 𝐵}} | ||
Theorem | opeq1 4340 | Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ (𝐴 = 𝐵 → 〈𝐴, 𝐶〉 = 〈𝐵, 𝐶〉) | ||
Theorem | opeq2 4341 | Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ (𝐴 = 𝐵 → 〈𝐶, 𝐴〉 = 〈𝐶, 𝐵〉) | ||
Theorem | opeq12 4342 | Equality theorem for ordered pairs. (Contributed by NM, 28-May-1995.) |
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → 〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉) | ||
Theorem | opeq1i 4343 | Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ 〈𝐴, 𝐶〉 = 〈𝐵, 𝐶〉 | ||
Theorem | opeq2i 4344 | Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ 〈𝐶, 𝐴〉 = 〈𝐶, 𝐵〉 | ||
Theorem | opeq12i 4345 | Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.) (Proof shortened by Eric Schmidt, 4-Apr-2007.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ 〈𝐴, 𝐶〉 = 〈𝐵, 𝐷〉 | ||
Theorem | opeq1d 4346 | Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 〈𝐴, 𝐶〉 = 〈𝐵, 𝐶〉) | ||
Theorem | opeq2d 4347 | Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 〈𝐶, 𝐴〉 = 〈𝐶, 𝐵〉) | ||
Theorem | opeq12d 4348 | Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → 〈𝐴, 𝐶〉 = 〈𝐵, 𝐷〉) | ||
Theorem | oteq1 4349 | Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015.) |
⊢ (𝐴 = 𝐵 → 〈𝐴, 𝐶, 𝐷〉 = 〈𝐵, 𝐶, 𝐷〉) | ||
Theorem | oteq2 4350 | Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015.) |
⊢ (𝐴 = 𝐵 → 〈𝐶, 𝐴, 𝐷〉 = 〈𝐶, 𝐵, 𝐷〉) | ||
Theorem | oteq3 4351 | Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015.) |
⊢ (𝐴 = 𝐵 → 〈𝐶, 𝐷, 𝐴〉 = 〈𝐶, 𝐷, 𝐵〉) | ||
Theorem | oteq1d 4352 | Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 〈𝐴, 𝐶, 𝐷〉 = 〈𝐵, 𝐶, 𝐷〉) | ||
Theorem | oteq2d 4353 | Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 〈𝐶, 𝐴, 𝐷〉 = 〈𝐶, 𝐵, 𝐷〉) | ||
Theorem | oteq3d 4354 | Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 〈𝐶, 𝐷, 𝐴〉 = 〈𝐶, 𝐷, 𝐵〉) | ||
Theorem | oteq123d 4355 | Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) & ⊢ (𝜑 → 𝐸 = 𝐹) ⇒ ⊢ (𝜑 → 〈𝐴, 𝐶, 𝐸〉 = 〈𝐵, 𝐷, 𝐹〉) | ||
Theorem | nfop 4356 | Bound-variable hypothesis builder for ordered pairs. (Contributed by NM, 14-Nov-1995.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥〈𝐴, 𝐵〉 | ||
Theorem | nfopd 4357 | Deduction version of bound-variable hypothesis builder nfop 4356. This shows how the deduction version of a not-free theorem such as nfop 4356 can be created from the corresponding not-free inference theorem. (Contributed by NM, 4-Feb-2008.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥〈𝐴, 𝐵〉) | ||
Theorem | csbopg 4358 | Distribution of class substitution over ordered pairs. (Contributed by Drahflow, 25-Sep-2015.) (Revised by Mario Carneiro, 29-Oct-2015.) (Revised by ML, 25-Oct-2020.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌〈𝐶, 𝐷〉 = 〈⦋𝐴 / 𝑥⦌𝐶, ⦋𝐴 / 𝑥⦌𝐷〉) | ||
Theorem | opid 4359 | The ordered pair 〈𝐴, 𝐴〉 in Kuratowski's representation. (Contributed by FL, 28-Dec-2011.) (Avoid depending on this detail.) |
⊢ 𝐴 ∈ V ⇒ ⊢ 〈𝐴, 𝐴〉 = {{𝐴}} | ||
Theorem | ralunsn 4360* | Restricted quantification over the union of a set and a singleton, using implicit substitution. (Contributed by Paul Chapman, 17-Nov-2012.) (Revised by Mario Carneiro, 23-Apr-2015.) |
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐵 ∈ 𝐶 → (∀𝑥 ∈ (𝐴 ∪ {𝐵})𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))) | ||
Theorem | 2ralunsn 4361* | Double restricted quantification over the union of a set and a singleton, using implicit substitution. (Contributed by Paul Chapman, 17-Nov-2012.) |
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝐵 ∈ 𝐶 → (∀𝑥 ∈ (𝐴 ∪ {𝐵})∀𝑦 ∈ (𝐴 ∪ {𝐵})𝜑 ↔ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) ∧ (∀𝑦 ∈ 𝐴 𝜒 ∧ 𝜃)))) | ||
Theorem | opprc 4362 | Expansion of an ordered pair when either member is a proper class. (Contributed by Mario Carneiro, 26-Apr-2015.) |
⊢ (¬ (𝐴 ∈ V ∧ 𝐵 ∈ V) → 〈𝐴, 𝐵〉 = ∅) | ||
Theorem | opprc1 4363 | Expansion of an ordered pair when the first member is a proper class. See also opprc 4362. (Contributed by NM, 10-Apr-2004.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ (¬ 𝐴 ∈ V → 〈𝐴, 𝐵〉 = ∅) | ||
Theorem | opprc2 4364 | Expansion of an ordered pair when the second member is a proper class. See also opprc 4362. (Contributed by NM, 15-Nov-1994.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ (¬ 𝐵 ∈ V → 〈𝐴, 𝐵〉 = ∅) | ||
Theorem | oprcl 4365 | If an ordered pair has an element, then its arguments are sets. (Contributed by Mario Carneiro, 26-Apr-2015.) |
⊢ (𝐶 ∈ 〈𝐴, 𝐵〉 → (𝐴 ∈ V ∧ 𝐵 ∈ V)) | ||
Theorem | pwsn 4366 | The power set of a singleton. (Contributed by NM, 5-Jun-2006.) |
⊢ 𝒫 {𝐴} = {∅, {𝐴}} | ||
Theorem | pwsnALT 4367 | Alternate proof of pwsn 4366, more direct. (Contributed by NM, 5-Jun-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝒫 {𝐴} = {∅, {𝐴}} | ||
Theorem | pwpr 4368 | The power set of an unordered pair. (Contributed by NM, 1-May-2009.) |
⊢ 𝒫 {𝐴, 𝐵} = ({∅, {𝐴}} ∪ {{𝐵}, {𝐴, 𝐵}}) | ||
Theorem | pwtp 4369 | The power set of an unordered triple. (Contributed by Mario Carneiro, 2-Jul-2016.) |
⊢ 𝒫 {𝐴, 𝐵, 𝐶} = (({∅, {𝐴}} ∪ {{𝐵}, {𝐴, 𝐵}}) ∪ ({{𝐶}, {𝐴, 𝐶}} ∪ {{𝐵, 𝐶}, {𝐴, 𝐵, 𝐶}})) | ||
Theorem | pwpwpw0 4370 | Compute the power set of the power set of the power set of the empty set. (See also pw0 4283 and pwpw0 4284.) (Contributed by NM, 2-May-2009.) |
⊢ 𝒫 {∅, {∅}} = ({∅, {∅}} ∪ {{{∅}}, {∅, {∅}}}) | ||
Theorem | pwv 4371 | The power class of the universe is the universe. Exercise 4.12(d) of [Mendelson] p. 235. (Contributed by NM, 14-Sep-2003.) |
⊢ 𝒫 V = V | ||
Syntax | cuni 4372 | Extend class notation to include the union of a class (read: 'union 𝐴') |
class ∪ 𝐴 | ||
Definition | df-uni 4373* | Define the union of a class i.e. the collection of all members of the members of the class. Definition 5.5 of [TakeutiZaring] p. 16. For example, ∪ {{1, 3}, {1, 8}} = {1, 3, 8} (ex-uni 26675). This is similar to the union of two classes df-un 3545. (Contributed by NM, 23-Aug-1993.) |
⊢ ∪ 𝐴 = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴)} | ||
Theorem | dfuni2 4374* | Alternate definition of class union. (Contributed by NM, 28-Jun-1998.) |
⊢ ∪ 𝐴 = {𝑥 ∣ ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦} | ||
Theorem | eluni 4375* | Membership in class union. (Contributed by NM, 22-May-1994.) |
⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵)) | ||
Theorem | eluni2 4376* | Membership in class union. Restricted quantifier version. (Contributed by NM, 31-Aug-1999.) |
⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥) | ||
Theorem | elunii 4377 | Membership in class union. (Contributed by NM, 24-Mar-1995.) |
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ ∪ 𝐶) | ||
Theorem | nfuni 4378 | Bound-variable hypothesis builder for union. (Contributed by NM, 30-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥∪ 𝐴 | ||
Theorem | nfunid 4379 | Deduction version of nfuni 4378. (Contributed by NM, 18-Feb-2013.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥∪ 𝐴) | ||
Theorem | unieq 4380 | Equality theorem for class union. Exercise 15 of [TakeutiZaring] p. 18. (Contributed by NM, 10-Aug-1993.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵) | ||
Theorem | unieqi 4381 | Inference of equality of two class unions. (Contributed by NM, 30-Aug-1993.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ∪ 𝐴 = ∪ 𝐵 | ||
Theorem | unieqd 4382 | Deduction of equality of two class unions. (Contributed by NM, 21-Apr-1995.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ∪ 𝐴 = ∪ 𝐵) | ||
Theorem | eluniab 4383* | Membership in union of a class abstraction. (Contributed by NM, 11-Aug-1994.) (Revised by Mario Carneiro, 14-Nov-2016.) |
⊢ (𝐴 ∈ ∪ {𝑥 ∣ 𝜑} ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝜑)) | ||
Theorem | elunirab 4384* | Membership in union of a class abstraction. (Contributed by NM, 4-Oct-2006.) |
⊢ (𝐴 ∈ ∪ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ ∃𝑥 ∈ 𝐵 (𝐴 ∈ 𝑥 ∧ 𝜑)) | ||
Theorem | unipr 4385 | The union of a pair is the union of its members. Proposition 5.7 of [TakeutiZaring] p. 16. (Contributed by NM, 23-Aug-1993.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵) | ||
Theorem | uniprg 4386 | The union of a pair is the union of its members. Proposition 5.7 of [TakeutiZaring] p. 16. (Contributed by NM, 25-Aug-2006.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵)) | ||
Theorem | unisn 4387 | A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53. (Contributed by NM, 30-Aug-1993.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ∪ {𝐴} = 𝐴 | ||
Theorem | unisng 4388 | A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53. (Contributed by NM, 13-Aug-2002.) |
⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴) | ||
Theorem | unisn3 4389* | Union of a singleton in the form of a restricted class abstraction. (Contributed by NM, 3-Jul-2008.) |
⊢ (𝐴 ∈ 𝐵 → ∪ {𝑥 ∈ 𝐵 ∣ 𝑥 = 𝐴} = 𝐴) | ||
Theorem | dfnfc2 4390* | An alternative statement of the effective freeness of a class 𝐴, when it is a set. (Contributed by Mario Carneiro, 14-Oct-2016.) (Proof shortened by JJ, 26-Jul-2021.) |
⊢ (∀𝑥 𝐴 ∈ 𝑉 → (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 = 𝐴)) | ||
Theorem | dfnfc2OLD 4391* | Obsolete proof of dfnfc2 4390 as of 26-Jul-2021. (Contributed by Mario Carneiro, 14-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝐴 ∈ 𝑉 → (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 = 𝐴)) | ||
Theorem | uniun 4392 | The class union of the union of two classes. Theorem 8.3 of [Quine] p. 53. (Contributed by NM, 20-Aug-1993.) |
⊢ ∪ (𝐴 ∪ 𝐵) = (∪ 𝐴 ∪ ∪ 𝐵) | ||
Theorem | uniin 4393 | The class union of the intersection of two classes. Exercise 4.12(n) of [Mendelson] p. 235. See uniinqs 7714 for a condition where equality holds. (Contributed by NM, 4-Dec-2003.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ ∪ (𝐴 ∩ 𝐵) ⊆ (∪ 𝐴 ∩ ∪ 𝐵) | ||
Theorem | uniss 4394 | Subclass relationship for class union. Theorem 61 of [Suppes] p. 39. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵) | ||
Theorem | ssuni 4395 | Subclass relationship for class union. (Contributed by NM, 24-May-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) (Proof shortened by JJ, 26-Jul-2021.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ⊆ ∪ 𝐶) | ||
Theorem | ssuniOLD 4396 | Obsolete proof of ssuni 4395 as of 26-Jul-2021. (Contributed by NM, 24-May-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ⊆ ∪ 𝐶) | ||
Theorem | unissi 4397 | Subclass relationship for subclass union. Inference form of uniss 4394. (Contributed by David Moews, 1-May-2017.) |
⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ ∪ 𝐴 ⊆ ∪ 𝐵 | ||
Theorem | unissd 4398 | Subclass relationship for subclass union. Deduction form of uniss 4394. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → ∪ 𝐴 ⊆ ∪ 𝐵) | ||
Theorem | uni0b 4399 | The union of a set is empty iff the set is included in the singleton of the empty set. (Contributed by NM, 12-Sep-2004.) |
⊢ (∪ 𝐴 = ∅ ↔ 𝐴 ⊆ {∅}) | ||
Theorem | uni0c 4400* | The union of a set is empty iff all of its members are empty. (Contributed by NM, 16-Aug-2006.) |
⊢ (∪ 𝐴 = ∅ ↔ ∀𝑥 ∈ 𝐴 𝑥 = ∅) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |