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-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fences 37201 | The Theorem of Fences by Equivalences: all conceivable equivalence relations (besides the comember equivalence relation cf. mpet 37196) generate a partition of the members. (Contributed by Peter Mazsa, 26-Sep-2021.) |
⊢ (𝑅 ErALTV 𝐴 → MembPart 𝐴) | ||
Theorem | fences2 37202 | The Theorem of Fences by Equivalences: all conceivable equivalence relations (besides the comember equivalence relation cf. mpet3 37193) generate a partition of the members, it alo means that (𝑅 ErALTV 𝐴 → ElDisj 𝐴) and that (𝑅 ErALTV 𝐴 → ¬ ∅ ∈ 𝐴). (Contributed by Peter Mazsa, 15-Oct-2021.) |
⊢ (𝑅 ErALTV 𝐴 → ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴)) | ||
Theorem | mainer2 37203 | The Main Theorem of Equivalences: every equivalence relation implies equivalent comembers. (Contributed by Peter Mazsa, 15-Oct-2021.) |
⊢ (𝑅 ErALTV 𝐴 → ( CoElEqvRel 𝐴 ∧ ¬ ∅ ∈ 𝐴)) | ||
Theorem | mainerim 37204 | Every equivalence relation implies equivalent coelements. (Contributed by Peter Mazsa, 20-Oct-2021.) |
⊢ (𝑅 ErALTV 𝐴 → CoElEqvRel 𝐴) | ||
Theorem | petincnvepres2 37205 | A partition-equivalence theorem with intersection and general 𝑅. (Contributed by Peter Mazsa, 31-Dec-2021.) |
⊢ (( Disj (𝑅 ∩ (◡ E ↾ 𝐴)) ∧ (dom (𝑅 ∩ (◡ E ↾ 𝐴)) / (𝑅 ∩ (◡ E ↾ 𝐴))) = 𝐴) ↔ ( EqvRel ≀ (𝑅 ∩ (◡ E ↾ 𝐴)) ∧ (dom ≀ (𝑅 ∩ (◡ E ↾ 𝐴)) / ≀ (𝑅 ∩ (◡ E ↾ 𝐴))) = 𝐴)) | ||
Theorem | petincnvepres 37206 | The shortest form of a partition-equivalence theorem with intersection and general 𝑅. Cf. br1cossincnvepres 36807. Cf. pet 37208. (Contributed by Peter Mazsa, 23-Sep-2021.) |
⊢ ((𝑅 ∩ (◡ E ↾ 𝐴)) Part 𝐴 ↔ ≀ (𝑅 ∩ (◡ E ↾ 𝐴)) ErALTV 𝐴) | ||
Theorem | pet2 37207 | Partition-Equivalence Theorem, with general 𝑅. This theorem (together with pet 37208 and pets 37209) is the main result of my investigation into set theory, see the comment of pet 37208. (Contributed by Peter Mazsa, 24-May-2021.) (Revised by Peter Mazsa, 23-Sep-2021.) |
⊢ (( Disj (𝑅 ⋉ (◡ E ↾ 𝐴)) ∧ (dom (𝑅 ⋉ (◡ E ↾ 𝐴)) / (𝑅 ⋉ (◡ E ↾ 𝐴))) = 𝐴) ↔ ( EqvRel ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) ∧ (dom ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) / ≀ (𝑅 ⋉ (◡ E ↾ 𝐴))) = 𝐴)) | ||
Theorem | pet 37208 |
Partition-Equivalence Theorem with general 𝑅 while preserving the
restricted converse epsilon relation of mpet2 37197 (as opposed to
petincnvepres 37206). A class is a partition by a range
Cartesian product
with general 𝑅 and the restricted converse element
class if and only
if the cosets by the range Cartesian product are in an equivalence
relation on it. Cf. br1cossxrncnvepres 36809.
This theorem (together with pets 37209 and pet2 37207) is the main result of my investigation into set theory. It is no more general than the conventional Member Partition-Equivalence Theorem mpet 37196, mpet2 37197 and mpet3 37193 (because you cannot set 𝑅 in this theorem in such a way that you get mpet2 37197), i.e., it is not the hypothetical General Partition-Equivalence Theorem gpet ⊢ (𝑅 Part 𝐴 ↔ ≀ 𝑅 ErALTV 𝐴), but this one has a general part that mpet2 37197 lacks: 𝑅, which is sufficient for my future application of set theory, for my purpose outside of set theory. (Contributed by Peter Mazsa, 23-Sep-2021.) |
⊢ ((𝑅 ⋉ (◡ E ↾ 𝐴)) Part 𝐴 ↔ ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) ErALTV 𝐴) | ||
Theorem | pets 37209 | Partition-Equivalence Theorem with general 𝑅, with binary relations. This theorem (together with pet 37208 and pet2 37207) is the main result of my investigation into set theory, cf. the comment of pet 37208. (Contributed by Peter Mazsa, 23-Sep-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → ((𝑅 ⋉ (◡ E ↾ 𝐴)) Parts 𝐴 ↔ ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) Ers 𝐴)) | ||
Theorem | prtlem60 37210 | Lemma for prter3 37239. (Contributed by Rodolfo Medina, 9-Oct-2010.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜓 → (𝜃 → 𝜏)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏))) | ||
Theorem | bicomdd 37211 | 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 37212 | Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 17-Oct-2010.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜓 → 𝜃) ⇒ ⊢ (𝜑 → (𝜓 → (𝜃 ∧ 𝜒))) | ||
Theorem | jca3 37213 | Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 14-Oct-2010.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜃 → 𝜏) ⇒ ⊢ (𝜑 → (𝜓 → (𝜃 → (𝜒 ∧ 𝜏)))) | ||
Theorem | prtlem70 37214 | Lemma for prter3 37239: a rearrangement of conjuncts. (Contributed by Rodolfo Medina, 20-Oct-2010.) |
⊢ ((((𝜓 ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜑) ↔ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ (𝜃 ∧ 𝜏)))) ∧ 𝜂)) | ||
Theorem | ibdr 37215 | Reverse of ibd 268. (Contributed by Rodolfo Medina, 30-Sep-2010.) |
⊢ (𝜑 → (𝜒 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (𝜒 → 𝜓)) | ||
Theorem | prtlem100 37216 | Lemma for prter3 37239. (Contributed by Rodolfo Medina, 19-Oct-2010.) |
⊢ (∃𝑥 ∈ 𝐴 (𝐵 ∈ 𝑥 ∧ 𝜑) ↔ ∃𝑥 ∈ (𝐴 ∖ {∅})(𝐵 ∈ 𝑥 ∧ 𝜑)) | ||
Theorem | prtlem5 37217* | Lemma for prter1 37236, prter2 37238, prter3 37239 and prtex 37237. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Mario Carneiro, 11-Dec-2016.) |
⊢ ([𝑠 / 𝑣][𝑟 / 𝑢]∃𝑥 ∈ 𝐴 (𝑢 ∈ 𝑥 ∧ 𝑣 ∈ 𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝑟 ∈ 𝑥 ∧ 𝑠 ∈ 𝑥)) | ||
Theorem | prtlem80 37218 | Lemma for prter2 37238. (Contributed by Rodolfo Medina, 17-Oct-2010.) |
⊢ (𝐴 ∈ 𝐵 → ¬ 𝐴 ∈ (𝐶 ∖ {𝐴})) | ||
Theorem | brabsb2 37219* | A closed form of brabsb 5485. (Contributed by Rodolfo Medina, 13-Oct-2010.) |
⊢ (𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑} → (𝑧𝑅𝑤 ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑)) | ||
Theorem | eqbrrdv2 37220* | Other version of eqbrrdiv 5746. (Contributed by Rodolfo Medina, 30-Sep-2010.) |
⊢ (((Rel 𝐴 ∧ Rel 𝐵) ∧ 𝜑) → (𝑥𝐴𝑦 ↔ 𝑥𝐵𝑦)) ⇒ ⊢ (((Rel 𝐴 ∧ Rel 𝐵) ∧ 𝜑) → 𝐴 = 𝐵) | ||
Theorem | prtlem9 37221* | Lemma for prter3 37239. (Contributed by Rodolfo Medina, 25-Sep-2010.) |
⊢ (𝐴 ∈ 𝐵 → ∃𝑥 ∈ 𝐵 [𝑥] ∼ = [𝐴] ∼ ) | ||
Theorem | prtlem10 37222* | Lemma for prter3 37239. (Contributed by Rodolfo Medina, 14-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ ( ∼ Er 𝐴 → (𝑧 ∈ 𝐴 → (𝑧 ∼ 𝑤 ↔ ∃𝑣 ∈ 𝐴 (𝑧 ∈ [𝑣] ∼ ∧ 𝑤 ∈ [𝑣] ∼ )))) | ||
Theorem | prtlem11 37223 | Lemma for prter2 37238. (Contributed by Rodolfo Medina, 12-Oct-2010.) |
⊢ (𝐵 ∈ 𝐷 → (𝐶 ∈ 𝐴 → (𝐵 = [𝐶] ∼ → 𝐵 ∈ (𝐴 / ∼ )))) | ||
Theorem | prtlem12 37224* | Lemma for prtex 37237 and prter3 37239. (Contributed by Rodolfo Medina, 13-Oct-2010.) |
⊢ ( ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} → Rel ∼ ) | ||
Theorem | prtlem13 37225* | Lemma for prter1 37236, prter2 37238, prter3 37239 and prtex 37237. (Contributed by Rodolfo Medina, 13-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ (𝑧 ∼ 𝑤 ↔ ∃𝑣 ∈ 𝐴 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) | ||
Theorem | prtlem16 37226* | Lemma for prtex 37237, prter2 37238 and prter3 37239. (Contributed by Rodolfo Medina, 14-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ dom ∼ = ∪ 𝐴 | ||
Theorem | prtlem400 37227* | Lemma for prter2 37238 and also a property of partitions . (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ ¬ ∅ ∈ (∪ 𝐴 / ∼ ) | ||
Syntax | wprt 37228 | Extend the definition of a wff to include the partition predicate. |
wff Prt 𝐴 | ||
Definition | df-prt 37229* | Define the partition predicate. (Contributed by Rodolfo Medina, 13-Oct-2010.) |
⊢ (Prt 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅)) | ||
Theorem | erprt 37230 | The quotient set of an equivalence relation is a partition. (Contributed by Rodolfo Medina, 13-Oct-2010.) |
⊢ ( ∼ Er 𝑋 → Prt (𝐴 / ∼ )) | ||
Theorem | prtlem14 37231* | Lemma for prter1 37236, prter2 37238 and prtex 37237. (Contributed by Rodolfo Medina, 13-Oct-2010.) |
⊢ (Prt 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑤 ∈ 𝑥 ∧ 𝑤 ∈ 𝑦) → 𝑥 = 𝑦))) | ||
Theorem | prtlem15 37232* | Lemma for prter1 37236 and prtex 37237. (Contributed by Rodolfo Medina, 13-Oct-2010.) |
⊢ (Prt 𝐴 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑢 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) ∧ (𝑤 ∈ 𝑦 ∧ 𝑣 ∈ 𝑦)) → ∃𝑧 ∈ 𝐴 (𝑢 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧))) | ||
Theorem | prtlem17 37233* | Lemma for prter2 37238. (Contributed by Rodolfo Medina, 15-Oct-2010.) |
⊢ (Prt 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥) → (∃𝑦 ∈ 𝐴 (𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦) → 𝑤 ∈ 𝑥))) | ||
Theorem | prtlem18 37234* | Lemma for prter2 37238. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ (Prt 𝐴 → ((𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣) → (𝑤 ∈ 𝑣 ↔ 𝑧 ∼ 𝑤))) | ||
Theorem | prtlem19 37235* | Lemma for prter2 37238. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ (Prt 𝐴 → ((𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣) → 𝑣 = [𝑧] ∼ )) | ||
Theorem | prter1 37236* | Every partition generates an equivalence relation. (Contributed by Rodolfo Medina, 13-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ (Prt 𝐴 → ∼ Er ∪ 𝐴) | ||
Theorem | prtex 37237* | 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 37238* | 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 37239* | 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 2176, axc7 2311, axc10 2384, axc11 2429, axc11n 2425, axc15 2421, axc9 2381, axc14 2462, and axc16 2253. | ||
Axiom | ax-c5 37240 |
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 1797. Conditional forms of the converse are given by ax-13 2371, ax-c14 37248, ax-c16 37249, and ax-5 1913. 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 2071). An interesting alternate axiomatization uses axc5c711 37275 and ax-c4 37241 in place of ax-c5 37240, ax-4 1811, ax-10 2137, and ax-11 2154. This axiom is obsolete and should no longer be used. It is proved above as Theorem sp 2176. (Contributed by NM, 3-Jan-1993.) Use sp 2176 instead. (New usage is discouraged.) |
⊢ (∀𝑥𝜑 → 𝜑) | ||
Axiom | ax-c4 37241 |
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 2315. (Contributed by NM, 3-Jan-1993.) (New usage is discouraged.) |
⊢ (∀𝑥(∀𝑥𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓)) | ||
Axiom | ax-c7 37242 |
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 37275 in place
of ax-c5 37240, ax-c7 37242, and ax-11 2154.
This axiom is obsolete and should no longer be used. It is proved above as Theorem axc7 2311. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑) | ||
Axiom | ax-c10 37243 |
A variant of ax6 2383. 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 2384. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.) |
⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) → 𝜑) | ||
Axiom | ax-c11 37244 |
Axiom ax-c11 37244 was the original version of ax-c11n 37245 ("n" for "new"),
before it was discovered (in May 2008) that the shorter ax-c11n 37245 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 2429. (Contributed by NM, 10-May-1993.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑)) | ||
Axiom | ax-c11n 37245 |
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 37244 and was replaced with this shorter ax-c11n 37245 ("n" for "new") in May 2008. The old axiom is proved from this one as Theorem axc11 2429. Conversely, this axiom is proved from ax-c11 37244 as Theorem axc11nfromc11 37283. This axiom was proved redundant in July 2015. See Theorem axc11n 2425. This axiom is obsolete and should no longer be used. It is proved above as Theorem axc11n 2425. (Contributed by NM, 16-May-2008.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥) | ||
Axiom | ax-c15 37246 |
Axiom ax-c15 37246 was the original version of ax-12 2171, before it was
discovered (in Jan. 2007) that the shorter ax-12 2171 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 37246 (from which the ax-12 2171 instance follows by Theorem ax12 2422.) The proof is by induction on formula length, using ax12eq 37298 and ax12el 37299 for the basis steps and ax12indn 37300, ax12indi 37301, and ax12inda 37305 for the induction steps. (This paragraph is true provided we use ax-c11 37244 in place of ax-c11n 37245.) This axiom is obsolete and should no longer be used. It is proved above as Theorem axc15 2421, which should be used instead. (Contributed by NM, 14-May-1993.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) | ||
Axiom | ax-c9 37247 |
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 2381. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.) |
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))) | ||
Axiom | ax-c14 37248 |
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 1913; see Theorem axc14 2462. Alternately,
ax-5 1913 becomes unnecessary in principle with this
axiom, but we lose the
more powerful metalogic afforded by ax-5 1913.
We retain ax-c14 37248 here to
provide completeness for systems with the simpler metalogic that results
from omitting ax-5 1913, 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 2462. (Contributed by NM, 24-Jun-1993.) (New usage is discouraged.) |
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦))) | ||
Axiom | ax-c16 37249* |
Axiom of Distinct Variables. The only axiom of predicate calculus
requiring that variables be distinct (if we consider ax-5 1913
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 5391), but nonetheless it is technically
necessary as you can see from its uses.
This axiom is redundant if we include ax-5 1913; see Theorem axc16 2253. Alternately, ax-5 1913 becomes logically redundant in the presence of this axiom, but without ax-5 1913 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 37249 here to provide logical completeness for systems with the simpler metalogic that results from omitting ax-5 1913, 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 2253. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑)) | ||
Theorems ax12fromc15 37262 and ax13fromc9 37263 require some intermediate theorems that are included in this section. | ||
Theorem | axc5 37250 | This theorem repeats sp 2176 under the name axc5 37250, so that the Metamath program "MM> VERIFY MARKUP" command will check that it matches axiom scheme ax-c5 37240. (Contributed by NM, 18-Aug-2017.) (Proof modification is discouraged.) Use sp 2176 instead. (New usage is discouraged.) |
⊢ (∀𝑥𝜑 → 𝜑) | ||
Theorem | ax4fromc4 37251 | Rederivation of Axiom ax-4 1811 from ax-c4 37241, ax-c5 37240, ax-gen 1797 and minimal implicational calculus { ax-mp 5, ax-1 6, ax-2 7 }. See axc4 2315 for the derivation of ax-c4 37241 from ax-4 1811. (Contributed by NM, 23-May-2008.) (Proof modification is discouraged.) Use ax-4 1811 instead. (New usage is discouraged.) |
⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓)) | ||
Theorem | ax10fromc7 37252 | Rederivation of Axiom ax-10 2137 from ax-c7 37242, ax-c4 37241, ax-c5 37240, ax-gen 1797 and propositional calculus. See axc7 2311 for the derivation of ax-c7 37242 from ax-10 2137. (Contributed by NM, 23-May-2008.) (Proof modification is discouraged.) Use ax-10 2137 instead. (New usage is discouraged.) |
⊢ (¬ ∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑) | ||
Theorem | ax6fromc10 37253 | Rederivation of Axiom ax-6 1971 from ax-c7 37242, ax-c10 37243, ax-gen 1797 and propositional calculus. See axc10 2384 for the derivation of ax-c10 37243 from ax-6 1971. Lemma L18 in [Megill] p. 446 (p. 14 of the preprint). (Contributed by NM, 14-May-1993.) (Proof modification is discouraged.) Use ax-6 1971 instead. (New usage is discouraged.) |
⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦 | ||
Theorem | hba1-o 37254 | 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 37255 | Inference version of ax-c4 37241. (Contributed by NM, 3-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥𝜑 → 𝜓) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑥𝜓) | ||
Theorem | equid1 37256 | 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 1913; see the proof of equid 2015. See equid1ALT 37282 for an alternate proof. (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝑥 = 𝑥 | ||
Theorem | equcomi1 37257 | Proof of equcomi 2020 from equid1 37256, avoiding use of ax-5 1913 (the only use of ax-5 1913 is via ax7 2019, so using ax-7 2011 instead would remove dependency on ax-5 1913). (Contributed by BJ, 8-Jul-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥) | ||
Theorem | aecom-o 37258 | 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 2426 using ax-c11 37244. Unlike axc11nfromc11 37283, this version does not require ax-5 1913 (see comment of equcomi1 37257). (Contributed by NM, 10-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥) | ||
Theorem | aecoms-o 37259 | A commutation rule for identical variable specifiers. Version of aecoms 2427 using ax-c11 37244. (Contributed by NM, 10-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → 𝜑) ⇒ ⊢ (∀𝑦 𝑦 = 𝑥 → 𝜑) | ||
Theorem | hbae-o 37260 | All variables are effectively bound in an identical variable specifier. Version of hbae 2430 using ax-c11 37244. (Contributed by NM, 13-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦) | ||
Theorem | dral1-o 37261 | 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 2438 using ax-c11 37244. (Contributed by NM, 24-Nov-1994.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 ↔ ∀𝑦𝜓)) | ||
Theorem | ax12fromc15 37262 |
Rederivation of Axiom ax-12 2171 from ax-c15 37246, ax-c11 37244 (used through
dral1-o 37261), and other older axioms. See Theorem axc15 2421 for the
derivation of ax-c15 37246 from ax-12 2171.
An open problem is whether we can prove this using ax-c11n 37245 instead of ax-c11 37244. This proof uses newer axioms ax-4 1811 and ax-6 1971, 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 37241 and ax-c10 37243. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | ax13fromc9 37263 |
Derive ax-13 2371 from ax-c9 37247 and other older axioms.
This proof uses newer axioms ax-4 1811 and ax-6 1971, 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 37241 and ax-c10 37243. (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 37264* |
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 1913 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 1797, ax-c4 37241, ax-c5 37240, ax-11 2154, ax-c7 37242, ax-7 2011, ax-c9 37247, ax-c10 37243, ax-c11 37244, ax-8 2108, ax-9 2116, ax-c14 37248, ax-c15 37246, and ax-c16 37249: in that system, we can derive any instance of ax-5 1913 not containing wff variables by induction on formula length, using ax5eq 37289 and ax5el 37294 for the basis together with hbn 2292, hbal 2167, and hbim 2296. 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 37265 | Generalization of antecedent. (Contributed by NM, 5-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
Theorem | hbequid 37266 | 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 37243.) (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 37267 | 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 1811, ax-7 2011, ax-c9 37247, and ax-gen 1797. This shows that this can be proved without ax6 2383, even though Theorem equid 2015 cannot. A shorter proof using ax6 2383 is obtainable from equid 2015 and hbth 1805.) Remark added 2-Dec-2015 NM: This proof does implicitly use ax6v 1972, which is used for the derivation of axc9 2381, unless we consider ax-c9 37247 the starting axiom rather than ax-13 2371. (Contributed by NM, 13-Jan-2011.) (Revised by Mario Carneiro, 12-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑦 𝑥 = 𝑥 | ||
Theorem | axc5c7 37268 | Proof of a single axiom that can replace ax-c5 37240 and ax-c7 37242. See axc5c7toc5 37269 and axc5c7toc7 37270 for the rederivation of those axioms. (Contributed by Scott Fenton, 12-Sep-2005.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((∀𝑥 ¬ ∀𝑥𝜑 → ∀𝑥𝜑) → 𝜑) | ||
Theorem | axc5c7toc5 37269 | Rederivation of ax-c5 37240 from axc5c7 37268. 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 37270 | Rederivation of ax-c7 37242 from axc5c7 37268. 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 37271 | Proof of a single axiom that can replace both ax-c7 37242 and ax-11 2154. See axc711toc7 37273 and axc711to11 37274 for the rederivation of those axioms. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 ¬ ∀𝑦∀𝑥𝜑 → ∀𝑦𝜑) | ||
Theorem | nfa1-o 37272 | 𝑥 is not free in ∀𝑥𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥∀𝑥𝜑 | ||
Theorem | axc711toc7 37273 | Rederivation of ax-c7 37242 from axc711 37271. Note that ax-c7 37242 and ax-11 2154 are not used by the rederivation. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑) | ||
Theorem | axc711to11 37274 | Rederivation of ax-11 2154 from axc711 37271. Note that ax-c7 37242 and ax-11 2154 are not used by the rederivation. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) | ||
Theorem | axc5c711 37275 | Proof of a single axiom that can replace ax-c5 37240, ax-c7 37242, and ax-11 2154 in a subsystem that includes these axioms plus ax-c4 37241 and ax-gen 1797 (and propositional calculus). See axc5c711toc5 37276, axc5c711toc7 37277, and axc5c711to11 37278 for the rederivation of those axioms. This theorem extends the idea in Scott Fenton's axc5c7 37268. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑 → ∀𝑥𝜑) → 𝜑) | ||
Theorem | axc5c711toc5 37276 | Rederivation of ax-c5 37240 from axc5c711 37275. Only propositional calculus is used by the rederivation. (Contributed by NM, 19-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥𝜑 → 𝜑) | ||
Theorem | axc5c711toc7 37277 | Rederivation of ax-c7 37242 from axc5c711 37275. Note that ax-c7 37242 and ax-11 2154 are not used by the rederivation. The use of alimi 1813 (which uses ax-c5 37240) is allowed since we have already proved axc5c711toc5 37276. (Contributed by NM, 19-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑) | ||
Theorem | axc5c711to11 37278 | Rederivation of ax-11 2154 from axc5c711 37275. Note that ax-c7 37242 and ax-11 2154 are not used by the rederivation. The use of alimi 1813 (which uses ax-c5 37240) is allowed since we have already proved axc5c711toc5 37276. (Contributed by NM, 19-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) | ||
Theorem | equidqe 37279 | equid 2015 with existential quantifier without using ax-c5 37240 or ax-5 1913. (Contributed by NM, 13-Jan-2011.) (Proof shortened by Wolf Lammen, 27-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ¬ ∀𝑦 ¬ 𝑥 = 𝑥 | ||
Theorem | axc5sp1 37280 | A special case of ax-c5 37240 without using ax-c5 37240 or ax-5 1913. (Contributed by NM, 13-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑦 ¬ 𝑥 = 𝑥 → ¬ 𝑥 = 𝑥) | ||
Theorem | equidq 37281 | equid 2015 with universal quantifier without using ax-c5 37240 or ax-5 1913. (Contributed by NM, 13-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ∀𝑦 𝑥 = 𝑥 | ||
Theorem | equid1ALT 37282 | Alternate proof of equid 2015 and equid1 37256 from older axioms ax-c7 37242, ax-c10 37243 and ax-c9 37247. (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝑥 = 𝑥 | ||
Theorem | axc11nfromc11 37283 |
Rederivation of ax-c11n 37245 from original version ax-c11 37244. See Theorem
axc11 2429 for the derivation of ax-c11 37244 from ax-c11n 37245.
This theorem should not be referenced in any proof. Instead, use ax-c11n 37245 above so that uses of ax-c11n 37245 can be more easily identified, or use aecom-o 37258 when this form is needed for studies involving ax-c11 37244 and omitting ax-5 1913. (Contributed by NM, 16-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥) | ||
Theorem | naecoms-o 37284 | A commutation rule for distinct variable specifiers. Version of naecoms 2428 using ax-c11 37244. (Contributed by NM, 2-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → 𝜑) ⇒ ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → 𝜑) | ||
Theorem | hbnae-o 37285 | All variables are effectively bound in a distinct variable specifier. Lemma L19 in [Megill] p. 446 (p. 14 of the preprint). Version of hbnae 2431 using ax-c11 37244. (Contributed by NM, 13-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦) | ||
Theorem | dvelimf-o 37286 | Proof of dvelimh 2449 that uses ax-c11 37244 but not ax-c15 37246, ax-c11n 37245, or ax-12 2171. Version of dvelimh 2449 using ax-c11 37244 instead of axc11 2429. (Contributed by NM, 12-Nov-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜓 → ∀𝑧𝜓) & ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓)) | ||
Theorem | dral2-o 37287 | 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 2437 using ax-c11 37244. (Contributed by NM, 27-Feb-2005.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑧𝜑 ↔ ∀𝑧𝜓)) | ||
Theorem | aev-o 37288* | A "distinctor elimination" lemma with no disjoint variable conditions on variables in the consequent, proved without using ax-c16 37249. Version of aev 2060 using ax-c11 37244. (Contributed by NM, 8-Nov-2006.) (Proof shortened by Andrew Salmon, 21-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑤 = 𝑣) | ||
Theorem | ax5eq 37289* | Theorem to add distinct quantifier to atomic formula. (This theorem demonstrates the induction basis for ax-5 1913 considered as a metatheorem. Do not use it for later proofs - use ax-5 1913 instead, to avoid reference to the redundant axiom ax-c16 37249.) (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦) | ||
Theorem | dveeq2-o 37290* | Quantifier introduction when one pair of variables is distinct. Version of dveeq2 2377 using ax-c15 37246. (Contributed by NM, 2-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) | ||
Theorem | axc16g-o 37291* | A generalization of Axiom ax-c16 37249. Version of axc16g 2252 using ax-c11 37244. (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 37292* | Quantifier introduction when one pair of variables is distinct. Version of dveeq1 2379 using ax-c11 . (Contributed by NM, 2-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) | ||
Theorem | dveeq1-o16 37293* | Version of dveeq1 2379 using ax-c16 37249 instead of ax-5 1913. (Contributed by NM, 29-Apr-2008.) TODO: Recover proof from older set.mm to remove use of ax-5 1913. (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) | ||
Theorem | ax5el 37294* | Theorem to add distinct quantifier to atomic formula. This theorem demonstrates the induction basis for ax-5 1913 considered as a metatheorem.) (Contributed by NM, 22-Jun-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦) | ||
Theorem | axc11n-16 37295* | This theorem shows that, given ax-c16 37249, we can derive a version of ax-c11n 37245. However, it is weaker than ax-c11n 37245 because it has a distinct variable requirement. (Contributed by Andrew Salmon, 27-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑧 → ∀𝑧 𝑧 = 𝑥) | ||
Theorem | dveel2ALT 37296* | Alternate proof of dveel2 2461 using ax-c16 37249 instead of ax-5 1913. (Contributed by NM, 10-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 ∈ 𝑦 → ∀𝑥 𝑧 ∈ 𝑦)) | ||
Theorem | ax12f 37297 | Basis step for constructing a substitution instance of ax-c15 37246 without using ax-c15 37246. 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 37298 | Basis step for constructing a substitution instance of ax-c15 37246 without using ax-c15 37246. Atomic formula for equality predicate. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))) | ||
Theorem | ax12el 37299 | Basis step for constructing a substitution instance of ax-c15 37246 without using ax-c15 37246. Atomic formula for membership predicate. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))) | ||
Theorem | ax12indn 37300 | Induction step for constructing a substitution instance of ax-c15 37246 without using ax-c15 37246. Negation case. (Contributed by NM, 21-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (¬ 𝜑 → ∀𝑥(𝑥 = 𝑦 → ¬ 𝜑)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |