P. 402 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 40101-40200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pets2eq 40101	Grade-stable generalized partition-equivalence identification. After applying the same grade-stability operator (SucMap ShiftStable) to both sides, the grade-stable pet classes still coincide. Confirms that the grade/tower infrastructure is orthogonal to the partition-vs-equivalence viewpoint: stability is preserved under the PetParts = PetErs identification. This is the level at which we can freely work on whichever side is more convenient (Parts for block discipline, Ers for equivalence reasoning), without changing the stable notion of "pet". (Contributed by Peter Mazsa, 19-Feb-2026.)
⊢ Pet2Parts = Pet2Ers
21.29  Mathbox for Rodolfo Medina
21.29.1  Partitions
Theorem	prtlem60 40102	Lemma for prter3 40131. (Contributed by Rodolfo Medina, 9-Oct-2010.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜓 → (𝜃 → 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏)))
Theorem	bicomdd 40103	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 40104	Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 17-Oct-2010.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜓 → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜃 ∧ 𝜒)))
Theorem	jca3 40105	Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 14-Oct-2010.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜃 → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜃 → (𝜒 ∧ 𝜏))))
Theorem	prtlem70 40106	Lemma for prter3 40131: a rearrangement of conjuncts. (Contributed by Rodolfo Medina, 20-Oct-2010.)
⊢ ((((𝜓 ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜑) ↔ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ (𝜃 ∧ 𝜏)))) ∧ 𝜂))
Theorem	ibdr 40107	Reverse of ibd 272. (Contributed by Rodolfo Medina, 30-Sep-2010.)
⊢ (𝜑 → (𝜒 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (𝜒 → 𝜓))
Theorem	prtlem100 40108	Lemma for prter3 40131. (Contributed by Rodolfo Medina, 19-Oct-2010.)
⊢ (∃𝑥 ∈ 𝐴 (𝐵 ∈ 𝑥 ∧ 𝜑) ↔ ∃𝑥 ∈ (𝐴 ∖ {∅})(𝐵 ∈ 𝑥 ∧ 𝜑))
Theorem	prtlem5 40109*	Lemma for prter1 40128, prter2 40130, prter3 40131 and prtex 40129. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
⊢ ([𝑠 / 𝑣][𝑟 / 𝑢]∃𝑥 ∈ 𝐴 (𝑢 ∈ 𝑥 ∧ 𝑣 ∈ 𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝑟 ∈ 𝑥 ∧ 𝑠 ∈ 𝑥))
Theorem	prtlem80 40110	Lemma for prter2 40130. (Contributed by Rodolfo Medina, 17-Oct-2010.)
⊢ (𝐴 ∈ 𝐵 → ¬ 𝐴 ∈ (𝐶 ∖ {𝐴}))
Theorem	brabsb2 40111*	A closed form of brabsb 5509. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ (𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑} → (𝑧𝑅𝑤 ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑))
Theorem	eqbrrdv2 40112*	Other version of eqbrrdiv 5775. (Contributed by Rodolfo Medina, 30-Sep-2010.)
⊢ (((Rel 𝐴 ∧ Rel 𝐵) ∧ 𝜑) → (𝑥𝐴𝑦 ↔ 𝑥𝐵𝑦))    ⇒   ⊢ (((Rel 𝐴 ∧ Rel 𝐵) ∧ 𝜑) → 𝐴 = 𝐵)
Theorem	prtlem9 40113*	Lemma for prter3 40131. (Contributed by Rodolfo Medina, 25-Sep-2010.)
⊢ (𝐴 ∈ 𝐵 → ∃𝑥 ∈ 𝐵 [𝑥] ∼ = [𝐴] ∼ )
Theorem	prtlem10 40114*	Lemma for prter3 40131. (Contributed by Rodolfo Medina, 14-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ( ∼ Er 𝐴 → (𝑧 ∈ 𝐴 → (𝑧 ∼ 𝑤 ↔ ∃𝑣 ∈ 𝐴 (𝑧 ∈ [𝑣] ∼ ∧ 𝑤 ∈ [𝑣] ∼ ))))
Theorem	prtlem11 40115	Lemma for prter2 40130. (Contributed by Rodolfo Medina, 12-Oct-2010.)
⊢ (𝐵 ∈ 𝐷 → (𝐶 ∈ 𝐴 → (𝐵 = [𝐶] ∼ → 𝐵 ∈ (𝐴 / ∼ ))))
Theorem	prtlem12 40116	Lemma for prtex 40129 and prter3 40131. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ ( ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} → Rel ∼ )
Theorem	prtlem13 40117*	Lemma for prter1 40128, prter2 40130, prter3 40131 and prtex 40129. (Contributed by Rodolfo Medina, 13-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ (𝑧 ∼ 𝑤 ↔ ∃𝑣 ∈ 𝐴 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))
Theorem	prtlem16 40118*	Lemma for prtex 40129, prter2 40130 and prter3 40131. (Contributed by Rodolfo Medina, 14-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ dom ∼ = ∪ 𝐴
Theorem	prtlem400 40119*	Lemma for prter2 40130 and also a property of partitions . (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ ¬ ∅ ∈ (∪ 𝐴 / ∼ )
Syntax	wprt 40120	Extend the definition of a wff to include the partition predicate.
wff Prt 𝐴
Definition	df-prt 40121*	Define the partition predicate. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ (Prt 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅))
Theorem	erprt 40122	The quotient set of an equivalence relation is a partition. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ ( ∼ Er 𝑋 → Prt (𝐴 / ∼ ))
Theorem	prtlem14 40123*	Lemma for prter1 40128, prter2 40130 and prtex 40129. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ (Prt 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑤 ∈ 𝑥 ∧ 𝑤 ∈ 𝑦) → 𝑥 = 𝑦)))
Theorem	prtlem15 40124*	Lemma for prter1 40128 and prtex 40129. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ (Prt 𝐴 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑢 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) ∧ (𝑤 ∈ 𝑦 ∧ 𝑣 ∈ 𝑦)) → ∃𝑧 ∈ 𝐴 (𝑢 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧)))
Theorem	prtlem17 40125*	Lemma for prter2 40130. (Contributed by Rodolfo Medina, 15-Oct-2010.)
⊢ (Prt 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥) → (∃𝑦 ∈ 𝐴 (𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦) → 𝑤 ∈ 𝑥)))
Theorem	prtlem18 40126*	Lemma for prter2 40130. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ (Prt 𝐴 → ((𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣) → (𝑤 ∈ 𝑣 ↔ 𝑧 ∼ 𝑤)))
Theorem	prtlem19 40127*	Lemma for prter2 40130. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ (Prt 𝐴 → ((𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣) → 𝑣 = [𝑧] ∼ ))
Theorem	prter1 40128*	Every partition generates an equivalence relation. (Contributed by Rodolfo Medina, 13-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ (Prt 𝐴 → ∼ Er ∪ 𝐴)
Theorem	prtex 40129*	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 40130*	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 40131*	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 ∪ 𝐴 ∧ (∪ 𝐴 / 𝑆) = (𝐴 ∖ {∅})) → ∼ = 𝑆)
21.30  Mathbox for Norm Megill 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."
21.30.1  Obsolete schemes ax-c4,c5,c7,c10,c11,c11n,c15,c9,c14,c16 These older axiom schemes are obsolete and should not be used outside of this section. They are proved above as theorems axc4 , sp 2223, axc7 2351, axc10 2417, axc11 2462, axc11n 2458, axc15 2454, axc9 2414, axc14 2495, and axc16 2299.
Axiom	ax-c5 40132	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 1828. Conditional forms of the converse are given by ax-13 2404, ax-c14 40140, ax-c16 40141, and ax-5 1945. 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 2107). An interesting alternate axiomatization uses axc5c711 40167 and ax-c4 40133 in place of ax-c5 40132, ax-4 1842, ax-10 2180, and ax-11 2197. This axiom is obsolete and should no longer be used. It is proved above as Theorem sp 2223. (Contributed by NM, 3-Jan-1993.) Use sp 2223 instead. (New usage is discouraged.)
⊢ (∀𝑥𝜑 → 𝜑)
Axiom	ax-c4 40133	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 2355. (Contributed by NM, 3-Jan-1993.) (New usage is discouraged.)
⊢ (∀𝑥(∀𝑥𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
Axiom	ax-c7 40134	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 40167 in place of ax-c5 40132, ax-c7 40134, and ax-11 2197. This axiom is obsolete and should no longer be used. It is proved above as Theorem axc7 2351. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑)
Axiom	ax-c10 40135	A variant of ax6 2416. 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 2417. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.)
⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) → 𝜑)
Axiom	ax-c11 40136	Axiom ax-c11 40136 was the original version of ax-c11n 40137 ("n" for "new"), before it was discovered (in May 2008) that the shorter ax-c11n 40137 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 2462. (Contributed by NM, 10-May-1993.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑))
Axiom	ax-c11n 40137	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 40136 and was replaced with this shorter ax-c11n 40137 ("n" for "new") in May 2008. The old axiom is proved from this one as Theorem axc11 2462. Conversely, this axiom is proved from ax-c11 40136 as Theorem axc11nfromc11 40175. This axiom was proved redundant in July 2015. See Theorem axc11n 2458. This axiom is obsolete and should no longer be used. It is proved above as Theorem axc11n 2458. (Contributed by NM, 16-May-2008.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Axiom	ax-c15 40138	Axiom ax-c15 40138 was the original version of ax-12 2216, before it was discovered (in Jan. 2007) that the shorter ax-12 2216 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 40138 (from which the ax-12 2216 instance follows by Theorem ax12 2455.) The proof is by induction on formula length, using ax12eq 40190 and ax12el 40191 for the basis steps and ax12indn 40192, ax12indi 40193, and ax12inda 40197 for the induction steps. (This paragraph is true provided we use ax-c11 40136 in place of ax-c11n 40137.) This axiom is obsolete and should no longer be used. It is proved above as Theorem axc15 2454, which should be used instead. (Contributed by NM, 14-May-1993.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))
Axiom	ax-c9 40139	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 2414. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.)
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
Axiom	ax-c14 40140	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 1945; see Theorem axc14 2495. Alternately, ax-5 1945 becomes unnecessary in principle with this axiom, but we lose the more powerful metalogic afforded by ax-5 1945. We retain ax-c14 40140 here to provide completeness for systems with the simpler metalogic that results from omitting ax-5 1945, 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 2495. (Contributed by NM, 24-Jun-1993.) (New usage is discouraged.)
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦)))
Axiom	ax-c16 40141*	Axiom of Distinct Variables. The only axiom of predicate calculus requiring that variables be distinct (if we consider ax-5 1945 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 5409), but nonetheless it is technically necessary as you can see from its uses. This axiom is redundant if we include ax-5 1945; see Theorem axc16 2299. Alternately, ax-5 1945 becomes logically redundant in the presence of this axiom, but without ax-5 1945 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 40141 here to provide logical completeness for systems with the simpler metalogic that results from omitting ax-5 1945, 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 2299. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑))
21.30.2  Rederive new axioms ax-4, ax-10, ax-6, ax-12, ax-13 from old Theorems ax12fromc15 40154 and ax13fromc9 40155 require some intermediate theorems that are included in this section.
Theorem	axc5 40142	This theorem repeats sp 2223 under the name axc5 40142, so that the Metamath program "MM> VERIFY MARKUP" command will check that it matches axiom scheme ax-c5 40132. (Contributed by NM, 18-Aug-2017.) (Proof modification is discouraged.) Use sp 2223 instead. (New usage is discouraged.)
⊢ (∀𝑥𝜑 → 𝜑)
Theorem	ax4fromc4 40143	Rederivation of Axiom ax-4 1842 from ax-c4 40133, ax-c5 40132, ax-gen 1828 and minimal implicational calculus { ax-mp 5, ax-1 6, ax-2 7 }. See axc4 2355 for the derivation of ax-c4 40133 from ax-4 1842. (Contributed by NM, 23-May-2008.) (Proof modification is discouraged.) Use ax-4 1842 instead. (New usage is discouraged.)
⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
Theorem	ax10fromc7 40144	Rederivation of Axiom ax-10 2180 from ax-c7 40134, ax-c4 40133, ax-c5 40132, ax-gen 1828 and propositional calculus. See axc7 2351 for the derivation of ax-c7 40134 from ax-10 2180. (Contributed by NM, 23-May-2008.) (Proof modification is discouraged.) Use ax-10 2180 instead. (New usage is discouraged.)
⊢ (¬ ∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑)
Theorem	ax6fromc10 40145	Rederivation of Axiom ax-6 2002 from ax-c7 40134, ax-c10 40135, ax-gen 1828 and propositional calculus. See axc10 2417 for the derivation of ax-c10 40135 from ax-6 2002. Lemma L18 in [Megill] p. 446 (p. 14 of the preprint). (Contributed by NM, 14-May-1993.) (Proof modification is discouraged.) Use ax-6 2002 instead. (New usage is discouraged.)
⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦
Theorem	hba1-o 40146	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 40147	Inference version of ax-c4 40133. (Contributed by NM, 3-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑥𝜓)
Theorem	equid1 40148	Proof of equid 2047 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 1945; see the proof of equid 2047. See equid1ALT 40174 for an alternate proof. (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑥 = 𝑥
Theorem	equcomi1 40149	Proof of equcomi 2052 from equid1 40148, avoiding use of ax-5 1945 (the only use of ax-5 1945 is via ax7 2051, so using ax-7 2043 instead would remove dependency on ax-5 1945). (Contributed by BJ, 8-Jul-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
Theorem	aecom-o 40150	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 2459 using ax-c11 40136. Unlike axc11nfromc11 40175, this version does not require ax-5 1945 (see comment of equcomi1 40149). (Contributed by NM, 10-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Theorem	aecoms-o 40151	A commutation rule for identical variable specifiers. Version of aecoms 2460 using ax-c11 40136. (Contributed by NM, 10-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ (∀𝑦 𝑦 = 𝑥 → 𝜑)
Theorem	hbae-o 40152	All variables are effectively bound in an identical variable specifier. Version of hbae 2463 using ax-c11 40136. (Contributed by NM, 13-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦)
Theorem	dral1-o 40153	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 2471 using ax-c11 40136. (Contributed by NM, 24-Nov-1994.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 ↔ ∀𝑦𝜓))
Theorem	ax12fromc15 40154	Rederivation of Axiom ax-12 2216 from ax-c15 40138, ax-c11 40136 (used through dral1-o 40153), and other older axioms. See Theorem axc15 2454 for the derivation of ax-c15 40138 from ax-12 2216. An open problem is whether we can prove this using ax-c11n 40137 instead of ax-c11 40136. This proof uses newer axioms ax-4 1842 and ax-6 2002, 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 40133 and ax-c10 40135. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	ax13fromc9 40155	Derive ax-13 2404 from ax-c9 40139 and other older axioms. This proof uses newer axioms ax-4 1842 and ax-6 2002, 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 40133 and ax-c10 40135. (Contributed by NM, 21-Dec-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧))
21.30.3  Legacy theorems using obsolete axioms 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 40156*	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 1945 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 1828, ax-c4 40133, ax-c5 40132, ax-11 2197, ax-c7 40134, ax-7 2043, ax-c9 40139, ax-c10 40135, ax-c11 40136, ax-8 2149, ax-9 2157, ax-c14 40140, ax-c15 40138, and ax-c16 40141: in that system, we can derive any instance of ax-5 1945 not containing wff variables by induction on formula length, using ax5eq 40181 and ax5el 40186 for the basis together with hbn 2332, hbal 2207, and hbim 2336. 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 40157	Generalization of antecedent. (Contributed by NM, 5-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	hbequid 40158	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 40135.) (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 40159	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 1842, ax-7 2043, ax-c9 40139, and ax-gen 1828. This shows that this can be proved without ax6 2416, even though Theorem equid 2047 cannot. A shorter proof using ax6 2416 is obtainable from equid 2047 and hbth 1836.) Remark added 2-Dec-2015 NM: This proof does implicitly use ax6v 2003, which is used for the derivation of axc9 2414, unless we consider ax-c9 40139 the starting axiom rather than ax-13 2404. (Contributed by NM, 13-Jan-2011.) (Revised by Mario Carneiro, 12-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑦 𝑥 = 𝑥
Theorem	axc5c7 40160	Proof of a single axiom that can replace ax-c5 40132 and ax-c7 40134. See axc5c7toc5 40161 and axc5c7toc7 40162 for the rederivation of those axioms. (Contributed by Scott Fenton, 12-Sep-2005.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((∀𝑥 ¬ ∀𝑥𝜑 → ∀𝑥𝜑) → 𝜑)
Theorem	axc5c7toc5 40161	Rederivation of ax-c5 40132 from axc5c7 40160. 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 40162	Rederivation of ax-c7 40134 from axc5c7 40160. 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 40163	Proof of a single axiom that can replace both ax-c7 40134 and ax-11 2197. See axc711toc7 40165 and axc711to11 40166 for the rederivation of those axioms. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 ¬ ∀𝑦∀𝑥𝜑 → ∀𝑦𝜑)
Theorem	nfa1-o 40164	𝑥 is not free in ∀𝑥𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥∀𝑥𝜑
Theorem	axc711toc7 40165	Rederivation of ax-c7 40134 from axc711 40163. Note that ax-c7 40134 and ax-11 2197 are not used by the rederivation. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑)
Theorem	axc711to11 40166	Rederivation of ax-11 2197 from axc711 40163. Note that ax-c7 40134 and ax-11 2197 are not used by the rederivation. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
Theorem	axc5c711 40167	Proof of a single axiom that can replace ax-c5 40132, ax-c7 40134, and ax-11 2197 in a subsystem that includes these axioms plus ax-c4 40133 and ax-gen 1828 (and propositional calculus). See axc5c711toc5 40168, axc5c711toc7 40169, and axc5c711to11 40170 for the rederivation of those axioms. This theorem extends the idea in Scott Fenton's axc5c7 40160. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑 → ∀𝑥𝜑) → 𝜑)
Theorem	axc5c711toc5 40168	Rederivation of ax-c5 40132 from axc5c711 40167. Only propositional calculus is used by the rederivation. (Contributed by NM, 19-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥𝜑 → 𝜑)
Theorem	axc5c711toc7 40169	Rederivation of ax-c7 40134 from axc5c711 40167. Note that ax-c7 40134 and ax-11 2197 are not used by the rederivation. The use of alimi 1844 (which uses ax-c5 40132) is allowed since we have already proved axc5c711toc5 40168. (Contributed by NM, 19-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑)
Theorem	axc5c711to11 40170	Rederivation of ax-11 2197 from axc5c711 40167. Note that ax-c7 40134 and ax-11 2197 are not used by the rederivation. The use of alimi 1844 (which uses ax-c5 40132) is allowed since we have already proved axc5c711toc5 40168. (Contributed by NM, 19-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
Theorem	equidqe 40171	equid 2047 with existential quantifier without using ax-c5 40132 or ax-5 1945. (Contributed by NM, 13-Jan-2011.) (Proof shortened by Wolf Lammen, 27-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ ∀𝑦 ¬ 𝑥 = 𝑥
Theorem	axc5sp1 40172	A special case of ax-c5 40132 without using ax-c5 40132 or ax-5 1945. (Contributed by NM, 13-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑦 ¬ 𝑥 = 𝑥 → ¬ 𝑥 = 𝑥)
Theorem	equidq 40173	equid 2047 with universal quantifier without using ax-c5 40132 or ax-5 1945. (Contributed by NM, 13-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∀𝑦 𝑥 = 𝑥
Theorem	equid1ALT 40174	Alternate proof of equid 2047 and equid1 40148 from older axioms ax-c7 40134, ax-c10 40135 and ax-c9 40139. (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑥 = 𝑥
Theorem	axc11nfromc11 40175	Rederivation of ax-c11n 40137 from original version ax-c11 40136. See Theorem axc11 2462 for the derivation of ax-c11 40136 from ax-c11n 40137. This theorem should not be referenced in any proof. Instead, use ax-c11n 40137 above so that uses of ax-c11n 40137 can be more easily identified, or use aecom-o 40150 when this form is needed for studies involving ax-c11 40136 and omitting ax-5 1945. (Contributed by NM, 16-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Theorem	naecoms-o 40176	A commutation rule for distinct variable specifiers. Version of naecoms 2461 using ax-c11 40136. (Contributed by NM, 2-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → 𝜑)
Theorem	hbnae-o 40177	All variables are effectively bound in a distinct variable specifier. Lemma L19 in [Megill] p. 446 (p. 14 of the preprint). Version of hbnae 2464 using ax-c11 40136. (Contributed by NM, 13-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦)
Theorem	dvelimf-o 40178	Proof of dvelimh 2482 that uses ax-c11 40136 but not ax-c15 40138, ax-c11n 40137, or ax-12 2216. Version of dvelimh 2482 using ax-c11 40136 instead of axc11 2462. (Contributed by NM, 12-Nov-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜓 → ∀𝑧𝜓)    &   ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓))
Theorem	dral2-o 40179	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 2470 using ax-c11 40136. (Contributed by NM, 27-Feb-2005.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑧𝜑 ↔ ∀𝑧𝜓))
Theorem	aev-o 40180*	A "distinctor elimination" lemma with no disjoint variable conditions on variables in the consequent, proved without using ax-c16 40141. Version of aev 2094 using ax-c11 40136. (Contributed by NM, 8-Nov-2006.) (Proof shortened by Andrew Salmon, 21-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑤 = 𝑣)
Theorem	ax5eq 40181*	Theorem to add distinct quantifier to atomic formula. (This theorem demonstrates the induction basis for ax-5 1945 considered as a metatheorem. Do not use it for later proofs - use ax-5 1945 instead, to avoid reference to the redundant axiom ax-c16 40141.) (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)
Theorem	dveeq2-o 40182*	Quantifier introduction when one pair of variables is distinct. Version of dveeq2 2410 using ax-c15 40138. (Contributed by NM, 2-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
Theorem	axc16g-o 40183*	A generalization of Axiom ax-c16 40141. Version of axc16g 2298 using ax-c11 40136. (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 40184*	Quantifier introduction when one pair of variables is distinct. Version of dveeq1 2412 using ax-c11 . (Contributed by NM, 2-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧))
Theorem	dveeq1-o16 40185*	Version of dveeq1 2412 using ax-c16 40141 instead of ax-5 1945. (Contributed by NM, 29-Apr-2008.) TODO: Recover proof from older set.mm to remove use of ax-5 1945. (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧))
Theorem	ax5el 40186*	Theorem to add distinct quantifier to atomic formula. This theorem demonstrates the induction basis for ax-5 1945 considered as a metatheorem.) (Contributed by NM, 22-Jun-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦)
Theorem	axc11n-16 40187*	This theorem shows that, given ax-c16 40141, we can derive a version of ax-c11n 40137. However, it is weaker than ax-c11n 40137 because it has a distinct variable requirement. (Contributed by Andrew Salmon, 27-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑧 → ∀𝑧 𝑧 = 𝑥)
Theorem	dveel2ALT 40188*	Alternate proof of dveel2 2494 using ax-c16 40141 instead of ax-5 1945. (Contributed by NM, 10-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 ∈ 𝑦 → ∀𝑥 𝑧 ∈ 𝑦))
Theorem	ax12f 40189	Basis step for constructing a substitution instance of ax-c15 40138 without using ax-c15 40138. 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 40190	Basis step for constructing a substitution instance of ax-c15 40138 without using ax-c15 40138. Atomic formula for equality predicate. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))
Theorem	ax12el 40191	Basis step for constructing a substitution instance of ax-c15 40138 without using ax-c15 40138. Atomic formula for membership predicate. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
Theorem	ax12indn 40192	Induction step for constructing a substitution instance of ax-c15 40138 without using ax-c15 40138. Negation case. (Contributed by NM, 21-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (¬ 𝜑 → ∀𝑥(𝑥 = 𝑦 → ¬ 𝜑))))
Theorem	ax12indi 40193	Induction step for constructing a substitution instance of ax-c15 40138 without using ax-c15 40138. Implication case. (Contributed by NM, 21-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))    &   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜓 → ∀𝑥(𝑥 = 𝑦 → 𝜓))))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → ((𝜑 → 𝜓) → ∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓)))))
Theorem	ax12indalem 40194	Lemma for ax12inda2 40196 and ax12inda 40197. (Contributed by NM, 24-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))    ⇒   ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))))
Theorem	ax12inda2ALT 40195*	Alternate proof of ax12inda2 40196, slightly more direct and not requiring ax-c16 40141. (Contributed by NM, 4-May-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))))
Theorem	ax12inda2 40196*	Induction step for constructing a substitution instance of ax-c15 40138 without using ax-c15 40138. Quantification case. When 𝑧 and 𝑦 are distinct, this theorem avoids the dummy variables needed by the more general ax12inda 40197. (Contributed by NM, 24-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))))
Theorem	ax12inda 40197*	Induction step for constructing a substitution instance of ax-c15 40138 without using ax-c15 40138. Quantification case. (When 𝑧 and 𝑦 are distinct, ax12inda2 40196 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 40198*	Rederivation of ax-c15 40138 from ax12v 2217 (without using ax-c15 40138 or the full ax-12 2216). Thus, the hypothesis (ax12v 2217) provides an alternate axiom that can be used in place of ax-c15 40138. See also axc15 2454. (Contributed by NM, 2-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑧 → (𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑)))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))
Theorem	ax12a2-o 40199*	Derive ax-c15 40138 from a hypothesis in the form of ax-12 2216, without using ax-12 2216 or ax-c15 40138. The hypothesis is weaker than ax-12 2216, with 𝑧 both distinct from 𝑥 and not occurring in 𝜑. Thus, the hypothesis provides an alternate axiom that can be used in place of ax-12 2216, if we also have ax-c11 40136, which this proof uses. As Theorem ax12 2455 shows, the distinct variable conditions are optional. An open problem is whether we can derive this with ax-c11n 40137 instead of ax-c11 40136. (Contributed by NM, 2-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑧 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑)))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))
Theorem	axc11-o 40200	Show that ax-c11 40136 can be derived from ax-c11n 40137 and ax-12 2216. An open problem is whether this theorem can be derived from ax-c11n 40137 and the others when ax-12 2216 is replaced with ax-c15 40138 or ax12v 2217. See Theorems axc11nfromc11 40175 for the rederivation of ax-c11n 40137 from axc11 2462. Normally, axc11 2462 should be used rather than ax-c11 40136 or axc11-o 40200, except by theorems specifically studying the latter's properties. (Contributed by NM, 16-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑))