Home | Metamath
Proof Explorer Theorem List (p. 361 of 449) | < 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-28689) |
Hilbert Space Explorer
(28690-30212) |
Users' Mathboxes
(30213-44899) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | wprt 36001 | Extend the definition of a wff to include the partition predicate. |
wff Prt 𝐴 | ||
Definition | df-prt 36002* | Define the partition predicate. (Contributed by Rodolfo Medina, 13-Oct-2010.) |
⊢ (Prt 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅)) | ||
Theorem | erprt 36003 | The quotient set of an equivalence relation is a partition. (Contributed by Rodolfo Medina, 13-Oct-2010.) |
⊢ ( ∼ Er 𝑋 → Prt (𝐴 / ∼ )) | ||
Theorem | prtlem14 36004* | Lemma for prter1 36009, prter2 36011 and prtex 36010. (Contributed by Rodolfo Medina, 13-Oct-2010.) |
⊢ (Prt 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑤 ∈ 𝑥 ∧ 𝑤 ∈ 𝑦) → 𝑥 = 𝑦))) | ||
Theorem | prtlem15 36005* | Lemma for prter1 36009 and prtex 36010. (Contributed by Rodolfo Medina, 13-Oct-2010.) |
⊢ (Prt 𝐴 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑢 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) ∧ (𝑤 ∈ 𝑦 ∧ 𝑣 ∈ 𝑦)) → ∃𝑧 ∈ 𝐴 (𝑢 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧))) | ||
Theorem | prtlem17 36006* | Lemma for prter2 36011. (Contributed by Rodolfo Medina, 15-Oct-2010.) |
⊢ (Prt 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥) → (∃𝑦 ∈ 𝐴 (𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦) → 𝑤 ∈ 𝑥))) | ||
Theorem | prtlem18 36007* | Lemma for prter2 36011. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ (Prt 𝐴 → ((𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣) → (𝑤 ∈ 𝑣 ↔ 𝑧 ∼ 𝑤))) | ||
Theorem | prtlem19 36008* | Lemma for prter2 36011. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ (Prt 𝐴 → ((𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣) → 𝑣 = [𝑧] ∼ )) | ||
Theorem | prter1 36009* | Every partition generates an equivalence relation. (Contributed by Rodolfo Medina, 13-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ (Prt 𝐴 → ∼ Er ∪ 𝐴) | ||
Theorem | prtex 36010* | The equivalence relation generated by a partition is a set if and only if the partition itself is a set. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ (Prt 𝐴 → ( ∼ ∈ V ↔ 𝐴 ∈ V)) | ||
Theorem | prter2 36011* | The quotient set of the equivalence relation generated by a partition equals the partition itself. (Contributed by Rodolfo Medina, 17-Oct-2010.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ (Prt 𝐴 → (∪ 𝐴 / ∼ ) = (𝐴 ∖ {∅})) | ||
Theorem | prter3 36012* | For every partition there exists a unique equivalence relation whose quotient set equals the partition. (Contributed by Rodolfo Medina, 19-Oct-2010.) (Proof shortened by Mario Carneiro, 12-Aug-2015.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ ((𝑆 Er ∪ 𝐴 ∧ (∪ 𝐴 / 𝑆) = (𝐴 ∖ {∅})) → ∼ = 𝑆) | ||
We are sad to report the passing of Metamath creator and long-time contributor Norm Megill (1950 - 2021). Norm of course was the author of the Metamath proof language, the specification, all of the early tools (and some of the later ones), and the foundational work in logic and set theory for set.mm. His tools, now at https://github.com/metamath/metamath-exe , include a proof verifier, a proof assistant, a proof minimizer, style checking and reformatting, and tools for searching and displaying proofs. One of his key insights was that formal proofs can exist not only to be verified by computers, but also to be read by humans. Both the specification of the proof format (which stores full proofs, as opposed to the proof templates used by most proof assistants) and the generated web display of Metamath proofs, one of its distinctive features, contribute to this double objective. Metamath innovated both by using a very simple substitution rule (and then using that to build more complicated notions like free and bound variables) and also by taking the axiom schemas found in many theories and taking them to the next level - by making all axioms, theorems and proofs operate in terms of schemas. Not content to create Metamath for his own amusement, he also published it for the world and encouraged the development of a community of people who contributed to it and created their own tools. He was an active participant in the Metamath mailing list and other forums until days before his passing. It is often our custom to supply a quote from someone memorialized in a mathbox entry. And it is difficult to select a quote for someone who has written so much about Metamath over the years. But here is one quote from the Metamath web page which illustrates not just his clear thinking about what Metamath can and cannot do but also his desire to encourage students at all levels: Q: Will Metamath help me learn abstract mathematics? A: Yes, but probably not by itself. In order to follow a proof in an advanced math textbook, you may need to know prerequisites that could take years to learn. Some people find this frustrating. In contrast, Metamath uses a single, simple substitution rule that allows you to follow any proof mechanically. You can actually jump in anywhere and be convinced that the symbol string you see in a proof step is a consequence of the symbol strings in the earlier steps that it references, even if you don't understand what the symbols mean. But this is quite different from understanding the meaning of the math that results. Metamath alone probably will not give you an intuitive feel for abstract math, in the same way it can be hard to grasp a large computer program just by reading its source code, even though you may understand each individual instruction. However, the Bibliographic Cross-Reference lets you compare informal proofs in math textbooks and see all the implicit missing details "left to the reader." | ||
These older axiom schemes are obsolete and should not be used outside of this section. They are proved above as theorems axc4 , sp 2177, axc7 2332, axc10 2399, axc11 2448, axc11n 2444, axc15 2440, axc9 2396, axc14 2482, and axc16 2257. | ||
Axiom | ax-c5 36013 |
Axiom of Specialization. A quantified wff implies the wff without a
quantifier (i.e. an instance, or special case, of the generalized wff).
In other words if something is true for all 𝑥, it is true for any
specific 𝑥 (that would typically occur as a free
variable in the wff
substituted for 𝜑). (A free variable is one that does
not occur in
the scope of a quantifier: 𝑥 and 𝑦 are both free in 𝑥 = 𝑦,
but only 𝑥 is free in ∀𝑦𝑥 = 𝑦.) Axiom scheme C5' in [Megill]
p. 448 (p. 16 of the preprint). Also appears as Axiom B5 of [Tarski]
p. 67 (under his system S2, defined in the last paragraph on p. 77).
Note that the converse of this axiom does not hold in general, but a weaker inference form of the converse holds and is expressed as rule ax-gen 1792. Conditional forms of the converse are given by ax-13 2386, ax-c14 36021, ax-c16 36022, and ax-5 1907. Unlike the more general textbook Axiom of Specialization, we cannot choose a variable different from 𝑥 for the special case. For use, that requires the assistance of equality axioms, and we deal with it later after we introduce the definition of proper substitution - see stdpc4 2069. An interesting alternate axiomatization uses axc5c711 36048 and ax-c4 36014 in place of ax-c5 36013, ax-4 1806, ax-10 2141, and ax-11 2156. This axiom is obsolete and should no longer be used. It is proved above as theorem sp 2177. (Contributed by NM, 3-Jan-1993.) (New usage is discouraged.) |
⊢ (∀𝑥𝜑 → 𝜑) | ||
Axiom | ax-c4 36014 |
Axiom of Quantified Implication. This axiom moves a quantifier from
outside to inside an implication, quantifying 𝜓. Notice that 𝑥
must not be a free variable in the antecedent of the quantified
implication, and we express this by binding 𝜑 to "protect" the
axiom
from a 𝜑 containing a free 𝑥. Axiom
scheme C4' in [Megill]
p. 448 (p. 16 of the preprint). It is a special case of Lemma 5 of
[Monk2] p. 108 and Axiom 5 of [Mendelson] p. 69.
This axiom is obsolete and should no longer be used. It is proved above as theorem axc4 2336. (Contributed by NM, 3-Jan-1993.) (New usage is discouraged.) |
⊢ (∀𝑥(∀𝑥𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓)) | ||
Axiom | ax-c7 36015 |
Axiom of Quantified Negation. This axiom is used to manipulate negated
quantifiers. Equivalent to axiom scheme C7' in [Megill] p. 448 (p. 16 of
the preprint). An alternate axiomatization could use axc5c711 36048 in place
of ax-c5 36013, ax-c7 36015, and ax-11 2156.
This axiom is obsolete and should no longer be used. It is proved above as theorem axc7 2332. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑) | ||
Axiom | ax-c10 36016 |
A variant of ax6 2398. Axiom scheme C10' in [Megill] p. 448 (p. 16 of the
preprint).
This axiom is obsolete and should no longer be used. It is proved above as theorem axc10 2399. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.) |
⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) → 𝜑) | ||
Axiom | ax-c11 36017 |
Axiom ax-c11 36017 was the original version of ax-c11n 36018 ("n" for "new"),
before it was discovered (in May 2008) that the shorter ax-c11n 36018 could
replace it. It appears as Axiom scheme C11' in [Megill] p. 448 (p. 16 of
the preprint).
This axiom is obsolete and should no longer be used. It is proved above as theorem axc11 2448. (Contributed by NM, 10-May-1993.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑)) | ||
Axiom | ax-c11n 36018 |
Axiom of Quantifier Substitution. One of the equality and substitution
axioms of predicate calculus with equality. Appears as Lemma L12 in
[Megill] p. 445 (p. 12 of the preprint).
The original version of this axiom was ax-c11 36017 and was replaced with this shorter ax-c11n 36018 ("n" for "new") in May 2008. The old axiom is proved from this one as theorem axc11 2448. Conversely, this axiom is proved from ax-c11 36017 as theorem axc11nfromc11 36056. This axiom was proved redundant in July 2015. See theorem axc11n 2444. This axiom is obsolete and should no longer be used. It is proved above as theorem axc11n 2444. (Contributed by NM, 16-May-2008.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥) | ||
Axiom | ax-c15 36019 |
Axiom ax-c15 36019 was the original version of ax-12 2172, before it was
discovered (in Jan. 2007) that the shorter ax-12 2172 could replace it. It
appears as Axiom scheme C15' in [Megill]
p. 448 (p. 16 of the preprint).
It is based on Lemma 16 of [Tarski] p. 70
and Axiom C8 of [Monk2] p. 105,
from which it can be proved by cases. To understand this theorem more
easily, think of "¬ ∀𝑥𝑥 = 𝑦 →..." as informally meaning
"if
𝑥 and 𝑦 are distinct variables
then..." The antecedent becomes
false if the same variable is substituted for 𝑥 and 𝑦,
ensuring
the theorem is sound whenever this is the case. In some later theorems,
we call an antecedent of the form ¬ ∀𝑥𝑥 = 𝑦 a "distinctor."
Interestingly, if the wff expression substituted for 𝜑 contains no wff variables, the resulting statement can be proved without invoking this axiom. This means that even though this axiom is metalogically independent from the others, it is not logically independent. Specifically, we can prove any wff-variable-free instance of axiom ax-c15 36019 (from which the ax-12 2172 instance follows by theorem ax12 2441.) The proof is by induction on formula length, using ax12eq 36071 and ax12el 36072 for the basis steps and ax12indn 36073, ax12indi 36074, and ax12inda 36078 for the induction steps. (This paragraph is true provided we use ax-c11 36017 in place of ax-c11n 36018.) This axiom is obsolete and should no longer be used. It is proved above as theorem axc15 2440, which should be used instead. (Contributed by NM, 14-May-1993.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) | ||
Axiom | ax-c9 36020 |
Axiom of Quantifier Introduction. One of the equality and substitution
axioms of predicate calculus with equality. Informally, it says that
whenever 𝑧 is distinct from 𝑥 and
𝑦,
and 𝑥 =
𝑦 is true,
then 𝑥 = 𝑦 quantified with 𝑧 is also
true. In other words, 𝑧
is irrelevant to the truth of 𝑥 = 𝑦. Axiom scheme C9' in [Megill]
p. 448 (p. 16 of the preprint). It apparently does not otherwise appear
in the literature but is easily proved from textbook predicate calculus by
cases.
This axiom is obsolete and should no longer be used. It is proved above as theorem axc9 2396. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.) |
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))) | ||
Axiom | ax-c14 36021 |
Axiom of Quantifier Introduction. One of the equality and substitution
axioms for a non-logical predicate in our predicate calculus with
equality. Axiom scheme C14' in [Megill]
p. 448 (p. 16 of the preprint).
It is redundant if we include ax-5 1907; see theorem axc14 2482. Alternately,
ax-5 1907 becomes unnecessary in principle with this
axiom, but we lose the
more powerful metalogic afforded by ax-5 1907.
We retain ax-c14 36021 here to
provide completeness for systems with the simpler metalogic that results
from omitting ax-5 1907, which might be easier to study for some
theoretical
purposes.
This axiom is obsolete and should no longer be used. It is proved above as theorem axc14 2482. (Contributed by NM, 24-Jun-1993.) (New usage is discouraged.) |
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦))) | ||
Axiom | ax-c16 36022* |
Axiom of Distinct Variables. The only axiom of predicate calculus
requiring that variables be distinct (if we consider ax-5 1907
to be a
metatheorem and not an axiom). Axiom scheme C16' in [Megill] p. 448 (p.
16 of the preprint). It apparently does not otherwise appear in the
literature but is easily proved from textbook predicate calculus by
cases. It is a somewhat bizarre axiom since the antecedent is always
false in set theory (see dtru 5264), but nonetheless it is technically
necessary as you can see from its uses.
This axiom is redundant if we include ax-5 1907; see theorem axc16 2257. Alternately, ax-5 1907 becomes logically redundant in the presence of this axiom, but without ax-5 1907 we lose the more powerful metalogic that results from being able to express the concept of a setvar variable not occurring in a wff (as opposed to just two setvar variables being distinct). We retain ax-c16 36022 here to provide logical completeness for systems with the simpler metalogic that results from omitting ax-5 1907, which might be easier to study for some theoretical purposes. This axiom is obsolete and should no longer be used. It is proved above as theorem axc16 2257. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑)) | ||
Theorems ax12fromc15 36035 and ax13fromc9 36036 require some intermediate theorems that are included in this section. | ||
Theorem | axc5 36023 | This theorem repeats sp 2177 under the name axc5 36023, so that the Metamath program "MM> VERIFY MARKUP" command will check that it matches axiom scheme ax-c5 36013. (Contributed by NM, 18-Aug-2017.) (Proof modification is discouraged.) Use sp 2177 instead. (New usage is discouraged.) |
⊢ (∀𝑥𝜑 → 𝜑) | ||
Theorem | ax4fromc4 36024 | Rederivation of axiom ax-4 1806 from ax-c4 36014, ax-c5 36013, ax-gen 1792 and minimal implicational calculus { ax-mp 5, ax-1 6, ax-2 7 }. See axc4 2336 for the derivation of ax-c4 36014 from ax-4 1806. (Contributed by NM, 23-May-2008.) (Proof modification is discouraged.) Use ax-4 1806 instead. (New usage is discouraged.) |
⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓)) | ||
Theorem | ax10fromc7 36025 | Rederivation of axiom ax-10 2141 from ax-c7 36015, ax-c4 36014, ax-c5 36013, ax-gen 1792 and propositional calculus. See axc7 2332 for the derivation of ax-c7 36015 from ax-10 2141. (Contributed by NM, 23-May-2008.) (Proof modification is discouraged.) Use ax-10 2141 instead. (New usage is discouraged.) |
⊢ (¬ ∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑) | ||
Theorem | ax6fromc10 36026 | Rederivation of axiom ax-6 1966 from ax-c7 36015, ax-c10 36016, ax-gen 1792 and propositional calculus. See axc10 2399 for the derivation of ax-c10 36016 from ax-6 1966. Lemma L18 in [Megill] p. 446 (p. 14 of the preprint). (Contributed by NM, 14-May-1993.) (Proof modification is discouraged.) Use ax-6 1966 instead. (New usage is discouraged.) |
⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦 | ||
Theorem | hba1-o 36027 | The setvar 𝑥 is not free in ∀𝑥𝜑. Example in Appendix in [Megill] p. 450 (p. 19 of the preprint). Also Lemma 22 of [Monk2] p. 114. (Contributed by NM, 24-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑) | ||
Theorem | axc4i-o 36028 | Inference version of ax-c4 36014. (Contributed by NM, 3-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥𝜑 → 𝜓) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑥𝜓) | ||
Theorem | equid1 36029 | Proof of equid 2015 from our older axioms. This is often an axiom of equality in textbook systems, but we don't need it as an axiom since it can be proved from our other axioms (although the proof, as you can see below, is not as obvious as you might think). This proof uses only axioms without distinct variable conditions and requires no dummy variables. A simpler proof, similar to Tarski's, is possible if we make use of ax-5 1907; see the proof of equid 2015. See equid1ALT 36055 for an alternate proof. (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝑥 = 𝑥 | ||
Theorem | equcomi1 36030 | Proof of equcomi 2020 from equid1 36029, avoiding use of ax-5 1907 (the only use of ax-5 1907 is via ax7 2019, so using ax-7 2011 instead would remove dependency on ax-5 1907). (Contributed by BJ, 8-Jul-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥) | ||
Theorem | aecom-o 36031 | Commutation law for identical variable specifiers. The antecedent and consequent are true when 𝑥 and 𝑦 are substituted with the same variable. Lemma L12 in [Megill] p. 445 (p. 12 of the preprint). Version of aecom 2445 using ax-c11 36017. Unlike axc11nfromc11 36056, this version does not require ax-5 1907 (see comment of equcomi1 36030). (Contributed by NM, 10-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥) | ||
Theorem | aecoms-o 36032 | A commutation rule for identical variable specifiers. Version of aecoms 2446 using ax-c11 36017. (Contributed by NM, 10-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → 𝜑) ⇒ ⊢ (∀𝑦 𝑦 = 𝑥 → 𝜑) | ||
Theorem | hbae-o 36033 | All variables are effectively bound in an identical variable specifier. Version of hbae 2449 using ax-c11 36017. (Contributed by NM, 13-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦) | ||
Theorem | dral1-o 36034 | Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). Version of dral1 2457 using ax-c11 36017. (Contributed by NM, 24-Nov-1994.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 ↔ ∀𝑦𝜓)) | ||
Theorem | ax12fromc15 36035 |
Rederivation of axiom ax-12 2172 from ax-c15 36019, ax-c11 36017 (used through
dral1-o 36034), and other older axioms. See theorem axc15 2440 for the
derivation of ax-c15 36019 from ax-12 2172.
An open problem is whether we can prove this using ax-c11n 36018 instead of ax-c11 36017. This proof uses newer axioms ax-4 1806 and ax-6 1966, but since these are proved from the older axioms above, this is acceptable and lets us avoid having to reprove several earlier theorems to use ax-c4 36014 and ax-c10 36016. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | ax13fromc9 36036 |
Derive ax-13 2386 from ax-c9 36020 and other older axioms.
This proof uses newer axioms ax-4 1806 and ax-6 1966, but since these are proved from the older axioms above, this is acceptable and lets us avoid having to reprove several earlier theorems to use ax-c4 36014 and ax-c10 36016. (Contributed by NM, 21-Dec-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) | ||
These theorems were mostly intended to study properties of the older axiom schemes and are not useful outside of this section. They should not be used outside of this section. They may be deleted when they are deemed to no longer be of interest. | ||
Theorem | ax5ALT 36037* |
Axiom to quantify a variable over a formula in which it does not occur.
Axiom C5 in [Megill] p. 444 (p. 11 of
the preprint). Also appears as
Axiom B6 (p. 75) of system S2 of [Tarski] p. 77 and Axiom C5-1 of
[Monk2] p. 113.
(This theorem simply repeats ax-5 1907 so that we can include the following note, which applies only to the obsolete axiomatization.) This axiom is logically redundant in the (logically complete) predicate calculus axiom system consisting of ax-gen 1792, ax-c4 36014, ax-c5 36013, ax-11 2156, ax-c7 36015, ax-7 2011, ax-c9 36020, ax-c10 36016, ax-c11 36017, ax-8 2112, ax-9 2120, ax-c14 36021, ax-c15 36019, and ax-c16 36022: in that system, we can derive any instance of ax-5 1907 not containing wff variables by induction on formula length, using ax5eq 36062 and ax5el 36067 for the basis together with hbn 2299, hbal 2169, and hbim 2303. However, if we omit this axiom, our development would be quite inconvenient since we could work only with specific instances of wffs containing no wff variables - this axiom introduces the concept of a setvar variable not occurring in a wff (as opposed to just two setvar variables being distinct). (Contributed by NM, 19-Aug-2017.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝜑 → ∀𝑥𝜑) | ||
Theorem | sps-o 36038 | Generalization of antecedent. (Contributed by NM, 5-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
Theorem | hbequid 36039 | Bound-variable hypothesis builder for 𝑥 = 𝑥. This theorem tells us that any variable, including 𝑥, is effectively not free in 𝑥 = 𝑥, even though 𝑥 is technically free according to the traditional definition of free variable. (The proof does not use ax-c10 36016.) (Contributed by NM, 13-Jan-2011.) (Proof shortened by Wolf Lammen, 23-Mar-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑥 → ∀𝑦 𝑥 = 𝑥) | ||
Theorem | nfequid-o 36040 | Bound-variable hypothesis builder for 𝑥 = 𝑥. This theorem tells us that any variable, including 𝑥, is effectively not free in 𝑥 = 𝑥, even though 𝑥 is technically free according to the traditional definition of free variable. (The proof uses only ax-4 1806, ax-7 2011, ax-c9 36020, and ax-gen 1792. This shows that this can be proved without ax6 2398, even though the theorem equid 2015 cannot be. A shorter proof using ax6 2398 is obtainable from equid 2015 and hbth 1800.) Remark added 2-Dec-2015 NM: This proof does implicitly use ax6v 1967, which is used for the derivation of axc9 2396, unless we consider ax-c9 36020 the starting axiom rather than ax-13 2386. (Contributed by NM, 13-Jan-2011.) (Revised by Mario Carneiro, 12-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑦 𝑥 = 𝑥 | ||
Theorem | axc5c7 36041 | Proof of a single axiom that can replace ax-c5 36013 and ax-c7 36015. See axc5c7toc5 36042 and axc5c7toc7 36043 for the rederivation of those axioms. (Contributed by Scott Fenton, 12-Sep-2005.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((∀𝑥 ¬ ∀𝑥𝜑 → ∀𝑥𝜑) → 𝜑) | ||
Theorem | axc5c7toc5 36042 | Rederivation of ax-c5 36013 from axc5c7 36041. Only propositional calculus is used for the rederivation. (Contributed by Scott Fenton, 12-Sep-2005.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥𝜑 → 𝜑) | ||
Theorem | axc5c7toc7 36043 | Rederivation of ax-c7 36015 from axc5c7 36041. Only propositional calculus is used for the rederivation. (Contributed by Scott Fenton, 12-Sep-2005.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑) | ||
Theorem | axc711 36044 | Proof of a single axiom that can replace both ax-c7 36015 and ax-11 2156. See axc711toc7 36046 and axc711to11 36047 for the rederivation of those axioms. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 ¬ ∀𝑦∀𝑥𝜑 → ∀𝑦𝜑) | ||
Theorem | nfa1-o 36045 | 𝑥 is not free in ∀𝑥𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥∀𝑥𝜑 | ||
Theorem | axc711toc7 36046 | Rederivation of ax-c7 36015 from axc711 36044. Note that ax-c7 36015 and ax-11 2156 are not used by the rederivation. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑) | ||
Theorem | axc711to11 36047 | Rederivation of ax-11 2156 from axc711 36044. Note that ax-c7 36015 and ax-11 2156 are not used by the rederivation. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) | ||
Theorem | axc5c711 36048 | Proof of a single axiom that can replace ax-c5 36013, ax-c7 36015, and ax-11 2156 in a subsystem that includes these axioms plus ax-c4 36014 and ax-gen 1792 (and propositional calculus). See axc5c711toc5 36049, axc5c711toc7 36050, and axc5c711to11 36051 for the rederivation of those axioms. This theorem extends the idea in Scott Fenton's axc5c7 36041. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑 → ∀𝑥𝜑) → 𝜑) | ||
Theorem | axc5c711toc5 36049 | Rederivation of ax-c5 36013 from axc5c711 36048. Only propositional calculus is used by the rederivation. (Contributed by NM, 19-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥𝜑 → 𝜑) | ||
Theorem | axc5c711toc7 36050 | Rederivation of ax-c7 36015 from axc5c711 36048. Note that ax-c7 36015 and ax-11 2156 are not used by the rederivation. The use of alimi 1808 (which uses ax-c5 36013) is allowed since we have already proved axc5c711toc5 36049. (Contributed by NM, 19-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑) | ||
Theorem | axc5c711to11 36051 | Rederivation of ax-11 2156 from axc5c711 36048. Note that ax-c7 36015 and ax-11 2156 are not used by the rederivation. The use of alimi 1808 (which uses ax-c5 36013) is allowed since we have already proved axc5c711toc5 36049. (Contributed by NM, 19-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) | ||
Theorem | equidqe 36052 | equid 2015 with existential quantifier without using ax-c5 36013 or ax-5 1907. (Contributed by NM, 13-Jan-2011.) (Proof shortened by Wolf Lammen, 27-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ¬ ∀𝑦 ¬ 𝑥 = 𝑥 | ||
Theorem | axc5sp1 36053 | A special case of ax-c5 36013 without using ax-c5 36013 or ax-5 1907. (Contributed by NM, 13-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑦 ¬ 𝑥 = 𝑥 → ¬ 𝑥 = 𝑥) | ||
Theorem | equidq 36054 | equid 2015 with universal quantifier without using ax-c5 36013 or ax-5 1907. (Contributed by NM, 13-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ∀𝑦 𝑥 = 𝑥 | ||
Theorem | equid1ALT 36055 | Alternate proof of equid 2015 and equid1 36029 from older axioms ax-c7 36015, ax-c10 36016 and ax-c9 36020. (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝑥 = 𝑥 | ||
Theorem | axc11nfromc11 36056 |
Rederivation of ax-c11n 36018 from original version ax-c11 36017. See theorem
axc11 2448 for the derivation of ax-c11 36017 from ax-c11n 36018.
This theorem should not be referenced in any proof. Instead, use ax-c11n 36018 above so that uses of ax-c11n 36018 can be more easily identified, or use aecom-o 36031 when this form is needed for studies involving ax-c11 36017 and omitting ax-5 1907. (Contributed by NM, 16-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥) | ||
Theorem | naecoms-o 36057 | A commutation rule for distinct variable specifiers. Version of naecoms 2447 using ax-c11 36017. (Contributed by NM, 2-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → 𝜑) ⇒ ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → 𝜑) | ||
Theorem | hbnae-o 36058 | All variables are effectively bound in a distinct variable specifier. Lemma L19 in [Megill] p. 446 (p. 14 of the preprint). Version of hbnae 2450 using ax-c11 36017. (Contributed by NM, 13-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦) | ||
Theorem | dvelimf-o 36059 | Proof of dvelimh 2468 that uses ax-c11 36017 but not ax-c15 36019, ax-c11n 36018, or ax-12 2172. Version of dvelimh 2468 using ax-c11 36017 instead of axc11 2448. (Contributed by NM, 12-Nov-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜓 → ∀𝑧𝜓) & ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓)) | ||
Theorem | dral2-o 36060 | Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). Version of dral2 2456 using ax-c11 36017. (Contributed by NM, 27-Feb-2005.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑧𝜑 ↔ ∀𝑧𝜓)) | ||
Theorem | aev-o 36061* | A "distinctor elimination" lemma with no restrictions on variables in the consequent, proved without using ax-c16 36022. Version of aev 2058 using ax-c11 36017. (Contributed by NM, 8-Nov-2006.) (Proof shortened by Andrew Salmon, 21-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑤 = 𝑣) | ||
Theorem | ax5eq 36062* | Theorem to add distinct quantifier to atomic formula. (This theorem demonstrates the induction basis for ax-5 1907 considered as a metatheorem. Do not use it for later proofs - use ax-5 1907 instead, to avoid reference to the redundant axiom ax-c16 36022.) (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦) | ||
Theorem | dveeq2-o 36063* | Quantifier introduction when one pair of variables is distinct. Version of dveeq2 2392 using ax-c15 36019. (Contributed by NM, 2-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) | ||
Theorem | axc16g-o 36064* | A generalization of axiom ax-c16 36022. Version of axc16g 2256 using ax-c11 36017. (Contributed by NM, 15-May-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑧𝜑)) | ||
Theorem | dveeq1-o 36065* | Quantifier introduction when one pair of variables is distinct. Version of dveeq1 2394 using ax-c11 . (Contributed by NM, 2-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) | ||
Theorem | dveeq1-o16 36066* | Version of dveeq1 2394 using ax-c16 36022 instead of ax-5 1907. (Contributed by NM, 29-Apr-2008.) TODO: Recover proof from older set.mm to remove use of ax-5 1907. (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) | ||
Theorem | ax5el 36067* | Theorem to add distinct quantifier to atomic formula. This theorem demonstrates the induction basis for ax-5 1907 considered as a metatheorem.) (Contributed by NM, 22-Jun-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦) | ||
Theorem | axc11n-16 36068* | This theorem shows that, given ax-c16 36022, we can derive a version of ax-c11n 36018. However, it is weaker than ax-c11n 36018 because it has a distinct variable requirement. (Contributed by Andrew Salmon, 27-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑧 → ∀𝑧 𝑧 = 𝑥) | ||
Theorem | dveel2ALT 36069* | Alternate proof of dveel2 2481 using ax-c16 36022 instead of ax-5 1907. (Contributed by NM, 10-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 ∈ 𝑦 → ∀𝑥 𝑧 ∈ 𝑦)) | ||
Theorem | ax12f 36070 | Basis step for constructing a substitution instance of ax-c15 36019 without using ax-c15 36019. We can start with any formula 𝜑 in which 𝑥 is not free. (Contributed by NM, 21-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥𝜑) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) | ||
Theorem | ax12eq 36071 | Basis step for constructing a substitution instance of ax-c15 36019 without using ax-c15 36019. Atomic formula for equality predicate. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))) | ||
Theorem | ax12el 36072 | Basis step for constructing a substitution instance of ax-c15 36019 without using ax-c15 36019. Atomic formula for membership predicate. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))) | ||
Theorem | ax12indn 36073 | Induction step for constructing a substitution instance of ax-c15 36019 without using ax-c15 36019. Negation case. (Contributed by NM, 21-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (¬ 𝜑 → ∀𝑥(𝑥 = 𝑦 → ¬ 𝜑)))) | ||
Theorem | ax12indi 36074 | Induction step for constructing a substitution instance of ax-c15 36019 without using ax-c15 36019. Implication case. (Contributed by NM, 21-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) & ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜓 → ∀𝑥(𝑥 = 𝑦 → 𝜓)))) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → ((𝜑 → 𝜓) → ∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓))))) | ||
Theorem | ax12indalem 36075 | Lemma for ax12inda2 36077 and ax12inda 36078. (Contributed by NM, 24-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) ⇒ ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))))) | ||
Theorem | ax12inda2ALT 36076* | Alternate proof of ax12inda2 36077, slightly more direct and not requiring ax-c16 36022. (Contributed by NM, 4-May-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))) | ||
Theorem | ax12inda2 36077* | Induction step for constructing a substitution instance of ax-c15 36019 without using ax-c15 36019. Quantification case. When 𝑧 and 𝑦 are distinct, this theorem avoids the dummy variables needed by the more general ax12inda 36078. (Contributed by NM, 24-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))) | ||
Theorem | ax12inda 36078* | Induction step for constructing a substitution instance of ax-c15 36019 without using ax-c15 36019. Quantification case. (When 𝑧 and 𝑦 are distinct, ax12inda2 36077 may be used instead to avoid the dummy variable 𝑤 in the proof.) (Contributed by NM, 24-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑤 → (𝑥 = 𝑤 → (𝜑 → ∀𝑥(𝑥 = 𝑤 → 𝜑)))) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))) | ||
Theorem | ax12v2-o 36079* | Rederivation of ax-c15 36019 from ax12v 2173 (without using ax-c15 36019 or the full ax-12 2172). Thus, the hypothesis (ax12v 2173) provides an alternate axiom that can be used in place of ax-c15 36019. See also axc15 2440. (Contributed by NM, 2-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑧 → (𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑))) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) | ||
Theorem | ax12a2-o 36080* | Derive ax-c15 36019 from a hypothesis in the form of ax-12 2172, without using ax-12 2172 or ax-c15 36019. The hypothesis is weaker than ax-12 2172, with 𝑧 both distinct from 𝑥 and not occurring in 𝜑. Thus, the hypothesis provides an alternate axiom that can be used in place of ax-12 2172, if we also have ax-c11 36017, which this proof uses. As theorem ax12 2441 shows, the distinct variable conditions are optional. An open problem is whether we can derive this with ax-c11n 36018 instead of ax-c11 36017. (Contributed by NM, 2-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑧 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑))) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) | ||
Theorem | axc11-o 36081 |
Show that ax-c11 36017 can be derived from ax-c11n 36018 and ax-12 2172. An open
problem is whether this theorem can be derived from ax-c11n 36018 and the
others when ax-12 2172 is replaced with ax-c15 36019 or ax12v 2173. See theorem
axc11nfromc11 36056 for the rederivation of ax-c11n 36018 from axc11 2448.
Normally, axc11 2448 should be used rather than ax-c11 36017 or axc11-o 36081, except by theorems specifically studying the latter's properties. (Contributed by NM, 16-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑)) | ||
Theorem | fsumshftd 36082* | Index shift of a finite sum with a weaker "implicit substitution" hypothesis than fsumshft 15129. The proof demonstrates how this can be derived starting from from fsumshft 15129. (Contributed by NM, 1-Nov-2019.) |
⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑗 = (𝑘 − 𝐾)) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ (𝑀...𝑁)𝐴 = Σ𝑘 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))𝐵) | ||
Axiom | ax-riotaBAD 36083 | Define restricted description binder. In case it doesn't exist, we return a set which is not a member of the domain of discourse 𝐴. See also comments for df-iota 6309. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) WARNING: THIS "AXIOM", WHICH IS THE OLD df-riota 7108, CONFLICTS WITH (THE NEW) df-riota 7108 AND MAKES THE SYSTEM IN set.mm INCONSISTENT. IT IS TEMPORARY AND WILL BE DELETED AFTER ALL USES ARE ELIMINATED. |
⊢ (℩𝑥 ∈ 𝐴 𝜑) = if(∃!𝑥 ∈ 𝐴 𝜑, (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)), (Undef‘{𝑥 ∣ 𝑥 ∈ 𝐴})) | ||
Theorem | riotaclbgBAD 36084* | Closure of restricted iota. (Contributed by NM, 28-Feb-2013.) (Revised by Mario Carneiro, 24-Dec-2016.) |
⊢ (𝐴 ∈ 𝑉 → (∃!𝑥 ∈ 𝐴 𝜑 ↔ (℩𝑥 ∈ 𝐴 𝜑) ∈ 𝐴)) | ||
Theorem | riotaclbBAD 36085* | Closure of restricted iota. (Contributed by NM, 15-Sep-2011.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (℩𝑥 ∈ 𝐴 𝜑) ∈ 𝐴) | ||
Theorem | riotasvd 36086* | Deduction version of riotasv 36089. (Contributed by NM, 4-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ (𝜑 → 𝐷 = (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜓 → 𝑥 = 𝐶))) & ⊢ (𝜑 → 𝐷 ∈ 𝐴) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → ((𝑦 ∈ 𝐵 ∧ 𝜓) → 𝐷 = 𝐶)) | ||
Theorem | riotasv2d 36087* | Value of description binder 𝐷 for a single-valued class expression 𝐶(𝑦) (as in e.g. reusv2 5296). Special case of riota2f 7132. (Contributed by NM, 2-Mar-2013.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝐹) & ⊢ (𝜑 → Ⅎ𝑦𝜒) & ⊢ (𝜑 → 𝐷 = (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜓 → 𝑥 = 𝐶))) & ⊢ ((𝜑 ∧ 𝑦 = 𝐸) → (𝜓 ↔ 𝜒)) & ⊢ ((𝜑 ∧ 𝑦 = 𝐸) → 𝐶 = 𝐹) & ⊢ (𝜑 → 𝐷 ∈ 𝐴) & ⊢ (𝜑 → 𝐸 ∈ 𝐵) & ⊢ (𝜑 → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → 𝐷 = 𝐹) | ||
Theorem | riotasv2s 36088* | The value of description binder 𝐷 for a single-valued class expression 𝐶(𝑦) (as in e.g. reusv2 5296) in the form of a substitution instance. Special case of riota2f 7132. (Contributed by NM, 3-Mar-2013.) (Proof shortened by Mario Carneiro, 6-Dec-2016.) |
⊢ 𝐷 = (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝐴 ∧ (𝐸 ∈ 𝐵 ∧ [𝐸 / 𝑦]𝜑)) → 𝐷 = ⦋𝐸 / 𝑦⦌𝐶) | ||
Theorem | riotasv 36089* | Value of description binder 𝐷 for a single-valued class expression 𝐶(𝑦) (as in e.g. reusv2 5296). Special case of riota2f 7132. (Contributed by NM, 26-Jan-2013.) (Proof shortened by Mario Carneiro, 6-Dec-2016.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶)) ⇒ ⊢ ((𝐷 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑) → 𝐷 = 𝐶) | ||
Theorem | riotasv3d 36090* | A property 𝜒 holding for a representative of a single-valued class expression 𝐶(𝑦) (see e.g. reusv2 5296) also holds for its description binder 𝐷 (in the form of property 𝜃). (Contributed by NM, 5-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜃) & ⊢ (𝜑 → 𝐷 = (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜓 → 𝑥 = 𝐶))) & ⊢ ((𝜑 ∧ 𝐶 = 𝐷) → (𝜒 ↔ 𝜃)) & ⊢ (𝜑 → ((𝑦 ∈ 𝐵 ∧ 𝜓) → 𝜒)) & ⊢ (𝜑 → 𝐷 ∈ 𝐴) & ⊢ (𝜑 → ∃𝑦 ∈ 𝐵 𝜓) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → 𝜃) | ||
Theorem | elimhyps 36091 | A version of elimhyp 4530 using explicit substitution. (Contributed by NM, 15-Jun-2019.) |
⊢ [𝐵 / 𝑥]𝜑 ⇒ ⊢ [if(𝜑, 𝑥, 𝐵) / 𝑥]𝜑 | ||
Theorem | dedths 36092 | A version of weak deduction theorem dedth 4523 using explicit substitution. (Contributed by NM, 15-Jun-2019.) |
⊢ [if(𝜑, 𝑥, 𝐵) / 𝑥]𝜓 ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | renegclALT 36093 | Closure law for negative of reals. Demonstrates use of weak deduction theorem with explicit substitution. The proof is much longer than that of renegcl 10943. (Contributed by NM, 15-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℝ → -𝐴 ∈ ℝ) | ||
Theorem | elimhyps2 36094 | Generalization of elimhyps 36091 that is not useful unless we can separately prove ⊢ 𝐴 ∈ V. (Contributed by NM, 13-Jun-2019.) |
⊢ [𝐵 / 𝑥]𝜑 ⇒ ⊢ [if([𝐴 / 𝑥]𝜑, 𝐴, 𝐵) / 𝑥]𝜑 | ||
Theorem | dedths2 36095 | Generalization of dedths 36092 that is not useful unless we can separately prove ⊢ 𝐴 ∈ V. (Contributed by NM, 13-Jun-2019.) |
⊢ [if([𝐴 / 𝑥]𝜑, 𝐴, 𝐵) / 𝑥]𝜓 ⇒ ⊢ ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥]𝜓) | ||
Theorem | nfcxfrdf 36096 | A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by NM, 19-Nov-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥𝐴) | ||
Theorem | nfded 36097 | A deduction theorem that converts a not-free inference directly to deduction form. The first hypothesis is the hypothesis of the deduction form. The second is an equality deduction (e.g., (Ⅎ𝑥𝐴 → ∪ {𝑦 ∣ ∀𝑥𝑦 ∈ 𝐴} = ∪ 𝐴)) that starts from abidnf 3694. The last is assigned to the inference form (e.g., Ⅎ𝑥∪ {𝑦 ∣ ∀𝑥𝑦 ∈ 𝐴}) whose hypothesis is satisfied using nfaba1 2986. (Contributed by NM, 19-Nov-2020.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (Ⅎ𝑥𝐴 → 𝐵 = 𝐶) & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝜑 → Ⅎ𝑥𝐶) | ||
Theorem | nfded2 36098 | A deduction theorem that converts a not-free inference directly to deduction form. The first 2 hypotheses are the hypotheses of the deduction form. The third is an equality deduction (e.g., ((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝐵) → 〈{𝑦 ∣ ∀𝑥𝑦 ∈ 𝐴}, {𝑦 ∣ ∀𝑥𝑦 ∈ 𝐵}〉 = 〈𝐴, 𝐵〉) for nfopd 4814) that starts from abidnf 3694. The last is assigned to the inference form (e.g., Ⅎ𝑥〈{𝑦 ∣ ∀𝑥𝑦 ∈ 𝐴}, {𝑦 ∣ ∀𝑥𝑦 ∈ 𝐵}〉 for nfop 4813) whose hypotheses are satisfied using nfaba1 2986. (Contributed by NM, 19-Nov-2020.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝐵) & ⊢ ((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝐵) → 𝐶 = 𝐷) & ⊢ Ⅎ𝑥𝐶 ⇒ ⊢ (𝜑 → Ⅎ𝑥𝐷) | ||
Theorem | nfunidALT2 36099 | Deduction version of nfuni 4839. (Contributed by NM, 19-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥∪ 𝐴) | ||
Theorem | nfunidALT 36100 | Deduction version of nfuni 4839. (Contributed by NM, 19-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥∪ 𝐴) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |