![]() |
Metamath
Proof Explorer Theorem List (p. 55 of 475) | < 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-30034) |
![]() (30035-31557) |
![]() (31558-47500) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ralxfr2d 5401* | Transfer universal quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by Mario Carneiro, 20-Aug-2014.) |
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐶 𝑥 = 𝐴)) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐶 𝜒)) | ||
Theorem | rexxfr2d 5402* | Transfer universal quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by Mario Carneiro, 20-Aug-2014.) (Proof shortened by Mario Carneiro, 19-Nov-2016.) |
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐶 𝑥 = 𝐴)) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐵 𝜓 ↔ ∃𝑦 ∈ 𝐶 𝜒)) | ||
Theorem | ralxfrd2 5403* | Transfer universal quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. Variant of ralxfrd 5399. (Contributed by Alexander van der Vekens, 25-Apr-2018.) |
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐶 𝑥 = 𝐴) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐶 𝜒)) | ||
Theorem | rexxfrd2 5404* | Transfer existence from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. Variant of rexxfrd 5400. (Contributed by Alexander van der Vekens, 25-Apr-2018.) |
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐶 𝑥 = 𝐴) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐵 𝜓 ↔ ∃𝑦 ∈ 𝐶 𝜒)) | ||
Theorem | ralxfr 5405* | Transfer universal quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by NM, 10-Jun-2005.) (Revised by Mario Carneiro, 15-Aug-2014.) |
⊢ (𝑦 ∈ 𝐶 → 𝐴 ∈ 𝐵) & ⊢ (𝑥 ∈ 𝐵 → ∃𝑦 ∈ 𝐶 𝑥 = 𝐴) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐶 𝜓) | ||
Theorem | ralxfrALT 5406* | Alternate proof of ralxfr 5405 which does not use ralxfrd 5399. (Contributed by NM, 10-Jun-2005.) (Revised by Mario Carneiro, 15-Aug-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑦 ∈ 𝐶 → 𝐴 ∈ 𝐵) & ⊢ (𝑥 ∈ 𝐵 → ∃𝑦 ∈ 𝐶 𝑥 = 𝐴) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐶 𝜓) | ||
Theorem | rexxfr 5407* | Transfer existence from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by NM, 10-Jun-2005.) (Revised by Mario Carneiro, 15-Aug-2014.) |
⊢ (𝑦 ∈ 𝐶 → 𝐴 ∈ 𝐵) & ⊢ (𝑥 ∈ 𝐵 → ∃𝑦 ∈ 𝐶 𝑥 = 𝐴) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐶 𝜓) | ||
Theorem | rabxfrd 5408* | Membership in a restricted class abstraction after substituting an expression 𝐴 (containing 𝑦) for 𝑥 in the formula defining the class abstraction. (Contributed by NM, 16-Jan-2012.) |
⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑦𝐶 & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝐴 ∈ 𝐷) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜒)) & ⊢ (𝑦 = 𝐵 → 𝐴 = 𝐶) ⇒ ⊢ ((𝜑 ∧ 𝐵 ∈ 𝐷) → (𝐶 ∈ {𝑥 ∈ 𝐷 ∣ 𝜓} ↔ 𝐵 ∈ {𝑦 ∈ 𝐷 ∣ 𝜒})) | ||
Theorem | rabxfr 5409* | Membership in a restricted class abstraction after substituting an expression 𝐴 (containing 𝑦) for 𝑥 in the the formula defining the class abstraction. (Contributed by NM, 10-Jun-2005.) |
⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑦𝐶 & ⊢ (𝑦 ∈ 𝐷 → 𝐴 ∈ 𝐷) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → 𝐴 = 𝐶) ⇒ ⊢ (𝐵 ∈ 𝐷 → (𝐶 ∈ {𝑥 ∈ 𝐷 ∣ 𝜑} ↔ 𝐵 ∈ {𝑦 ∈ 𝐷 ∣ 𝜓})) | ||
Theorem | reuhypd 5410* | A theorem useful for eliminating the restricted existential uniqueness hypotheses in riotaxfrd 7384. (Contributed by NM, 16-Jan-2012.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐵 ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶) → (𝑥 = 𝐴 ↔ 𝑦 = 𝐵)) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ∃!𝑦 ∈ 𝐶 𝑥 = 𝐴) | ||
Theorem | reuhyp 5411* | A theorem useful for eliminating the restricted existential uniqueness hypotheses in reuxfr1 3744. (Contributed by NM, 15-Nov-2004.) |
⊢ (𝑥 ∈ 𝐶 → 𝐵 ∈ 𝐶) & ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶) → (𝑥 = 𝐴 ↔ 𝑦 = 𝐵)) ⇒ ⊢ (𝑥 ∈ 𝐶 → ∃!𝑦 ∈ 𝐶 𝑥 = 𝐴) | ||
Theorem | zfpair 5412 |
The Axiom of Pairing of Zermelo-Fraenkel set theory. Axiom 2 of
[TakeutiZaring] p. 15. In some
textbooks this is stated as a separate
axiom; here we show it is redundant since it can be derived from the
other axioms.
This theorem should not be referenced by any proof other than axprALT 5413. Instead, use zfpair2 5421 below so that the uses of the Axiom of Pairing can be more easily identified. (Contributed by NM, 18-Oct-1995.) (New usage is discouraged.) |
⊢ {𝑥, 𝑦} ∈ V | ||
Theorem | axprALT 5413* | Alternate proof of axpr 5419. (Contributed by NM, 14-Nov-2006.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧) | ||
Theorem | axprlem1 5414* | Lemma for axpr 5419. There exists a set to which all empty sets belong. (Contributed by Rohan Ridenour, 10-Aug-2023.) (Revised by BJ, 13-Aug-2023.) |
⊢ ∃𝑥∀𝑦(∀𝑧 ¬ 𝑧 ∈ 𝑦 → 𝑦 ∈ 𝑥) | ||
Theorem | axprlem2 5415* | Lemma for axpr 5419. There exists a set to which all sets whose only members are empty sets belong. (Contributed by Rohan Ridenour, 9-Aug-2023.) (Revised by BJ, 13-Aug-2023.) |
⊢ ∃𝑥∀𝑦(∀𝑧 ∈ 𝑦 ∀𝑤 ¬ 𝑤 ∈ 𝑧 → 𝑦 ∈ 𝑥) | ||
Theorem | axprlem3 5416* | Lemma for axpr 5419. Eliminate the antecedent of the relevant replacement instance. (Contributed by Rohan Ridenour, 10-Aug-2023.) |
⊢ ∃𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) | ||
Theorem | axprlem4 5417* | Lemma for axpr 5419. The first element of the pair is included in any superset of the set whose existence is asserted by the axiom of replacement. (Contributed by Rohan Ridenour, 10-Aug-2023.) (Revised by BJ, 13-Aug-2023.) |
⊢ ((∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑥) → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) | ||
Theorem | axprlem5 5418* | Lemma for axpr 5419. The second element of the pair is included in any superset of the set whose existence is asserted by the axiom of replacement. (Contributed by Rohan Ridenour, 10-Aug-2023.) (Revised by BJ, 13-Aug-2023.) |
⊢ ((∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑦) → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) | ||
Theorem | axpr 5419* |
Unabbreviated version of the Axiom of Pairing of ZF set theory, derived
as a theorem from the other axioms.
This theorem should not be referenced by any proof. Instead, use ax-pr 5420 below so that the uses of the Axiom of Pairing can be more easily identified. For a shorter proof using ax-ext 2702, see axprALT 5413. (Contributed by NM, 14-Nov-2006.) Remove dependency on ax-ext 2702. (Revised by Rohan Ridenour, 10-Aug-2023.) (Proof shortened by BJ, 13-Aug-2023.) Use ax-pr 5420 instead. (New usage is discouraged.) |
⊢ ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧) | ||
Axiom | ax-pr 5420* | The Axiom of Pairing of ZF set theory. It was derived as Theorem axpr 5419 above and is therefore redundant, but we state it as a separate axiom here so that its uses can be identified more easily. (Contributed by NM, 14-Nov-2006.) |
⊢ ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧) | ||
Theorem | zfpair2 5421 | Derive the abbreviated version of the Axiom of Pairing from ax-pr 5420. See zfpair 5412 for its derivation from the other axioms. (Contributed by NM, 14-Nov-2006.) |
⊢ {𝑥, 𝑦} ∈ V | ||
Theorem | vsnex 5422 | A singleton built on a setvar is a set. (Contributed by BJ, 15-Jan-2025.) |
⊢ {𝑥} ∈ V | ||
Theorem | snexg 5423 | A singleton built on a set is a set. Special case of snex 5424 which does not require ax-nul 5299 and is intuitionistically valid. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 19-May-2013.) Extract from snex 5424 and shorten proof. (Revised by BJ, 15-Jan-2025.) |
⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V) | ||
Theorem | snex 5424 | A singleton is a set. Theorem 7.12 of [Quine] p. 51, proved using Extensionality, Separation, Null Set, and Pairing. See also snexALT 5374. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 19-May-2013.) |
⊢ {𝐴} ∈ V | ||
Theorem | prex 5425 | The Axiom of Pairing using class variables. Theorem 7.13 of [Quine] p. 51. By virtue of its definition, an unordered pair remains a set (even though no longer a pair) even when its components are proper classes (see prprc 4764), so we can dispense with hypotheses requiring them to be sets. (Contributed by NM, 15-Jul-1993.) |
⊢ {𝐴, 𝐵} ∈ V | ||
Theorem | exel 5426* |
There exist two sets, one a member of the other.
This theorem looks similar to el 5430, but its meaning is different. It only depends on the axioms ax-mp 5 to ax-4 1811, ax-6 1971, and ax-pr 5420. This theorem does not exclude that these two sets could actually be one single set containing itself. That two different sets exist is proved by exexneq 5427. (Contributed by SN, 23-Dec-2024.) |
⊢ ∃𝑦∃𝑥 𝑥 ∈ 𝑦 | ||
Theorem | exexneq 5427* | There exist two different sets. (Contributed by NM, 7-Nov-2006.) Avoid ax-13 2370. (Revised by BJ, 31-May-2019.) Avoid ax-8 2108. (Revised by SN, 21-Sep-2023.) Avoid ax-12 2171. (Revised by Rohan Ridenour, 9-Oct-2024.) Use ax-pr 5420 instead of ax-pow 5356. (Revised by BTernaryTau, 3-Dec-2024.) Extract this result from the proof of dtru 5429. (Revised by BJ, 2-Jan-2025.) |
⊢ ∃𝑥∃𝑦 ¬ 𝑥 = 𝑦 | ||
Theorem | exneq 5428* |
Given any set (the "𝑦 " in the statement), there
exists a set not
equal to it.
The same statement without disjoint variable condition is false, since we do not have ∃𝑥¬ 𝑥 = 𝑥. This theorem is proved directly from set theory axioms (no class definitions) and does not depend on ax-ext 2702, ax-sep 5292, or ax-pow 5356 nor auxiliary logical axiom schemes ax-10 2137 to ax-13 2370. See dtruALT 5379 for a shorter proof using more axioms, and dtruALT2 5361 for a proof using ax-pow 5356 instead of ax-pr 5420. (Contributed by NM, 7-Nov-2006.) Avoid ax-13 2370. (Revised by BJ, 31-May-2019.) Avoid ax-8 2108. (Revised by SN, 21-Sep-2023.) Avoid ax-12 2171. (Revised by Rohan Ridenour, 9-Oct-2024.) Use ax-pr 5420 instead of ax-pow 5356. (Revised by BTernaryTau, 3-Dec-2024.) Extract this result from the proof of dtru 5429. (Revised by BJ, 2-Jan-2025.) |
⊢ ∃𝑥 ¬ 𝑥 = 𝑦 | ||
Theorem | dtru 5429* | Given any set (the "𝑦 " in the statement), not all sets are equal to it. The same statement without disjoint variable condition is false since it contradicts stdpc6 2031. The same comments and revision history concerning axiom usage as in exneq 5428 apply. (Contributed by NM, 7-Nov-2006.) Extract exneq 5428 as an intermediate result. (Revised by BJ, 2-Jan-2025.) |
⊢ ¬ ∀𝑥 𝑥 = 𝑦 | ||
Theorem | el 5430* | Any set is an element of some other set. See elALT 5433 for a shorter proof using more axioms, and see elALT2 5360 for a proof that uses ax-9 2116 and ax-pow 5356 instead of ax-pr 5420. (Contributed by NM, 4-Jan-2002.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) Use ax-pr 5420 instead of ax-9 2116 and ax-pow 5356. (Revised by BTernaryTau, 2-Dec-2024.) |
⊢ ∃𝑦 𝑥 ∈ 𝑦 | ||
Theorem | sels 5431* | If a class is a set, then it is a member of a set. (Contributed by NM, 4-Jan-2002.) Generalize from the proof of elALT 5433. (Revised by BJ, 3-Apr-2019.) Avoid ax-sep 5292, ax-nul 5299, ax-pow 5356. (Revised by BTernaryTau, 15-Jan-2025.) |
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝐴 ∈ 𝑥) | ||
Theorem | selsALT 5432* | Alternate proof of sels 5431, requiring ax-sep 5292 but not using el 5430 (which is proved from it as elALT 5433). (especially when the proof of el 5430 is inlined in sels 5431). (Contributed by NM, 4-Jan-2002.) Generalize from the proof of elALT 5433. (Revised by BJ, 3-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝐴 ∈ 𝑥) | ||
Theorem | elALT 5433* | Alternate proof of el 5430, shorter but requiring ax-sep 5292. (Contributed by NM, 4-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ∃𝑦 𝑥 ∈ 𝑦 | ||
Theorem | dtruOLD 5434* | Obsolete proof of dtru 5429 as of 01-Jan-2025. (Contributed by NM, 7-Nov-2006.) Avoid ax-13 2370. (Revised by BJ, 31-May-2019.) Avoid ax-12 2171. (Revised by Rohan Ridenour, 9-Oct-2024.) Use ax-pr 5420 instead of ax-pow 5356. (Revised by BTernaryTau, 3-Dec-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ¬ ∀𝑥 𝑥 = 𝑦 | ||
Theorem | snelpwg 5435 | A singleton of a set is a member of the powerclass of a class if and only if that set is a member of that class. (Contributed by NM, 1-Apr-1998.) Put in closed form and avoid ax-nul 5299. (Revised by BJ, 17-Jan-2025.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ 𝒫 𝐵)) | ||
Theorem | snelpwi 5436 | If a set is a member of a class, then the singleton of that set is a member of the powerclass of that class. (Contributed by Alan Sare, 25-Aug-2011.) |
⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ 𝒫 𝐵) | ||
Theorem | snelpwiOLD 5437 | Obsolete version of snelpwi 5436 as of 17-Jan-2025. (Contributed by NM, 28-May-1995.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ 𝒫 𝐵) | ||
Theorem | snelpw 5438 | A singleton of a set is a member of the powerclass of a class if and only if that set is a member of that class. (Contributed by NM, 1-Apr-1998.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ 𝒫 𝐵) | ||
Theorem | prelpw 5439 | An unordered pair of two sets is a member of the powerclass of a class if and only if the two sets are members of that class. (Contributed by AV, 8-Jan-2020.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ∈ 𝒫 𝐶)) | ||
Theorem | prelpwi 5440 | If two sets are members of a class, then the unordered pair of those two sets is a member of the powerclass of that class. (Contributed by Thierry Arnoux, 10-Mar-2017.) (Proof shortened by AV, 23-Oct-2021.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → {𝐴, 𝐵} ∈ 𝒫 𝐶) | ||
Theorem | rext 5441* | A theorem similar to extensionality, requiring the existence of a singleton. Exercise 8 of [TakeutiZaring] p. 16. (Contributed by NM, 10-Aug-1993.) |
⊢ (∀𝑧(𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧) → 𝑥 = 𝑦) | ||
Theorem | sspwb 5442 | The powerclass construction preserves and reflects inclusion. Classes are subclasses if and only if their power classes are subclasses. Exercise 18 of [TakeutiZaring] p. 18. (Contributed by NM, 13-Oct-1996.) |
⊢ (𝐴 ⊆ 𝐵 ↔ 𝒫 𝐴 ⊆ 𝒫 𝐵) | ||
Theorem | unipw 5443 | A class equals the union of its power class. Exercise 6(a) of [Enderton] p. 38. (Contributed by NM, 14-Oct-1996.) (Proof shortened by Alan Sare, 28-Dec-2008.) |
⊢ ∪ 𝒫 𝐴 = 𝐴 | ||
Theorem | univ 5444 | The union of the universe is the universe. Exercise 4.12(c) of [Mendelson] p. 235. (Contributed by NM, 14-Sep-2003.) |
⊢ ∪ V = V | ||
Theorem | pwtr 5445 | A class is transitive iff its power class is transitive. (Contributed by Alan Sare, 25-Aug-2011.) (Revised by Mario Carneiro, 15-Jun-2014.) |
⊢ (Tr 𝐴 ↔ Tr 𝒫 𝐴) | ||
Theorem | ssextss 5446* | An extensionality-like principle defining subclass in terms of subsets. (Contributed by NM, 30-Jun-2004.) |
⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ⊆ 𝐴 → 𝑥 ⊆ 𝐵)) | ||
Theorem | ssext 5447* | An extensionality-like principle that uses the subset instead of the membership relation: two classes are equal iff they have the same subsets. (Contributed by NM, 30-Jun-2004.) |
⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ⊆ 𝐴 ↔ 𝑥 ⊆ 𝐵)) | ||
Theorem | nssss 5448* | Negation of subclass relationship. Compare nss 4042. (Contributed by NM, 30-Jun-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ (¬ 𝐴 ⊆ 𝐵 ↔ ∃𝑥(𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵)) | ||
Theorem | pweqb 5449 | Classes are equal if and only if their power classes are equal. Exercise 19 of [TakeutiZaring] p. 18. (Contributed by NM, 13-Oct-1996.) |
⊢ (𝐴 = 𝐵 ↔ 𝒫 𝐴 = 𝒫 𝐵) | ||
Theorem | intidg 5450* | The intersection of all sets to which a set belongs is the singleton of that set. (Contributed by NM, 5-Jun-2009.) Put in closed form and avoid ax-nul 5299. (Revised by BJ, 17-Jan-2025.) |
⊢ (𝐴 ∈ 𝑉 → ∩ {𝑥 ∣ 𝐴 ∈ 𝑥} = {𝐴}) | ||
Theorem | intidOLD 5451* | Obsolete version of intidg 5450 as of 18-Jan-2025. (Contributed by NM, 5-Jun-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ∩ {𝑥 ∣ 𝐴 ∈ 𝑥} = {𝐴} | ||
Theorem | moabex 5452 | "At most one" existence implies a class abstraction exists. (Contributed by NM, 30-Dec-1996.) |
⊢ (∃*𝑥𝜑 → {𝑥 ∣ 𝜑} ∈ V) | ||
Theorem | rmorabex 5453 | Restricted "at most one" existence implies a restricted class abstraction exists. (Contributed by NM, 17-Jun-2017.) |
⊢ (∃*𝑥 ∈ 𝐴 𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V) | ||
Theorem | euabex 5454 | The abstraction of a wff with existential uniqueness exists. (Contributed by NM, 25-Nov-1994.) |
⊢ (∃!𝑥𝜑 → {𝑥 ∣ 𝜑} ∈ V) | ||
Theorem | nnullss 5455* | A nonempty class (even if proper) has a nonempty subset. (Contributed by NM, 23-Aug-2003.) |
⊢ (𝐴 ≠ ∅ → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅)) | ||
Theorem | exss 5456* | Restricted existence in a class (even if proper) implies restricted existence in a subset. (Contributed by NM, 23-Aug-2003.) |
⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑦(𝑦 ⊆ 𝐴 ∧ ∃𝑥 ∈ 𝑦 𝜑)) | ||
Theorem | opex 5457 | An ordered pair of classes is a set. Exercise 7 of [TakeutiZaring] p. 16. (Contributed by NM, 18-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ 〈𝐴, 𝐵〉 ∈ V | ||
Theorem | otex 5458 | An ordered triple of classes is a set. (Contributed by NM, 3-Apr-2015.) |
⊢ 〈𝐴, 𝐵, 𝐶〉 ∈ V | ||
Theorem | elopg 5459 | Characterization of the elements of an ordered pair. Closed form of elop 5460. (Contributed by BJ, 22-Jun-2019.) (Avoid depending on this detail.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ 〈𝐴, 𝐵〉 ↔ (𝐶 = {𝐴} ∨ 𝐶 = {𝐴, 𝐵}))) | ||
Theorem | elop 5460 | Characterization of the elements of an ordered pair. Exercise 3 of [TakeutiZaring] p. 15. (Contributed by NM, 15-Jul-1993.) (Revised by Mario Carneiro, 26-Apr-2015.) Remove an extraneous hypothesis. (Revised by BJ, 25-Dec-2020.) (Avoid depending on this detail.) |
⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (𝐴 ∈ 〈𝐵, 𝐶〉 ↔ (𝐴 = {𝐵} ∨ 𝐴 = {𝐵, 𝐶})) | ||
Theorem | opi1 5461 | One of the two elements in an ordered pair. (Contributed by NM, 15-Jul-1993.) (Revised by Mario Carneiro, 26-Apr-2015.) (Avoid depending on this detail.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ {𝐴} ∈ 〈𝐴, 𝐵〉 | ||
Theorem | opi2 5462 | One of the two elements of an ordered pair. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.) (Avoid depending on this detail.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ {𝐴, 𝐵} ∈ 〈𝐴, 𝐵〉 | ||
Theorem | opeluu 5463 | Each member of an ordered pair belongs to the union of the union of a class to which the ordered pair belongs. Lemma 3D of [Enderton] p. 41. (Contributed by NM, 31-Mar-1995.) (Revised by Mario Carneiro, 27-Feb-2016.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉 ∈ 𝐶 → (𝐴 ∈ ∪ ∪ 𝐶 ∧ 𝐵 ∈ ∪ ∪ 𝐶)) | ||
Theorem | op1stb 5464 | Extract the first member of an ordered pair. Theorem 73 of [Suppes] p. 42. (See op2ndb 6215 to extract the second member, op1sta 6213 for an alternate version, and op1st 7965 for the preferred version.) (Contributed by NM, 25-Nov-2003.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ∩ ∩ 〈𝐴, 𝐵〉 = 𝐴 | ||
Theorem | brv 5465 | Two classes are always in relation by V. This is simply equivalent to 〈𝐴, 𝐵〉 ∈ V, and does not imply that V is a relation: see nrelv 5792. (Contributed by Scott Fenton, 11-Apr-2012.) |
⊢ 𝐴V𝐵 | ||
Theorem | opnz 5466 | An ordered pair is nonempty iff the arguments are sets. (Contributed by NM, 24-Jan-2004.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ (〈𝐴, 𝐵〉 ≠ ∅ ↔ (𝐴 ∈ V ∧ 𝐵 ∈ V)) | ||
Theorem | opnzi 5467 | An ordered pair is nonempty if the arguments are sets. (Contributed by Mario Carneiro, 26-Apr-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ 〈𝐴, 𝐵〉 ≠ ∅ | ||
Theorem | opth1 5468 | Equality of the first members of equal ordered pairs. (Contributed by NM, 28-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 𝐴 = 𝐶) | ||
Theorem | opth 5469 | The ordered pair theorem. If two ordered pairs are equal, their first elements are equal and their second elements are equal. Exercise 6 of [TakeutiZaring] p. 16. Note that 𝐶 and 𝐷 are not required to be sets due our specific ordered pair definition. (Contributed by NM, 28-May-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | opthg 5470 | Ordered pair theorem. 𝐶 and 𝐷 are not required to be sets under our specific ordered pair definition. (Contributed by NM, 14-Oct-2005.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) | ||
Theorem | opth1g 5471 | Equality of the first members of equal ordered pairs. Closed form of opth1 5468. (Contributed by AV, 14-Oct-2018.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 𝐴 = 𝐶)) | ||
Theorem | opthg2 5472 | Ordered pair theorem. (Contributed by NM, 14-Oct-2005.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) → (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) | ||
Theorem | opth2 5473 | Ordered pair theorem. (Contributed by NM, 21-Sep-2014.) |
⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | opthneg 5474 | Two ordered pairs are not equal iff their first components or their second components are not equal. (Contributed by AV, 13-Dec-2018.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈𝐴, 𝐵〉 ≠ 〈𝐶, 𝐷〉 ↔ (𝐴 ≠ 𝐶 ∨ 𝐵 ≠ 𝐷))) | ||
Theorem | opthne 5475 | Two ordered pairs are not equal iff their first components or their second components are not equal. (Contributed by AV, 13-Dec-2018.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉 ≠ 〈𝐶, 𝐷〉 ↔ (𝐴 ≠ 𝐶 ∨ 𝐵 ≠ 𝐷)) | ||
Theorem | otth2 5476 | Ordered triple theorem, with triple expressed with ordered pairs. (Contributed by NM, 1-May-1995.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝑅 ∈ V ⇒ ⊢ (〈〈𝐴, 𝐵〉, 𝑅〉 = 〈〈𝐶, 𝐷〉, 𝑆〉 ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ∧ 𝑅 = 𝑆)) | ||
Theorem | otth 5477 | Ordered triple theorem. (Contributed by NM, 25-Sep-2014.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝑅 ∈ V ⇒ ⊢ (〈𝐴, 𝐵, 𝑅〉 = 〈𝐶, 𝐷, 𝑆〉 ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ∧ 𝑅 = 𝑆)) | ||
Theorem | otthg 5478 | Ordered triple theorem, closed form. (Contributed by Alexander van der Vekens, 10-Mar-2018.) |
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (〈𝐴, 𝐵, 𝐶〉 = 〈𝐷, 𝐸, 𝐹〉 ↔ (𝐴 = 𝐷 ∧ 𝐵 = 𝐸 ∧ 𝐶 = 𝐹))) | ||
Theorem | otthne 5479 | Contrapositive of the ordered triple theorem. (Contributed by Scott Fenton, 31-Jan-2025.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (〈𝐴, 𝐵, 𝐶〉 ≠ 〈𝐷, 𝐸, 𝐹〉 ↔ (𝐴 ≠ 𝐷 ∨ 𝐵 ≠ 𝐸 ∨ 𝐶 ≠ 𝐹)) | ||
Theorem | eqvinop 5480* | A variable introduction law for ordered pairs. Analogue of Lemma 15 of [Monk2] p. 109. (Contributed by NM, 28-May-1995.) |
⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (𝐴 = 〈𝐵, 𝐶〉 ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 〈𝑥, 𝑦〉 = 〈𝐵, 𝐶〉)) | ||
Theorem | sbcop1 5481* | The proper substitution of an ordered pair for a setvar variable corresponds to a proper substitution of its first component. (Contributed by AV, 8-Apr-2023.) |
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ([𝑎 / 𝑥]𝜓 ↔ [〈𝑎, 𝑦〉 / 𝑧]𝜑) | ||
Theorem | sbcop 5482* | The proper substitution of an ordered pair for a setvar variable corresponds to a proper substitution of each of its components. (Contributed by AV, 8-Apr-2023.) |
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ([𝑏 / 𝑦][𝑎 / 𝑥]𝜓 ↔ [〈𝑎, 𝑏〉 / 𝑧]𝜑) | ||
Theorem | copsexgw 5483* | Version of copsexg 5484 with a disjoint variable condition, which does not require ax-13 2370. (Contributed by Gino Giotto, 26-Jan-2024.) |
⊢ (𝐴 = 〈𝑥, 𝑦〉 → (𝜑 ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑))) | ||
Theorem | copsexg 5484* | Substitution of class 𝐴 for ordered pair 〈𝑥, 𝑦〉. Usage of this theorem is discouraged because it depends on ax-13 2370. Use the weaker copsexgw 5483 when possible. (Contributed by NM, 27-Dec-1996.) (Revised by Andrew Salmon, 11-Jul-2011.) (Proof shortened by Wolf Lammen, 25-Aug-2019.) (New usage is discouraged.) |
⊢ (𝐴 = 〈𝑥, 𝑦〉 → (𝜑 ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑))) | ||
Theorem | copsex2t 5485* | Closed theorem form of copsex2g 5486. (Contributed by NM, 17-Feb-2013.) |
⊢ ((∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ 𝜓)) | ||
Theorem | copsex2g 5486* | Implicit substitution inference for ordered pairs. (Contributed by NM, 28-May-1995.) Use a similar proof to copsex4g 5488 to reduce axiom usage. (Revised by SN, 1-Sep-2024.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ 𝜓)) | ||
Theorem | copsex2gOLD 5487* | Obsolete version of copsex2g 5486 as of 1-Sep-2024. (Contributed by NM, 28-May-1995.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ 𝜓)) | ||
Theorem | copsex4g 5488* | An implicit substitution inference for 2 ordered pairs. (Contributed by NM, 5-Aug-1995.) |
⊢ (((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆)) → (∃𝑥∃𝑦∃𝑧∃𝑤((〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 〈𝐶, 𝐷〉 = 〈𝑧, 𝑤〉) ∧ 𝜑) ↔ 𝜓)) | ||
Theorem | 0nelop 5489 | A property of ordered pairs. (Contributed by Mario Carneiro, 26-Apr-2015.) |
⊢ ¬ ∅ ∈ 〈𝐴, 𝐵〉 | ||
Theorem | opwo0id 5490 | An ordered pair is equal to the ordered pair without the empty set. This is because no ordered pair contains the empty set. (Contributed by AV, 15-Nov-2021.) |
⊢ 〈𝑋, 𝑌〉 = (〈𝑋, 𝑌〉 ∖ {∅}) | ||
Theorem | opeqex 5491 | Equivalence of existence implied by equality of ordered pairs. (Contributed by NM, 28-May-2008.) |
⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐷 ∈ V))) | ||
Theorem | oteqex2 5492 | Equivalence of existence implied by equality of ordered triples. (Contributed by NM, 26-Apr-2015.) |
⊢ (〈〈𝐴, 𝐵〉, 𝐶〉 = 〈〈𝑅, 𝑆〉, 𝑇〉 → (𝐶 ∈ V ↔ 𝑇 ∈ V)) | ||
Theorem | oteqex 5493 | Equivalence of existence implied by equality of ordered triples. (Contributed by NM, 28-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ (〈〈𝐴, 𝐵〉, 𝐶〉 = 〈〈𝑅, 𝑆〉, 𝑇〉 → ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ↔ (𝑅 ∈ V ∧ 𝑆 ∈ V ∧ 𝑇 ∈ V))) | ||
Theorem | opcom 5494 | An ordered pair commutes iff its members are equal. (Contributed by NM, 28-May-2009.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉 = 〈𝐵, 𝐴〉 ↔ 𝐴 = 𝐵) | ||
Theorem | moop2 5495* | "At most one" property of an ordered pair. (Contributed by NM, 11-Apr-2004.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ 𝐵 ∈ V ⇒ ⊢ ∃*𝑥 𝐴 = 〈𝐵, 𝑥〉 | ||
Theorem | opeqsng 5496 | Equivalence for an ordered pair equal to a singleton. (Contributed by NM, 3-Jun-2008.) (Revised by AV, 15-Jul-2022.) (Avoid depending on this detail.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈𝐴, 𝐵〉 = {𝐶} ↔ (𝐴 = 𝐵 ∧ 𝐶 = {𝐴}))) | ||
Theorem | opeqsn 5497 | Equivalence for an ordered pair equal to a singleton. (Contributed by NM, 3-Jun-2008.) (Revised by AV, 15-Jul-2022.) (Avoid depending on this detail.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉 = {𝐶} ↔ (𝐴 = 𝐵 ∧ 𝐶 = {𝐴})) | ||
Theorem | opeqpr 5498 | Equivalence for an ordered pair equal to an unordered pair. (Contributed by NM, 3-Jun-2008.) (Avoid depending on this detail.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉 = {𝐶, 𝐷} ↔ ((𝐶 = {𝐴} ∧ 𝐷 = {𝐴, 𝐵}) ∨ (𝐶 = {𝐴, 𝐵} ∧ 𝐷 = {𝐴}))) | ||
Theorem | snopeqop 5499 | Equivalence for an ordered pair equal to a singleton of an ordered pair. (Contributed by AV, 18-Sep-2020.) (Revised by AV, 15-Jul-2022.) (Avoid depending on this detail.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ({〈𝐴, 𝐵〉} = 〈𝐶, 𝐷〉 ↔ (𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ∧ 𝐶 = {𝐴})) | ||
Theorem | propeqop 5500 | Equivalence for an ordered pair equal to a pair of ordered pairs. (Contributed by AV, 18-Sep-2020.) (Proof shortened by AV, 16-Jun-2022.) (Avoid depending on this detail.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V & ⊢ 𝐸 ∈ V & ⊢ 𝐹 ∈ V ⇒ ⊢ ({〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = 〈𝐸, 𝐹〉 ↔ ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) ∧ ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵})))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |