Home | Metamath
Proof Explorer Theorem List (p. 373 of 470) | < 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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | prtlem60 37201 | Lemma for prter3 37230. (Contributed by Rodolfo Medina, 9-Oct-2010.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜓 → (𝜃 → 𝜏)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏))) | ||
Theorem | bicomdd 37202 | Commute two sides of a biconditional in a deduction. (Contributed by Rodolfo Medina, 19-Oct-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))) ⇒ ⊢ (𝜑 → (𝜓 → (𝜃 ↔ 𝜒))) | ||
Theorem | jca2r 37203 | Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 17-Oct-2010.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜓 → 𝜃) ⇒ ⊢ (𝜑 → (𝜓 → (𝜃 ∧ 𝜒))) | ||
Theorem | jca3 37204 | Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 14-Oct-2010.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜃 → 𝜏) ⇒ ⊢ (𝜑 → (𝜓 → (𝜃 → (𝜒 ∧ 𝜏)))) | ||
Theorem | prtlem70 37205 | Lemma for prter3 37230: a rearrangement of conjuncts. (Contributed by Rodolfo Medina, 20-Oct-2010.) |
⊢ ((((𝜓 ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜑) ↔ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ (𝜃 ∧ 𝜏)))) ∧ 𝜂)) | ||
Theorem | ibdr 37206 | Reverse of ibd 269. (Contributed by Rodolfo Medina, 30-Sep-2010.) |
⊢ (𝜑 → (𝜒 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (𝜒 → 𝜓)) | ||
Theorem | prtlem100 37207 | Lemma for prter3 37230. (Contributed by Rodolfo Medina, 19-Oct-2010.) |
⊢ (∃𝑥 ∈ 𝐴 (𝐵 ∈ 𝑥 ∧ 𝜑) ↔ ∃𝑥 ∈ (𝐴 ∖ {∅})(𝐵 ∈ 𝑥 ∧ 𝜑)) | ||
Theorem | prtlem5 37208* | Lemma for prter1 37227, prter2 37229, prter3 37230 and prtex 37228. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Mario Carneiro, 11-Dec-2016.) |
⊢ ([𝑠 / 𝑣][𝑟 / 𝑢]∃𝑥 ∈ 𝐴 (𝑢 ∈ 𝑥 ∧ 𝑣 ∈ 𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝑟 ∈ 𝑥 ∧ 𝑠 ∈ 𝑥)) | ||
Theorem | prtlem80 37209 | Lemma for prter2 37229. (Contributed by Rodolfo Medina, 17-Oct-2010.) |
⊢ (𝐴 ∈ 𝐵 → ¬ 𝐴 ∈ (𝐶 ∖ {𝐴})) | ||
Theorem | brabsb2 37210* | A closed form of brabsb 5486. (Contributed by Rodolfo Medina, 13-Oct-2010.) |
⊢ (𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑} → (𝑧𝑅𝑤 ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑)) | ||
Theorem | eqbrrdv2 37211* | Other version of eqbrrdiv 5747. (Contributed by Rodolfo Medina, 30-Sep-2010.) |
⊢ (((Rel 𝐴 ∧ Rel 𝐵) ∧ 𝜑) → (𝑥𝐴𝑦 ↔ 𝑥𝐵𝑦)) ⇒ ⊢ (((Rel 𝐴 ∧ Rel 𝐵) ∧ 𝜑) → 𝐴 = 𝐵) | ||
Theorem | prtlem9 37212* | Lemma for prter3 37230. (Contributed by Rodolfo Medina, 25-Sep-2010.) |
⊢ (𝐴 ∈ 𝐵 → ∃𝑥 ∈ 𝐵 [𝑥] ∼ = [𝐴] ∼ ) | ||
Theorem | prtlem10 37213* | Lemma for prter3 37230. (Contributed by Rodolfo Medina, 14-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ ( ∼ Er 𝐴 → (𝑧 ∈ 𝐴 → (𝑧 ∼ 𝑤 ↔ ∃𝑣 ∈ 𝐴 (𝑧 ∈ [𝑣] ∼ ∧ 𝑤 ∈ [𝑣] ∼ )))) | ||
Theorem | prtlem11 37214 | Lemma for prter2 37229. (Contributed by Rodolfo Medina, 12-Oct-2010.) |
⊢ (𝐵 ∈ 𝐷 → (𝐶 ∈ 𝐴 → (𝐵 = [𝐶] ∼ → 𝐵 ∈ (𝐴 / ∼ )))) | ||
Theorem | prtlem12 37215* | Lemma for prtex 37228 and prter3 37230. (Contributed by Rodolfo Medina, 13-Oct-2010.) |
⊢ ( ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} → Rel ∼ ) | ||
Theorem | prtlem13 37216* | Lemma for prter1 37227, prter2 37229, prter3 37230 and prtex 37228. (Contributed by Rodolfo Medina, 13-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ (𝑧 ∼ 𝑤 ↔ ∃𝑣 ∈ 𝐴 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) | ||
Theorem | prtlem16 37217* | Lemma for prtex 37228, prter2 37229 and prter3 37230. (Contributed by Rodolfo Medina, 14-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ dom ∼ = ∪ 𝐴 | ||
Theorem | prtlem400 37218* | Lemma for prter2 37229 and also a property of partitions . (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ ¬ ∅ ∈ (∪ 𝐴 / ∼ ) | ||
Syntax | wprt 37219 | Extend the definition of a wff to include the partition predicate. |
wff Prt 𝐴 | ||
Definition | df-prt 37220* | Define the partition predicate. (Contributed by Rodolfo Medina, 13-Oct-2010.) |
⊢ (Prt 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅)) | ||
Theorem | erprt 37221 | The quotient set of an equivalence relation is a partition. (Contributed by Rodolfo Medina, 13-Oct-2010.) |
⊢ ( ∼ Er 𝑋 → Prt (𝐴 / ∼ )) | ||
Theorem | prtlem14 37222* | Lemma for prter1 37227, prter2 37229 and prtex 37228. (Contributed by Rodolfo Medina, 13-Oct-2010.) |
⊢ (Prt 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑤 ∈ 𝑥 ∧ 𝑤 ∈ 𝑦) → 𝑥 = 𝑦))) | ||
Theorem | prtlem15 37223* | Lemma for prter1 37227 and prtex 37228. (Contributed by Rodolfo Medina, 13-Oct-2010.) |
⊢ (Prt 𝐴 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑢 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) ∧ (𝑤 ∈ 𝑦 ∧ 𝑣 ∈ 𝑦)) → ∃𝑧 ∈ 𝐴 (𝑢 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧))) | ||
Theorem | prtlem17 37224* | Lemma for prter2 37229. (Contributed by Rodolfo Medina, 15-Oct-2010.) |
⊢ (Prt 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥) → (∃𝑦 ∈ 𝐴 (𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦) → 𝑤 ∈ 𝑥))) | ||
Theorem | prtlem18 37225* | Lemma for prter2 37229. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ (Prt 𝐴 → ((𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣) → (𝑤 ∈ 𝑣 ↔ 𝑧 ∼ 𝑤))) | ||
Theorem | prtlem19 37226* | Lemma for prter2 37229. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ (Prt 𝐴 → ((𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣) → 𝑣 = [𝑧] ∼ )) | ||
Theorem | prter1 37227* | Every partition generates an equivalence relation. (Contributed by Rodolfo Medina, 13-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ (Prt 𝐴 → ∼ Er ∪ 𝐴) | ||
Theorem | prtex 37228* | 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 37229* | 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 37230* | 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 2312, axc10 2385, axc11 2430, axc11n 2426, axc15 2422, axc9 2382, axc14 2463, and axc16 2254. | ||
Axiom | ax-c5 37231 |
Axiom of Specialization. A universally quantified wff implies the wff
without the universal quantifier (i.e., an instance, or special case, of
the generalized wff). In other words, if something is true for all
𝑥, then 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 1798. Conditional forms of the converse are given by ax-13 2372, ax-c14 37239, ax-c16 37240, and ax-5 1914. Unlike the more general textbook Axiom of Specialization, we cannot choose a variable different from 𝑥 for the special case. In our axiomatization, that requires the assistance of equality axioms, and we deal with it later after we introduce the definition of proper substitution (see stdpc4 2072). An interesting alternate axiomatization uses axc5c711 37266 and ax-c4 37232 in place of ax-c5 37231, ax-4 1812, ax-10 2138, and ax-11 2155. This axiom is obsolete and should no longer be used. It is proved above as Theorem sp 2177. (Contributed by NM, 3-Jan-1993.) Use sp 2177 instead. (New usage is discouraged.) |
⊢ (∀𝑥𝜑 → 𝜑) | ||
Axiom | ax-c4 37232 |
Axiom of Quantified Implication. This axiom moves a universal 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 2316. (Contributed by NM, 3-Jan-1993.) (New usage is discouraged.) |
⊢ (∀𝑥(∀𝑥𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓)) | ||
Axiom | ax-c7 37233 |
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 37266 in place
of ax-c5 37231, ax-c7 37233, and ax-11 2155.
This axiom is obsolete and should no longer be used. It is proved above as Theorem axc7 2312. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑) | ||
Axiom | ax-c10 37234 |
A variant of ax6 2384. 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 2385. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.) |
⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) → 𝜑) | ||
Axiom | ax-c11 37235 |
Axiom ax-c11 37235 was the original version of ax-c11n 37236 ("n" for "new"),
before it was discovered (in May 2008) that the shorter ax-c11n 37236 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 2430. (Contributed by NM, 10-May-1993.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑)) | ||
Axiom | ax-c11n 37236 |
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 37235 and was replaced with this shorter ax-c11n 37236 ("n" for "new") in May 2008. The old axiom is proved from this one as Theorem axc11 2430. Conversely, this axiom is proved from ax-c11 37235 as Theorem axc11nfromc11 37274. This axiom was proved redundant in July 2015. See Theorem axc11n 2426. This axiom is obsolete and should no longer be used. It is proved above as Theorem axc11n 2426. (Contributed by NM, 16-May-2008.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥) | ||
Axiom | ax-c15 37237 |
Axiom ax-c15 37237 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 37237 (from which the ax-12 2172 instance follows by Theorem ax12 2423.) The proof is by induction on formula length, using ax12eq 37289 and ax12el 37290 for the basis steps and ax12indn 37291, ax12indi 37292, and ax12inda 37296 for the induction steps. (This paragraph is true provided we use ax-c11 37235 in place of ax-c11n 37236.) This axiom is obsolete and should no longer be used. It is proved above as Theorem axc15 2422, which should be used instead. (Contributed by NM, 14-May-1993.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) | ||
Axiom | ax-c9 37238 |
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 2382. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.) |
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))) | ||
Axiom | ax-c14 37239 |
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 1914; see Theorem axc14 2463. Alternately,
ax-5 1914 becomes unnecessary in principle with this
axiom, but we lose the
more powerful metalogic afforded by ax-5 1914.
We retain ax-c14 37239 here to
provide completeness for systems with the simpler metalogic that results
from omitting ax-5 1914, 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 2463. (Contributed by NM, 24-Jun-1993.) (New usage is discouraged.) |
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦))) | ||
Axiom | ax-c16 37240* |
Axiom of Distinct Variables. The only axiom of predicate calculus
requiring that variables be distinct (if we consider ax-5 1914
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 5392), but nonetheless it is technically
necessary as you can see from its uses.
This axiom is redundant if we include ax-5 1914; see Theorem axc16 2254. Alternately, ax-5 1914 becomes logically redundant in the presence of this axiom, but without ax-5 1914 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 37240 here to provide logical completeness for systems with the simpler metalogic that results from omitting ax-5 1914, 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 2254. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑)) | ||
Theorems ax12fromc15 37253 and ax13fromc9 37254 require some intermediate theorems that are included in this section. | ||
Theorem | axc5 37241 | This theorem repeats sp 2177 under the name axc5 37241, so that the Metamath program "MM> VERIFY MARKUP" command will check that it matches axiom scheme ax-c5 37231. (Contributed by NM, 18-Aug-2017.) (Proof modification is discouraged.) Use sp 2177 instead. (New usage is discouraged.) |
⊢ (∀𝑥𝜑 → 𝜑) | ||
Theorem | ax4fromc4 37242 | Rederivation of Axiom ax-4 1812 from ax-c4 37232, ax-c5 37231, ax-gen 1798 and minimal implicational calculus { ax-mp 5, ax-1 6, ax-2 7 }. See axc4 2316 for the derivation of ax-c4 37232 from ax-4 1812. (Contributed by NM, 23-May-2008.) (Proof modification is discouraged.) Use ax-4 1812 instead. (New usage is discouraged.) |
⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓)) | ||
Theorem | ax10fromc7 37243 | Rederivation of Axiom ax-10 2138 from ax-c7 37233, ax-c4 37232, ax-c5 37231, ax-gen 1798 and propositional calculus. See axc7 2312 for the derivation of ax-c7 37233 from ax-10 2138. (Contributed by NM, 23-May-2008.) (Proof modification is discouraged.) Use ax-10 2138 instead. (New usage is discouraged.) |
⊢ (¬ ∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑) | ||
Theorem | ax6fromc10 37244 | Rederivation of Axiom ax-6 1972 from ax-c7 37233, ax-c10 37234, ax-gen 1798 and propositional calculus. See axc10 2385 for the derivation of ax-c10 37234 from ax-6 1972. Lemma L18 in [Megill] p. 446 (p. 14 of the preprint). (Contributed by NM, 14-May-1993.) (Proof modification is discouraged.) Use ax-6 1972 instead. (New usage is discouraged.) |
⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦 | ||
Theorem | hba1-o 37245 | 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 37246 | Inference version of ax-c4 37232. (Contributed by NM, 3-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥𝜑 → 𝜓) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑥𝜓) | ||
Theorem | equid1 37247 | Proof of equid 2016 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 1914; see the proof of equid 2016. See equid1ALT 37273 for an alternate proof. (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝑥 = 𝑥 | ||
Theorem | equcomi1 37248 | Proof of equcomi 2021 from equid1 37247, avoiding use of ax-5 1914 (the only use of ax-5 1914 is via ax7 2020, so using ax-7 2012 instead would remove dependency on ax-5 1914). (Contributed by BJ, 8-Jul-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥) | ||
Theorem | aecom-o 37249 | 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 2427 using ax-c11 37235. Unlike axc11nfromc11 37274, this version does not require ax-5 1914 (see comment of equcomi1 37248). (Contributed by NM, 10-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥) | ||
Theorem | aecoms-o 37250 | A commutation rule for identical variable specifiers. Version of aecoms 2428 using ax-c11 37235. (Contributed by NM, 10-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → 𝜑) ⇒ ⊢ (∀𝑦 𝑦 = 𝑥 → 𝜑) | ||
Theorem | hbae-o 37251 | All variables are effectively bound in an identical variable specifier. Version of hbae 2431 using ax-c11 37235. (Contributed by NM, 13-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦) | ||
Theorem | dral1-o 37252 | 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 2439 using ax-c11 37235. (Contributed by NM, 24-Nov-1994.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 ↔ ∀𝑦𝜓)) | ||
Theorem | ax12fromc15 37253 |
Rederivation of Axiom ax-12 2172 from ax-c15 37237, ax-c11 37235 (used through
dral1-o 37252), and other older axioms. See Theorem axc15 2422 for the
derivation of ax-c15 37237 from ax-12 2172.
An open problem is whether we can prove this using ax-c11n 37236 instead of ax-c11 37235. This proof uses newer axioms ax-4 1812 and ax-6 1972, 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 37232 and ax-c10 37234. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | ax13fromc9 37254 |
Derive ax-13 2372 from ax-c9 37238 and other older axioms.
This proof uses newer axioms ax-4 1812 and ax-6 1972, 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 37232 and ax-c10 37234. (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 37255* |
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 1914 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 1798, ax-c4 37232, ax-c5 37231, ax-11 2155, ax-c7 37233, ax-7 2012, ax-c9 37238, ax-c10 37234, ax-c11 37235, ax-8 2109, ax-9 2117, ax-c14 37239, ax-c15 37237, and ax-c16 37240: in that system, we can derive any instance of ax-5 1914 not containing wff variables by induction on formula length, using ax5eq 37280 and ax5el 37285 for the basis together with hbn 2293, hbal 2168, and hbim 2297. 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 37256 | Generalization of antecedent. (Contributed by NM, 5-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
Theorem | hbequid 37257 | 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 37234.) (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 37258 | 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 1812, ax-7 2012, ax-c9 37238, and ax-gen 1798. This shows that this can be proved without ax6 2384, even though Theorem equid 2016 cannot. A shorter proof using ax6 2384 is obtainable from equid 2016 and hbth 1806.) Remark added 2-Dec-2015 NM: This proof does implicitly use ax6v 1973, which is used for the derivation of axc9 2382, unless we consider ax-c9 37238 the starting axiom rather than ax-13 2372. (Contributed by NM, 13-Jan-2011.) (Revised by Mario Carneiro, 12-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑦 𝑥 = 𝑥 | ||
Theorem | axc5c7 37259 | Proof of a single axiom that can replace ax-c5 37231 and ax-c7 37233. See axc5c7toc5 37260 and axc5c7toc7 37261 for the rederivation of those axioms. (Contributed by Scott Fenton, 12-Sep-2005.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((∀𝑥 ¬ ∀𝑥𝜑 → ∀𝑥𝜑) → 𝜑) | ||
Theorem | axc5c7toc5 37260 | Rederivation of ax-c5 37231 from axc5c7 37259. 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 37261 | Rederivation of ax-c7 37233 from axc5c7 37259. 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 37262 | Proof of a single axiom that can replace both ax-c7 37233 and ax-11 2155. See axc711toc7 37264 and axc711to11 37265 for the rederivation of those axioms. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 ¬ ∀𝑦∀𝑥𝜑 → ∀𝑦𝜑) | ||
Theorem | nfa1-o 37263 | 𝑥 is not free in ∀𝑥𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥∀𝑥𝜑 | ||
Theorem | axc711toc7 37264 | Rederivation of ax-c7 37233 from axc711 37262. Note that ax-c7 37233 and ax-11 2155 are not used by the rederivation. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑) | ||
Theorem | axc711to11 37265 | Rederivation of ax-11 2155 from axc711 37262. Note that ax-c7 37233 and ax-11 2155 are not used by the rederivation. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) | ||
Theorem | axc5c711 37266 | Proof of a single axiom that can replace ax-c5 37231, ax-c7 37233, and ax-11 2155 in a subsystem that includes these axioms plus ax-c4 37232 and ax-gen 1798 (and propositional calculus). See axc5c711toc5 37267, axc5c711toc7 37268, and axc5c711to11 37269 for the rederivation of those axioms. This theorem extends the idea in Scott Fenton's axc5c7 37259. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑 → ∀𝑥𝜑) → 𝜑) | ||
Theorem | axc5c711toc5 37267 | Rederivation of ax-c5 37231 from axc5c711 37266. Only propositional calculus is used by the rederivation. (Contributed by NM, 19-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥𝜑 → 𝜑) | ||
Theorem | axc5c711toc7 37268 | Rederivation of ax-c7 37233 from axc5c711 37266. Note that ax-c7 37233 and ax-11 2155 are not used by the rederivation. The use of alimi 1814 (which uses ax-c5 37231) is allowed since we have already proved axc5c711toc5 37267. (Contributed by NM, 19-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑) | ||
Theorem | axc5c711to11 37269 | Rederivation of ax-11 2155 from axc5c711 37266. Note that ax-c7 37233 and ax-11 2155 are not used by the rederivation. The use of alimi 1814 (which uses ax-c5 37231) is allowed since we have already proved axc5c711toc5 37267. (Contributed by NM, 19-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) | ||
Theorem | equidqe 37270 | equid 2016 with existential quantifier without using ax-c5 37231 or ax-5 1914. (Contributed by NM, 13-Jan-2011.) (Proof shortened by Wolf Lammen, 27-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ¬ ∀𝑦 ¬ 𝑥 = 𝑥 | ||
Theorem | axc5sp1 37271 | A special case of ax-c5 37231 without using ax-c5 37231 or ax-5 1914. (Contributed by NM, 13-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑦 ¬ 𝑥 = 𝑥 → ¬ 𝑥 = 𝑥) | ||
Theorem | equidq 37272 | equid 2016 with universal quantifier without using ax-c5 37231 or ax-5 1914. (Contributed by NM, 13-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ∀𝑦 𝑥 = 𝑥 | ||
Theorem | equid1ALT 37273 | Alternate proof of equid 2016 and equid1 37247 from older axioms ax-c7 37233, ax-c10 37234 and ax-c9 37238. (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝑥 = 𝑥 | ||
Theorem | axc11nfromc11 37274 |
Rederivation of ax-c11n 37236 from original version ax-c11 37235. See Theorem
axc11 2430 for the derivation of ax-c11 37235 from ax-c11n 37236.
This theorem should not be referenced in any proof. Instead, use ax-c11n 37236 above so that uses of ax-c11n 37236 can be more easily identified, or use aecom-o 37249 when this form is needed for studies involving ax-c11 37235 and omitting ax-5 1914. (Contributed by NM, 16-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥) | ||
Theorem | naecoms-o 37275 | A commutation rule for distinct variable specifiers. Version of naecoms 2429 using ax-c11 37235. (Contributed by NM, 2-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → 𝜑) ⇒ ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → 𝜑) | ||
Theorem | hbnae-o 37276 | All variables are effectively bound in a distinct variable specifier. Lemma L19 in [Megill] p. 446 (p. 14 of the preprint). Version of hbnae 2432 using ax-c11 37235. (Contributed by NM, 13-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦) | ||
Theorem | dvelimf-o 37277 | Proof of dvelimh 2450 that uses ax-c11 37235 but not ax-c15 37237, ax-c11n 37236, or ax-12 2172. Version of dvelimh 2450 using ax-c11 37235 instead of axc11 2430. (Contributed by NM, 12-Nov-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜓 → ∀𝑧𝜓) & ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓)) | ||
Theorem | dral2-o 37278 | 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 2438 using ax-c11 37235. (Contributed by NM, 27-Feb-2005.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑧𝜑 ↔ ∀𝑧𝜓)) | ||
Theorem | aev-o 37279* | A "distinctor elimination" lemma with no disjoint variable conditions on variables in the consequent, proved without using ax-c16 37240. Version of aev 2061 using ax-c11 37235. (Contributed by NM, 8-Nov-2006.) (Proof shortened by Andrew Salmon, 21-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑤 = 𝑣) | ||
Theorem | ax5eq 37280* | Theorem to add distinct quantifier to atomic formula. (This theorem demonstrates the induction basis for ax-5 1914 considered as a metatheorem. Do not use it for later proofs - use ax-5 1914 instead, to avoid reference to the redundant axiom ax-c16 37240.) (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦) | ||
Theorem | dveeq2-o 37281* | Quantifier introduction when one pair of variables is distinct. Version of dveeq2 2378 using ax-c15 37237. (Contributed by NM, 2-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) | ||
Theorem | axc16g-o 37282* | A generalization of Axiom ax-c16 37240. Version of axc16g 2253 using ax-c11 37235. (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 37283* | Quantifier introduction when one pair of variables is distinct. Version of dveeq1 2380 using ax-c11 . (Contributed by NM, 2-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) | ||
Theorem | dveeq1-o16 37284* | Version of dveeq1 2380 using ax-c16 37240 instead of ax-5 1914. (Contributed by NM, 29-Apr-2008.) TODO: Recover proof from older set.mm to remove use of ax-5 1914. (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) | ||
Theorem | ax5el 37285* | Theorem to add distinct quantifier to atomic formula. This theorem demonstrates the induction basis for ax-5 1914 considered as a metatheorem.) (Contributed by NM, 22-Jun-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦) | ||
Theorem | axc11n-16 37286* | This theorem shows that, given ax-c16 37240, we can derive a version of ax-c11n 37236. However, it is weaker than ax-c11n 37236 because it has a distinct variable requirement. (Contributed by Andrew Salmon, 27-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑧 → ∀𝑧 𝑧 = 𝑥) | ||
Theorem | dveel2ALT 37287* | Alternate proof of dveel2 2462 using ax-c16 37240 instead of ax-5 1914. (Contributed by NM, 10-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 ∈ 𝑦 → ∀𝑥 𝑧 ∈ 𝑦)) | ||
Theorem | ax12f 37288 | Basis step for constructing a substitution instance of ax-c15 37237 without using ax-c15 37237. 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 37289 | Basis step for constructing a substitution instance of ax-c15 37237 without using ax-c15 37237. Atomic formula for equality predicate. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))) | ||
Theorem | ax12el 37290 | Basis step for constructing a substitution instance of ax-c15 37237 without using ax-c15 37237. Atomic formula for membership predicate. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))) | ||
Theorem | ax12indn 37291 | Induction step for constructing a substitution instance of ax-c15 37237 without using ax-c15 37237. Negation case. (Contributed by NM, 21-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (¬ 𝜑 → ∀𝑥(𝑥 = 𝑦 → ¬ 𝜑)))) | ||
Theorem | ax12indi 37292 | Induction step for constructing a substitution instance of ax-c15 37237 without using ax-c15 37237. Implication case. (Contributed by NM, 21-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) & ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜓 → ∀𝑥(𝑥 = 𝑦 → 𝜓)))) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → ((𝜑 → 𝜓) → ∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓))))) | ||
Theorem | ax12indalem 37293 | Lemma for ax12inda2 37295 and ax12inda 37296. (Contributed by NM, 24-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) ⇒ ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))))) | ||
Theorem | ax12inda2ALT 37294* | Alternate proof of ax12inda2 37295, slightly more direct and not requiring ax-c16 37240. (Contributed by NM, 4-May-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))) | ||
Theorem | ax12inda2 37295* | Induction step for constructing a substitution instance of ax-c15 37237 without using ax-c15 37237. Quantification case. When 𝑧 and 𝑦 are distinct, this theorem avoids the dummy variables needed by the more general ax12inda 37296. (Contributed by NM, 24-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))) | ||
Theorem | ax12inda 37296* | Induction step for constructing a substitution instance of ax-c15 37237 without using ax-c15 37237. Quantification case. (When 𝑧 and 𝑦 are distinct, ax12inda2 37295 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 37297* | Rederivation of ax-c15 37237 from ax12v 2173 (without using ax-c15 37237 or the full ax-12 2172). Thus, the hypothesis (ax12v 2173) provides an alternate axiom that can be used in place of ax-c15 37237. See also axc15 2422. (Contributed by NM, 2-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑧 → (𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑))) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) | ||
Theorem | ax12a2-o 37298* | Derive ax-c15 37237 from a hypothesis in the form of ax-12 2172, without using ax-12 2172 or ax-c15 37237. 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 37235, which this proof uses. As Theorem ax12 2423 shows, the distinct variable conditions are optional. An open problem is whether we can derive this with ax-c11n 37236 instead of ax-c11 37235. (Contributed by NM, 2-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑧 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑))) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) | ||
Theorem | axc11-o 37299 |
Show that ax-c11 37235 can be derived from ax-c11n 37236 and ax-12 2172. An open
problem is whether this theorem can be derived from ax-c11n 37236 and the
others when ax-12 2172 is replaced with ax-c15 37237 or ax12v 2173. See Theorems
axc11nfromc11 37274 for the rederivation of ax-c11n 37236 from axc11 2430.
Normally, axc11 2430 should be used rather than ax-c11 37235 or axc11-o 37299, 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 37300* | Index shift of a finite sum with a weaker "implicit substitution" hypothesis than fsumshft 15600. The proof demonstrates how this can be derived starting from from fsumshft 15600. (Contributed by NM, 1-Nov-2019.) |
⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑗 = (𝑘 − 𝐾)) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ (𝑀...𝑁)𝐴 = Σ𝑘 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))𝐵) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |