Home | Metamath
Proof Explorer Theorem List (p. 54 of 466) | < 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-29289) |
Hilbert Space Explorer
(29290-30812) |
Users' Mathboxes
(30813-46532) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | vpwex 5301 | Power set axiom: the powerclass of a set is a set. Axiom 4 of [TakeutiZaring] p. 17. (Contributed by NM, 30-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) Revised to prove pwexg 5302 from vpwex 5301. (Revised by BJ, 10-Aug-2022.) |
⊢ 𝒫 𝑥 ∈ V | ||
Theorem | pwexg 5302 | Power set axiom expressed in class notation, with the sethood requirement as an antecedent. (Contributed by NM, 30-Oct-2003.) |
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V) | ||
Theorem | pwexd 5303 | Deduction version of the power set axiom. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝒫 𝐴 ∈ V) | ||
Theorem | pwex 5304 | Power set axiom expressed in class notation. (Contributed by NM, 21-Jun-1993.) |
⊢ 𝐴 ∈ V ⇒ ⊢ 𝒫 𝐴 ∈ V | ||
Theorem | pwel 5305 | Quantitative version of pwexg 5302: the powerset of an element of a class is an element of the double powerclass of the union of that class. Exercise 10 of [Enderton] p. 26. (Contributed by NM, 13-Jan-2007.) Remove use of ax-nul 5231 and ax-pr 5353 and shorten proof. (Revised by BJ, 13-Apr-2024.) |
⊢ (𝐴 ∈ 𝐵 → 𝒫 𝐴 ∈ 𝒫 𝒫 ∪ 𝐵) | ||
Theorem | abssexg 5306* | Existence of a class of subsets. (Contributed by NM, 15-Jul-2006.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ 𝜑)} ∈ V) | ||
Theorem | snexALT 5307 | Alternate proof of snex 5355 using Power Set (ax-pow 5289) instead of Pairing (ax-pr 5353). Unlike in the proof of zfpair 5345, Replacement (ax-rep 5210) is not needed. (Contributed by NM, 7-Aug-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ {𝐴} ∈ V | ||
Theorem | p0ex 5308 | The power set of the empty set (the ordinal 1) is a set. See also p0exALT 5309. (Contributed by NM, 23-Dec-1993.) |
⊢ {∅} ∈ V | ||
Theorem | p0exALT 5309 | Alternate proof of p0ex 5308 which is quite different and longer if snexALT 5307 is expanded. (Contributed by NM, 23-Dec-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ {∅} ∈ V | ||
Theorem | pp0ex 5310 | The power set of the power set of the empty set (the ordinal 2) is a set. (Contributed by NM, 24-Jun-1993.) |
⊢ {∅, {∅}} ∈ V | ||
Theorem | ord3ex 5311 | The ordinal number 3 is a set, proved without the Axiom of Union ax-un 7597. (Contributed by NM, 2-May-2009.) |
⊢ {∅, {∅}, {∅, {∅}}} ∈ V | ||
Theorem | dtruALT 5312* |
Alternate proof of dtru 5360 which requires more axioms but is shorter and
may be easier to understand.
Assuming that ZF set theory is consistent, we cannot prove this theorem unless we specify that 𝑥 and 𝑦 be distinct. Specifically, Theorem spcev 3546 requires that 𝑥 must not occur in the subexpression ¬ 𝑦 = {∅} in step 4 nor in the subexpression ¬ 𝑦 = ∅ in step 9. The proof verifier will require that 𝑥 and 𝑦 be in a distinct variable group to ensure this. You can check this by deleting the $d statement in set.mm and rerunning the verifier, which will print a detailed explanation of the distinct variable violation. (Contributed by NM, 15-Jul-1994.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ¬ ∀𝑥 𝑥 = 𝑦 | ||
Theorem | axc16b 5313* | This theorem shows that Axiom ax-c16 36913 is redundant in the presence of Theorem dtruALT2 5294, which states simply that at least two things exist. This justifies the remark at mmzfcnd.html#twoness 5294 (which links to this theorem). (Proof modification is discouraged.) (New usage is discouraged.) (Contributed by NM, 7-Nov-2006.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑)) | ||
Theorem | eunex 5314 | Existential uniqueness implies there is a value for which the wff argument is false. (Contributed by NM, 24-Oct-2010.) (Proof shortened by BJ, 2-Jan-2023.) |
⊢ (∃!𝑥𝜑 → ∃𝑥 ¬ 𝜑) | ||
Theorem | eusv1 5315* | Two ways to express single-valuedness of a class expression 𝐴(𝑥). (Contributed by NM, 14-Oct-2010.) |
⊢ (∃!𝑦∀𝑥 𝑦 = 𝐴 ↔ ∃𝑦∀𝑥 𝑦 = 𝐴) | ||
Theorem | eusvnf 5316* | Even if 𝑥 is free in 𝐴, it is effectively bound when 𝐴(𝑥) is single-valued. (Contributed by NM, 14-Oct-2010.) (Revised by Mario Carneiro, 14-Oct-2016.) |
⊢ (∃!𝑦∀𝑥 𝑦 = 𝐴 → Ⅎ𝑥𝐴) | ||
Theorem | eusvnfb 5317* | Two ways to say that 𝐴(𝑥) is a set expression that does not depend on 𝑥. (Contributed by Mario Carneiro, 18-Nov-2016.) |
⊢ (∃!𝑦∀𝑥 𝑦 = 𝐴 ↔ (Ⅎ𝑥𝐴 ∧ 𝐴 ∈ V)) | ||
Theorem | eusv2i 5318* | Two ways to express single-valuedness of a class expression 𝐴(𝑥). (Contributed by NM, 14-Oct-2010.) (Revised by Mario Carneiro, 18-Nov-2016.) |
⊢ (∃!𝑦∀𝑥 𝑦 = 𝐴 → ∃!𝑦∃𝑥 𝑦 = 𝐴) | ||
Theorem | eusv2nf 5319* | Two ways to express single-valuedness of a class expression 𝐴(𝑥). (Contributed by Mario Carneiro, 18-Nov-2016.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (∃!𝑦∃𝑥 𝑦 = 𝐴 ↔ Ⅎ𝑥𝐴) | ||
Theorem | eusv2 5320* | Two ways to express single-valuedness of a class expression 𝐴(𝑥). (Contributed by NM, 15-Oct-2010.) (Proof shortened by Mario Carneiro, 18-Nov-2016.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (∃!𝑦∃𝑥 𝑦 = 𝐴 ↔ ∃!𝑦∀𝑥 𝑦 = 𝐴) | ||
Theorem | reusv1 5321* | Two ways to express single-valuedness of a class expression 𝐶(𝑦). (Contributed by NM, 16-Dec-2012.) (Proof shortened by Mario Carneiro, 18-Nov-2016.) (Proof shortened by JJ, 7-Aug-2021.) |
⊢ (∃𝑦 ∈ 𝐵 𝜑 → (∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶) ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶))) | ||
Theorem | reusv2lem1 5322* | Lemma for reusv2 5327. (Contributed by NM, 22-Oct-2010.) (Proof shortened by Mario Carneiro, 19-Nov-2016.) |
⊢ (𝐴 ≠ ∅ → (∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵)) | ||
Theorem | reusv2lem2 5323* | Lemma for reusv2 5327. (Contributed by NM, 27-Oct-2010.) (Proof shortened by Mario Carneiro, 19-Nov-2016.) (Proof shortened by JJ, 7-Aug-2021.) |
⊢ (∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵) | ||
Theorem | reusv2lem3 5324* | Lemma for reusv2 5327. (Contributed by NM, 14-Dec-2012.) (Proof shortened by Mario Carneiro, 19-Nov-2016.) |
⊢ (∀𝑦 ∈ 𝐴 𝐵 ∈ V → (∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵)) | ||
Theorem | reusv2lem4 5325* | Lemma for reusv2 5327. (Contributed by NM, 13-Dec-2012.) |
⊢ (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝑥 = 𝐶) ↔ ∃!𝑥∀𝑦 ∈ 𝐵 ((𝐶 ∈ 𝐴 ∧ 𝜑) → 𝑥 = 𝐶)) | ||
Theorem | reusv2lem5 5326* | Lemma for reusv2 5327. (Contributed by NM, 4-Jan-2013.) (Proof shortened by Mario Carneiro, 19-Nov-2016.) |
⊢ ((∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐴 ∧ 𝐵 ≠ ∅) → (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 = 𝐶)) | ||
Theorem | reusv2 5327* | Two ways to express single-valuedness of a class expression 𝐶(𝑦) that is constant for those 𝑦 ∈ 𝐵 such that 𝜑. The first antecedent ensures that the constant value belongs to the existential uniqueness domain 𝐴, and the second ensures that 𝐶(𝑦) is evaluated for at least one 𝑦. (Contributed by NM, 4-Jan-2013.) (Proof shortened by Mario Carneiro, 19-Nov-2016.) |
⊢ ((∀𝑦 ∈ 𝐵 (𝜑 → 𝐶 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐵 𝜑) → (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝑥 = 𝐶) ↔ ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶))) | ||
Theorem | reusv3i 5328* | Two ways of expressing existential uniqueness via an indirect equality. (Contributed by NM, 23-Dec-2012.) |
⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝑧 → 𝐶 = 𝐷) ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝜑 ∧ 𝜓) → 𝐶 = 𝐷)) | ||
Theorem | reusv3 5329* | Two ways to express single-valuedness of a class expression 𝐶(𝑦). See reusv1 5321 for the connection to uniqueness. (Contributed by NM, 27-Dec-2012.) |
⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝑧 → 𝐶 = 𝐷) ⇒ ⊢ (∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝐶 ∈ 𝐴) → (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝜑 ∧ 𝜓) → 𝐶 = 𝐷) ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶))) | ||
Theorem | eusv4 5330* | Two ways to express single-valuedness of a class expression 𝐵(𝑦). (Contributed by NM, 27-Oct-2010.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃!𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵) | ||
Theorem | alxfr 5331* | Transfer universal quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by NM, 18-Feb-2007.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((∀𝑦 𝐴 ∈ 𝐵 ∧ ∀𝑥∃𝑦 𝑥 = 𝐴) → (∀𝑥𝜑 ↔ ∀𝑦𝜓)) | ||
Theorem | ralxfrd 5332* | Transfer universal quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by NM, 15-Aug-2014.) (Proof shortened by Mario Carneiro, 19-Nov-2016.) (Proof shortened by JJ, 7-Aug-2021.) |
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐶 𝑥 = 𝐴) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐶 𝜒)) | ||
Theorem | rexxfrd 5333* | Transfer universal quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by FL, 10-Apr-2007.) (Revised by Mario Carneiro, 15-Aug-2014.) |
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐶 𝑥 = 𝐴) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐵 𝜓 ↔ ∃𝑦 ∈ 𝐶 𝜒)) | ||
Theorem | ralxfr2d 5334* | Transfer universal quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by Mario Carneiro, 20-Aug-2014.) |
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐶 𝑥 = 𝐴)) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐶 𝜒)) | ||
Theorem | rexxfr2d 5335* | 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 5336* | Transfer universal quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. Variant of ralxfrd 5332. (Contributed by Alexander van der Vekens, 25-Apr-2018.) |
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐶 𝑥 = 𝐴) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐶 𝜒)) | ||
Theorem | rexxfrd2 5337* | Transfer existence from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. Variant of rexxfrd 5333. (Contributed by Alexander van der Vekens, 25-Apr-2018.) |
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐶 𝑥 = 𝐴) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐵 𝜓 ↔ ∃𝑦 ∈ 𝐶 𝜒)) | ||
Theorem | ralxfr 5338* | 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 5339* | Alternate proof of ralxfr 5338 which does not use ralxfrd 5332. (Contributed by NM, 10-Jun-2005.) (Revised by Mario Carneiro, 15-Aug-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑦 ∈ 𝐶 → 𝐴 ∈ 𝐵) & ⊢ (𝑥 ∈ 𝐵 → ∃𝑦 ∈ 𝐶 𝑥 = 𝐴) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐶 𝜓) | ||
Theorem | rexxfr 5340* | 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 5341* | 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 5342* | 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 5343* | A theorem useful for eliminating the restricted existential uniqueness hypotheses in riotaxfrd 7276. (Contributed by NM, 16-Jan-2012.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐵 ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶) → (𝑥 = 𝐴 ↔ 𝑦 = 𝐵)) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ∃!𝑦 ∈ 𝐶 𝑥 = 𝐴) | ||
Theorem | reuhyp 5344* | A theorem useful for eliminating the restricted existential uniqueness hypotheses in reuxfr1 3688. (Contributed by NM, 15-Nov-2004.) |
⊢ (𝑥 ∈ 𝐶 → 𝐵 ∈ 𝐶) & ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶) → (𝑥 = 𝐴 ↔ 𝑦 = 𝐵)) ⇒ ⊢ (𝑥 ∈ 𝐶 → ∃!𝑦 ∈ 𝐶 𝑥 = 𝐴) | ||
Theorem | zfpair 5345 |
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 5346. Instead, use zfpair2 5354 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 5346* | Alternate proof of axpr 5352. (Contributed by NM, 14-Nov-2006.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧) | ||
Theorem | axprlem1 5347* | Lemma for axpr 5352. 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 5348* | Lemma for axpr 5352. 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 5349* | Lemma for axpr 5352. Eliminate the antecedent of the relevant replacement instance. (Contributed by Rohan Ridenour, 10-Aug-2023.) |
⊢ ∃𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) | ||
Theorem | axprlem4 5350* | Lemma for axpr 5352. 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 5351* | Lemma for axpr 5352. 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 5352* |
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 5353 below so that the uses of the Axiom of Pairing can be more easily identified. For a shorter proof using ax-ext 2710, see axprALT 5346. (Contributed by NM, 14-Nov-2006.) Remove dependency on ax-ext 2710. (Revised by Rohan Ridenour, 10-Aug-2023.) (Proof shortened by BJ, 13-Aug-2023.) Use ax-pr 5353 instead. (New usage is discouraged.) |
⊢ ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧) | ||
Axiom | ax-pr 5353* | The Axiom of Pairing of ZF set theory. It was derived as Theorem axpr 5352 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 5354 | Derive the abbreviated version of the Axiom of Pairing from ax-pr 5353. See zfpair 5345 for its derivation from the other axioms. (Contributed by NM, 14-Nov-2006.) |
⊢ {𝑥, 𝑦} ∈ V | ||
Theorem | snex 5355 | A singleton is a set. Theorem 7.12 of [Quine] p. 51, proved using Extensionality, Separation, Null Set, and Pairing. See also snexALT 5307. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 19-May-2013.) (Proof modification is discouraged.) |
⊢ {𝐴} ∈ V | ||
Theorem | prex 5356 | 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 4704), so we can dispense with hypotheses requiring them to be sets. (Contributed by NM, 15-Jul-1993.) |
⊢ {𝐴, 𝐵} ∈ V | ||
Theorem | sels 5357* | If a class is a set, then it is a member of a set. (Contributed by BJ, 3-Apr-2019.) |
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝐴 ∈ 𝑥) | ||
Theorem | el 5358* | Every set is an element of some other set. See elALT 5359 for a shorter proof using more axioms, and see elALT2 5293 for a proof that uses ax-9 2117 and ax-pow 5289 instead of ax-pr 5353. (Contributed by NM, 4-Jan-2002.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) Avoid ax-9 2117, ax-pow 5289. (Revised by BTernaryTau, 2-Dec-2024.) |
⊢ ∃𝑦 𝑥 ∈ 𝑦 | ||
Theorem | elALT 5359* | Alternate proof of el 5358, shorter but requiring more axioms. (Contributed by NM, 4-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ∃𝑦 𝑥 ∈ 𝑦 | ||
Theorem | dtru 5360* |
At least two sets exist (or in terms of first-order logic, the universe
of discourse has two or more objects). Note that we may not substitute
the same variable for both 𝑥 and 𝑦 (as indicated by the
distinct
variable requirement), for otherwise we would contradict stdpc6 2032.
This theorem is proved directly from set theory axioms (no set theory definitions) and does not use ax-ext 2710, ax-sep 5224, or ax-pow 5289. See dtruALT 5312 for a shorter proof using these axioms, and see dtruALT2 5294 for a proof that uses ax-pow 5289 instead of ax-pr 5353. The proof makes use of dummy variables 𝑧 and 𝑤 which do not appear in the final theorem. They must be distinct from each other and from 𝑥 and 𝑦. In other words, if we were to substitute 𝑥 for 𝑧 throughout the proof, the proof would fail. (Contributed by NM, 7-Nov-2006.) Avoid ax-13 2373. (Revised by Gino Giotto, 5-Sep-2023.) Avoid ax-12 2172. (Revised by Rohan Ridenour, 9-Oct-2024.) Use ax-pr 5353 instead of ax-pow 5289. (Revised by BTernaryTau, 3-Dec-2024.) |
⊢ ¬ ∀𝑥 𝑥 = 𝑦 | ||
Theorem | snelpwi 5361 | A singleton of a set belongs to the power class of a class containing the set. (Contributed by Alan Sare, 25-Aug-2011.) |
⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ 𝒫 𝐵) | ||
Theorem | snelpw 5362 | A singleton of a set belongs to the power class of a class containing the set. (Contributed by NM, 1-Apr-1998.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ 𝒫 𝐵) | ||
Theorem | prelpw 5363 | A pair of two sets belongs to the power class of a class containing those two sets and vice versa. (Contributed by AV, 8-Jan-2020.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ∈ 𝒫 𝐶)) | ||
Theorem | prelpwi 5364 | A pair of two sets belongs to the power class of a class containing those two sets. (Contributed by Thierry Arnoux, 10-Mar-2017.) (Proof shortened by AV, 23-Oct-2021.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → {𝐴, 𝐵} ∈ 𝒫 𝐶) | ||
Theorem | rext 5365* | 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 5366 | 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 5367 | 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 5368 | 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 5369 | 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 5370* | An extensionality-like principle defining subclass in terms of subsets. (Contributed by NM, 30-Jun-2004.) |
⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ⊆ 𝐴 → 𝑥 ⊆ 𝐵)) | ||
Theorem | ssext 5371* | 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 5372* | Negation of subclass relationship. Compare nss 3984. (Contributed by NM, 30-Jun-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ (¬ 𝐴 ⊆ 𝐵 ↔ ∃𝑥(𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵)) | ||
Theorem | pweqb 5373 | 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 | intid 5374* | The intersection of all sets to which a set belongs is the singleton of that set. (Contributed by NM, 5-Jun-2009.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ∩ {𝑥 ∣ 𝐴 ∈ 𝑥} = {𝐴} | ||
Theorem | moabex 5375 | "At most one" existence implies a class abstraction exists. (Contributed by NM, 30-Dec-1996.) |
⊢ (∃*𝑥𝜑 → {𝑥 ∣ 𝜑} ∈ V) | ||
Theorem | rmorabex 5376 | Restricted "at most one" existence implies a restricted class abstraction exists. (Contributed by NM, 17-Jun-2017.) |
⊢ (∃*𝑥 ∈ 𝐴 𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V) | ||
Theorem | euabex 5377 | The abstraction of a wff with existential uniqueness exists. (Contributed by NM, 25-Nov-1994.) |
⊢ (∃!𝑥𝜑 → {𝑥 ∣ 𝜑} ∈ V) | ||
Theorem | nnullss 5378* | A nonempty class (even if proper) has a nonempty subset. (Contributed by NM, 23-Aug-2003.) |
⊢ (𝐴 ≠ ∅ → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅)) | ||
Theorem | exss 5379* | Restricted existence in a class (even if proper) implies restricted existence in a subset. (Contributed by NM, 23-Aug-2003.) |
⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑦(𝑦 ⊆ 𝐴 ∧ ∃𝑥 ∈ 𝑦 𝜑)) | ||
Theorem | opex 5380 | 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 5381 | An ordered triple of classes is a set. (Contributed by NM, 3-Apr-2015.) |
⊢ 〈𝐴, 𝐵, 𝐶〉 ∈ V | ||
Theorem | elopg 5382 | Characterization of the elements of an ordered pair. Closed form of elop 5383. (Contributed by BJ, 22-Jun-2019.) (Avoid depending on this detail.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ 〈𝐴, 𝐵〉 ↔ (𝐶 = {𝐴} ∨ 𝐶 = {𝐴, 𝐵}))) | ||
Theorem | elop 5383 | 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 5384 | 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 5385 | 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 5386 | 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 5387 | Extract the first member of an ordered pair. Theorem 73 of [Suppes] p. 42. (See op2ndb 6135 to extract the second member, op1sta 6133 for an alternate version, and op1st 7848 for the preferred version.) (Contributed by NM, 25-Nov-2003.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ∩ ∩ 〈𝐴, 𝐵〉 = 𝐴 | ||
Theorem | brv 5388 | 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 5712. (Contributed by Scott Fenton, 11-Apr-2012.) |
⊢ 𝐴V𝐵 | ||
Theorem | opnz 5389 | 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 5390 | An ordered pair is nonempty if the arguments are sets. (Contributed by Mario Carneiro, 26-Apr-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ 〈𝐴, 𝐵〉 ≠ ∅ | ||
Theorem | opth1 5391 | 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 5392 | 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 5393 | 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 5394 | Equality of the first members of equal ordered pairs. Closed form of opth1 5391. (Contributed by AV, 14-Oct-2018.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → 𝐴 = 𝐶)) | ||
Theorem | opthg2 5395 | Ordered pair theorem. (Contributed by NM, 14-Oct-2005.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) → (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) | ||
Theorem | opth2 5396 | Ordered pair theorem. (Contributed by NM, 21-Sep-2014.) |
⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | opthneg 5397 | 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 5398 | 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 5399 | 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 5400 | Ordered triple theorem. (Contributed by NM, 25-Sep-2014.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝑅 ∈ V ⇒ ⊢ (〈𝐴, 𝐵, 𝑅〉 = 〈𝐶, 𝐷, 𝑆〉 ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ∧ 𝑅 = 𝑆)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |