P. 400 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 39901-40000   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-peters 39901*	Define the class of equivalence-side general partition-equivalence spans. ⟨𝑟, 𝑛⟩ ∈ PetErs means: (1) 𝑟 is a set-relation (𝑟 ∈ Rels), and (2) 𝑛 is a carrier recognized on the equivalence side of membership (𝑛 ∈ CoMembErs), and (3) the coset relation of the lifted span, ≀ (𝑟 ⋉ (◡ E ↾ 𝑛)), is an equivalence relation on its natural quotient with carrier 𝑛 (i.e. ≀ (𝑟 ⋉ (◡ E ↾ 𝑛)) Ers 𝑛). This packages the equivalence-view of the same lifted construction that underlies PetParts. It is designed to be parallel to PetParts so later proofs can freely choose the partition side (Parts) or the equivalence side (Ers) without rebuilding the bridge each time; the identification is provided by petseq 39908 (using typesafepets 39907 and mpets 39888). The explicit typing (𝑟 ∈ Rels ∧ 𝑛 ∈ CoMembErs ) is included for the same reason as in df-petparts 39900: to make typedness a reusable module. (Contributed by Peter Mazsa, 19-Feb-2026.) (Revised by Peter Mazsa, 25-Feb-2026.)
⊢ PetErs = {⟨𝑟, 𝑛⟩ ∣ ((𝑟 ∈ Rels ∧ 𝑛 ∈ CoMembErs ) ∧ ≀ (𝑟 ⋉ (◡ E ↾ 𝑛)) Ers 𝑛)}
Definition	df-pet2parts 39902	Define the class of grade- and blocklift-stable partition-side general partition-equivalence spans. It consists of those ⟨𝑟, 𝑛⟩ ∈ PetParts such that ⟨𝑟, 𝑛⟩ remains in PetParts after shifting one grade along SucMap (via ShiftStable). Concretely: ⟨𝑟, 𝑛⟩ ∈ PetParts and there exists a predecessor 𝑚 with suc 𝑚 = 𝑛 such that ⟨𝑟, 𝑚⟩ ∈ PetParts (encoded by SucMap ∘ PetParts inside ShiftStable). I.e., it introduces the external (tower/grade) stability axis. This is the "4th level" for pet 39897 (see dfpet2parts2 39905): beyond (i) carrier membership partition, (ii) disjointness, and (iii) semantic equilibrium, we require (iv) stability under a canonical grade shift. PetParts already enforces disjointness and the quotient-carrier equation for the lifted span (hence semantic equilibrium via dfpetparts2 39904). Pet2Parts adds the external grade (tower) stability axis via df-shiftstable 39414 with SucMap. This (iv) is why we need explicit second-level Pet2Parts, while Disjs typically does not: Disjs already packages its own internal two-step consistency (carrier + map) by dfdisjs6 39874 / dfdisjs7 39875, whereas pet 39897 has an additional grade axis that must be imposed separately. (Contributed by Peter Mazsa, 19-Feb-2026.)
⊢ Pet2Parts = ( SucMap ShiftStable PetParts )
Definition	df-pet2ers 39903	Define the class of grade- and blocklift-stable equivalence-side general partition-equivalence spans. The equivalence-side analogue of Pet2Parts: stability of PetErs under one-step grade shift along SucMap. Ensures that the equivalence-side formulation supports the same tower/grade infrastructure as the partition-side formulation. SucMap ShiftStable is the grade axis and does not change the equivalence-vs-partition viewpoint (reinforced by pets2eq 39909). (Contributed by Peter Mazsa, 19-Feb-2026.)
⊢ Pet2Ers = ( SucMap ShiftStable PetErs )
Theorem	dfpetparts2 39904*	Alternate definition of PetParts as typedness + disjoint-span + block-lift equilibrium. This theorem is the key modularization step. It decomposes PetParts into the intersection of three orthogonal modules: (T) typedness: ⟨𝑟, 𝑛⟩ ∈ ( Rels × MembParts ), (D) disjoint-span: (𝑟 ⋉ (◡ E ↾ 𝑛)) ∈ Disjs, (E) semantic equilibrium: ⟨𝑟, 𝑛⟩ ∈ BlockLiftFix, i.e. the carrier 𝑛 is a fixpoint of the induced block-generation operator. Conceptually, (D) provides the disjointness/quotient discipline for the lifted span, while (E) prevents hidden carrier drift (refinement or coarsening of what counts as a block) by enforcing the fixpoint equation. The point of this theorem is that these constraints can be imposed and reused independently by later constructions, while their intersection recovers the intended Parts-based notion. This mirrors the internal packaging of Disjs (see dfdisjs6 39874 / dfdisjs7 39875): for disjoint relations, the "map layer + carrier layer" decomposition is internal via QMap and ElDisjs; for PetParts, the carrier 𝑛 is an external parameter, so the additional carrier stability must be factored explicitly as BlockLiftFix. (Contributed by Peter Mazsa, 20-Feb-2026.) (Revised by Peter Mazsa, 25-Feb-2026.)
⊢ PetParts = ((( Rels × MembParts ) ∩ {⟨𝑟, 𝑛⟩ ∣ (𝑟 ⋉ (◡ E ↾ 𝑛)) ∈ Disjs }) ∩ BlockLiftFix )
Theorem	dfpet2parts2 39905*	Grade stability applied to the decomposed PetParts modules. Pet2Parts is obtained by applying the grade-stability operator SucMap ShiftStable (see df-shiftstable 39414) to the modular intersection from dfpetparts2 39904. This makes the two orthogonal stability axes explicit: (E) semantic stability / equilibrium: BlockLiftFix, (G) grade stability: SucMap ShiftStable, assembled on top of typedness and disjoint-span base modules. This is the principled "extra level" that does not arise for Disjs: disjoint relations already bundle their internal map/carrier consistency via QMap and ElDisjs (see dfdisjs6 39874 / dfdisjs7 39875), while the present construction has an additional external grading axis imposed by the canonical successor map SucMap. (Contributed by Peter Mazsa, 20-Feb-2026.) (Revised by Peter Mazsa, 25-Feb-2026.)
⊢ Pet2Parts = ( SucMap ShiftStable ((( Rels × MembParts ) ∩ {⟨𝑟, 𝑛⟩ ∣ (𝑟 ⋉ (◡ E ↾ 𝑛)) ∈ Disjs }) ∩ BlockLiftFix ))
Theorem	dfpeters2 39906*	Alternate definition of PetErs in fully modular form. This expands the Ers 𝑛 predicate into: (i) a typedness module ( Rels × CoMembErs ), (ii) an equivalence module for the coset relation ≀ (𝑟 ⋉ (◡ E ↾ 𝑛)) ∈ EqvRels, (iii) the corresponding quotient-carrier (domain quotient) equation dom ≀ (...) / ≀ (...) = 𝑛. This is the equivalence-side counterpart of the modular decomposition dfpetparts2 39904 on the partition side. (Contributed by Peter Mazsa, 25-Feb-2026.)
⊢ PetErs = ((( Rels × CoMembErs ) ∩ {⟨𝑟, 𝑛⟩ ∣ ≀ (𝑟 ⋉ (◡ E ↾ 𝑛)) ∈ EqvRels }) ∩ {⟨𝑟, 𝑛⟩ ∣ (dom ≀ (𝑟 ⋉ (◡ E ↾ 𝑛)) / ≀ (𝑟 ⋉ (◡ E ↾ 𝑛))) = 𝑛})
Theorem	typesafepets 39907	Type-safe pets 39898 scheme. On a membership block-carrier 𝐴 ∈ MembParts, the lifted span (𝑅 ⋉ (◡ E ↾ 𝐴)) yields a generalized partition of 𝐴 iff its coset relation yields an equivalence relation on the same carrier 𝐴. This is the type-safe replacement for the earlier broad pets 39898: it explicitly restricts to carriers where 𝐴 is already known to be a block-family (by MembParts). That removes the standard type-safety objection ("are you equating a quotient-carrier of blocks with raw witnesses?") by construction. It is the key bridge used to identify the partition-side and equivalence-side pet classes (petseq 39908), in complete parallel with the membership bridge mpets 39888. This theorem is intentionally not the definition of PetParts; it is the bridge used by petseq 39908 after typedness is enforced by the "Pet*" definitions. (Contributed by Peter Mazsa, 19-Feb-2026.)
⊢ ((𝐴 ∈ MembParts ∧ 𝑅 ∈ 𝑉) → ((𝑅 ⋉ (◡ E ↾ 𝐴)) Parts 𝐴 ↔ ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) Ers 𝐴))
Theorem	petseq 39908	Generalized partition-equivalence identification. The partition-side scheme PetParts and the equivalence-side scheme PetErs define the same class of spans (pairs ⟨𝑟, 𝑛⟩). This plays the same organizational role for lifted spans that mpets 39888 plays for carriers: mpets 39888 identifies MembParts with CoMembErs at the membership-carrier level, while petseq 39908 identifies the corresponding span-level predicates built from Parts and Ers. Unlike the earlier broad pets 39898, the bridge used here is the type-safe span theorem typesafepets 39907, which restricts to membership block-carriers. Since typedness (𝑟 ∈ Rels and the appropriate carrier condition) is now built directly into PetParts and PetErs, this theorem can be used downstream without repeatedly re-establishing basic typing premises. (Contributed by Peter Mazsa, 19-Feb-2026.)
⊢ PetParts = PetErs
Theorem	pets2eq 39909	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.28  Mathbox for Rodolfo Medina
21.28.1  Partitions
Theorem	prtlem60 39910	Lemma for prter3 39939. (Contributed by Rodolfo Medina, 9-Oct-2010.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜓 → (𝜃 → 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏)))
Theorem	bicomdd 39911	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 39912	Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 17-Oct-2010.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜓 → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜃 ∧ 𝜒)))
Theorem	jca3 39913	Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 14-Oct-2010.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜃 → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜃 → (𝜒 ∧ 𝜏))))
Theorem	prtlem70 39914	Lemma for prter3 39939: a rearrangement of conjuncts. (Contributed by Rodolfo Medina, 20-Oct-2010.)
⊢ ((((𝜓 ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜑) ↔ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ (𝜃 ∧ 𝜏)))) ∧ 𝜂))
Theorem	ibdr 39915	Reverse of ibd 272. (Contributed by Rodolfo Medina, 30-Sep-2010.)
⊢ (𝜑 → (𝜒 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (𝜒 → 𝜓))
Theorem	prtlem100 39916	Lemma for prter3 39939. (Contributed by Rodolfo Medina, 19-Oct-2010.)
⊢ (∃𝑥 ∈ 𝐴 (𝐵 ∈ 𝑥 ∧ 𝜑) ↔ ∃𝑥 ∈ (𝐴 ∖ {∅})(𝐵 ∈ 𝑥 ∧ 𝜑))
Theorem	prtlem5 39917*	Lemma for prter1 39936, prter2 39938, prter3 39939 and prtex 39937. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
⊢ ([𝑠 / 𝑣][𝑟 / 𝑢]∃𝑥 ∈ 𝐴 (𝑢 ∈ 𝑥 ∧ 𝑣 ∈ 𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝑟 ∈ 𝑥 ∧ 𝑠 ∈ 𝑥))
Theorem	prtlem80 39918	Lemma for prter2 39938. (Contributed by Rodolfo Medina, 17-Oct-2010.)
⊢ (𝐴 ∈ 𝐵 → ¬ 𝐴 ∈ (𝐶 ∖ {𝐴}))
Theorem	brabsb2 39919*	A closed form of brabsb 5505. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ (𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑} → (𝑧𝑅𝑤 ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑))
Theorem	eqbrrdv2 39920*	Other version of eqbrrdiv 5770. (Contributed by Rodolfo Medina, 30-Sep-2010.)
⊢ (((Rel 𝐴 ∧ Rel 𝐵) ∧ 𝜑) → (𝑥𝐴𝑦 ↔ 𝑥𝐵𝑦))    ⇒   ⊢ (((Rel 𝐴 ∧ Rel 𝐵) ∧ 𝜑) → 𝐴 = 𝐵)
Theorem	prtlem9 39921*	Lemma for prter3 39939. (Contributed by Rodolfo Medina, 25-Sep-2010.)
⊢ (𝐴 ∈ 𝐵 → ∃𝑥 ∈ 𝐵 [𝑥] ∼ = [𝐴] ∼ )
Theorem	prtlem10 39922*	Lemma for prter3 39939. (Contributed by Rodolfo Medina, 14-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ( ∼ Er 𝐴 → (𝑧 ∈ 𝐴 → (𝑧 ∼ 𝑤 ↔ ∃𝑣 ∈ 𝐴 (𝑧 ∈ [𝑣] ∼ ∧ 𝑤 ∈ [𝑣] ∼ ))))
Theorem	prtlem11 39923	Lemma for prter2 39938. (Contributed by Rodolfo Medina, 12-Oct-2010.)
⊢ (𝐵 ∈ 𝐷 → (𝐶 ∈ 𝐴 → (𝐵 = [𝐶] ∼ → 𝐵 ∈ (𝐴 / ∼ ))))
Theorem	prtlem12 39924*	Lemma for prtex 39937 and prter3 39939. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ ( ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} → Rel ∼ )
Theorem	prtlem13 39925*	Lemma for prter1 39936, prter2 39938, prter3 39939 and prtex 39937. (Contributed by Rodolfo Medina, 13-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ (𝑧 ∼ 𝑤 ↔ ∃𝑣 ∈ 𝐴 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))
Theorem	prtlem16 39926*	Lemma for prtex 39937, prter2 39938 and prter3 39939. (Contributed by Rodolfo Medina, 14-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ dom ∼ = ∪ 𝐴
Theorem	prtlem400 39927*	Lemma for prter2 39938 and also a property of partitions . (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ ¬ ∅ ∈ (∪ 𝐴 / ∼ )
Syntax	wprt 39928	Extend the definition of a wff to include the partition predicate.
wff Prt 𝐴
Definition	df-prt 39929*	Define the partition predicate. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ (Prt 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅))
Theorem	erprt 39930	The quotient set of an equivalence relation is a partition. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ ( ∼ Er 𝑋 → Prt (𝐴 / ∼ ))
Theorem	prtlem14 39931*	Lemma for prter1 39936, prter2 39938 and prtex 39937. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ (Prt 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑤 ∈ 𝑥 ∧ 𝑤 ∈ 𝑦) → 𝑥 = 𝑦)))
Theorem	prtlem15 39932*	Lemma for prter1 39936 and prtex 39937. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ (Prt 𝐴 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑢 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) ∧ (𝑤 ∈ 𝑦 ∧ 𝑣 ∈ 𝑦)) → ∃𝑧 ∈ 𝐴 (𝑢 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧)))
Theorem	prtlem17 39933*	Lemma for prter2 39938. (Contributed by Rodolfo Medina, 15-Oct-2010.)
⊢ (Prt 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥) → (∃𝑦 ∈ 𝐴 (𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦) → 𝑤 ∈ 𝑥)))
Theorem	prtlem18 39934*	Lemma for prter2 39938. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ (Prt 𝐴 → ((𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣) → (𝑤 ∈ 𝑣 ↔ 𝑧 ∼ 𝑤)))
Theorem	prtlem19 39935*	Lemma for prter2 39938. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ (Prt 𝐴 → ((𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣) → 𝑣 = [𝑧] ∼ ))
Theorem	prter1 39936*	Every partition generates an equivalence relation. (Contributed by Rodolfo Medina, 13-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ (Prt 𝐴 → ∼ Er ∪ 𝐴)
Theorem	prtex 39937*	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 39938*	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 39939*	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.29  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.29.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 2220, axc7 2348, axc10 2415, axc11 2460, axc11n 2456, axc15 2452, axc9 2412, axc14 2493, and axc16 2296.
Axiom	ax-c5 39940	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 2402, ax-c14 39948, ax-c16 39949, and ax-5 1943. 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 2105). An interesting alternate axiomatization uses axc5c711 39975 and ax-c4 39941 in place of ax-c5 39940, ax-4 1842, ax-10 2178, and ax-11 2194. This axiom is obsolete and should no longer be used. It is proved above as Theorem sp 2220. (Contributed by NM, 3-Jan-1993.) Use sp 2220 instead. (New usage is discouraged.)
⊢ (∀𝑥𝜑 → 𝜑)
Axiom	ax-c4 39941	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 2352. (Contributed by NM, 3-Jan-1993.) (New usage is discouraged.)
⊢ (∀𝑥(∀𝑥𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
Axiom	ax-c7 39942	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 39975 in place of ax-c5 39940, ax-c7 39942, and ax-11 2194. This axiom is obsolete and should no longer be used. It is proved above as Theorem axc7 2348. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑)
Axiom	ax-c10 39943	A variant of ax6 2414. 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 2415. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.)
⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) → 𝜑)
Axiom	ax-c11 39944	Axiom ax-c11 39944 was the original version of ax-c11n 39945 ("n" for "new"), before it was discovered (in May 2008) that the shorter ax-c11n 39945 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 2460. (Contributed by NM, 10-May-1993.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑))
Axiom	ax-c11n 39945	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 39944 and was replaced with this shorter ax-c11n 39945 ("n" for "new") in May 2008. The old axiom is proved from this one as Theorem axc11 2460. Conversely, this axiom is proved from ax-c11 39944 as Theorem axc11nfromc11 39983. This axiom was proved redundant in July 2015. See Theorem axc11n 2456. This axiom is obsolete and should no longer be used. It is proved above as Theorem axc11n 2456. (Contributed by NM, 16-May-2008.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Axiom	ax-c15 39946	Axiom ax-c15 39946 was the original version of ax-12 2213, before it was discovered (in Jan. 2007) that the shorter ax-12 2213 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 39946 (from which the ax-12 2213 instance follows by Theorem ax12 2453.) The proof is by induction on formula length, using ax12eq 39998 and ax12el 39999 for the basis steps and ax12indn 40000, ax12indi 40001, and ax12inda 40005 for the induction steps. (This paragraph is true provided we use ax-c11 39944 in place of ax-c11n 39945.) This axiom is obsolete and should no longer be used. It is proved above as Theorem axc15 2452, which should be used instead. (Contributed by NM, 14-May-1993.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))
Axiom	ax-c9 39947	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 2412. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.)
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
Axiom	ax-c14 39948	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 1943; see Theorem axc14 2493. Alternately, ax-5 1943 becomes unnecessary in principle with this axiom, but we lose the more powerful metalogic afforded by ax-5 1943. We retain ax-c14 39948 here to provide completeness for systems with the simpler metalogic that results from omitting ax-5 1943, 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 2493. (Contributed by NM, 24-Jun-1993.) (New usage is discouraged.)
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦)))
Axiom	ax-c16 39949*	Axiom of Distinct Variables. The only axiom of predicate calculus requiring that variables be distinct (if we consider ax-5 1943 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 5405), but nonetheless it is technically necessary as you can see from its uses. This axiom is redundant if we include ax-5 1943; see Theorem axc16 2296. Alternately, ax-5 1943 becomes logically redundant in the presence of this axiom, but without ax-5 1943 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 39949 here to provide logical completeness for systems with the simpler metalogic that results from omitting ax-5 1943, 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 2296. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑))
21.29.2  Rederive new axioms ax-4, ax-10, ax-6, ax-12, ax-13 from old Theorems ax12fromc15 39962 and ax13fromc9 39963 require some intermediate theorems that are included in this section.
Theorem	axc5 39950	This theorem repeats sp 2220 under the name axc5 39950, so that the Metamath program "MM> VERIFY MARKUP" command will check that it matches axiom scheme ax-c5 39940. (Contributed by NM, 18-Aug-2017.) (Proof modification is discouraged.) Use sp 2220 instead. (New usage is discouraged.)
⊢ (∀𝑥𝜑 → 𝜑)
Theorem	ax4fromc4 39951	Rederivation of Axiom ax-4 1842 from ax-c4 39941, ax-c5 39940, ax-gen 1828 and minimal implicational calculus { ax-mp 5, ax-1 6, ax-2 7 }. See axc4 2352 for the derivation of ax-c4 39941 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 39952	Rederivation of Axiom ax-10 2178 from ax-c7 39942, ax-c4 39941, ax-c5 39940, ax-gen 1828 and propositional calculus. See axc7 2348 for the derivation of ax-c7 39942 from ax-10 2178. (Contributed by NM, 23-May-2008.) (Proof modification is discouraged.) Use ax-10 2178 instead. (New usage is discouraged.)
⊢ (¬ ∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑)
Theorem	ax6fromc10 39953	Rederivation of Axiom ax-6 2000 from ax-c7 39942, ax-c10 39943, ax-gen 1828 and propositional calculus. See axc10 2415 for the derivation of ax-c10 39943 from ax-6 2000. Lemma L18 in [Megill] p. 446 (p. 14 of the preprint). (Contributed by NM, 14-May-1993.) (Proof modification is discouraged.) Use ax-6 2000 instead. (New usage is discouraged.)
⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦
Theorem	hba1-o 39954	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 39955	Inference version of ax-c4 39941. (Contributed by NM, 3-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑥𝜓)
Theorem	equid1 39956	Proof of equid 2045 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 1943; see the proof of equid 2045. See equid1ALT 39982 for an alternate proof. (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑥 = 𝑥
Theorem	equcomi1 39957	Proof of equcomi 2050 from equid1 39956, avoiding use of ax-5 1943 (the only use of ax-5 1943 is via ax7 2049, so using ax-7 2041 instead would remove dependency on ax-5 1943). (Contributed by BJ, 8-Jul-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
Theorem	aecom-o 39958	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 2457 using ax-c11 39944. Unlike axc11nfromc11 39983, this version does not require ax-5 1943 (see comment of equcomi1 39957). (Contributed by NM, 10-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Theorem	aecoms-o 39959	A commutation rule for identical variable specifiers. Version of aecoms 2458 using ax-c11 39944. (Contributed by NM, 10-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ (∀𝑦 𝑦 = 𝑥 → 𝜑)
Theorem	hbae-o 39960	All variables are effectively bound in an identical variable specifier. Version of hbae 2461 using ax-c11 39944. (Contributed by NM, 13-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦)
Theorem	dral1-o 39961	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 2469 using ax-c11 39944. (Contributed by NM, 24-Nov-1994.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 ↔ ∀𝑦𝜓))
Theorem	ax12fromc15 39962	Rederivation of Axiom ax-12 2213 from ax-c15 39946, ax-c11 39944 (used through dral1-o 39961), and other older axioms. See Theorem axc15 2452 for the derivation of ax-c15 39946 from ax-12 2213. An open problem is whether we can prove this using ax-c11n 39945 instead of ax-c11 39944. This proof uses newer axioms ax-4 1842 and ax-6 2000, 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 39941 and ax-c10 39943. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	ax13fromc9 39963	Derive ax-13 2402 from ax-c9 39947 and other older axioms. This proof uses newer axioms ax-4 1842 and ax-6 2000, 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 39941 and ax-c10 39943. (Contributed by NM, 21-Dec-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧))
21.29.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 39964*	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 1943 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 39941, ax-c5 39940, ax-11 2194, ax-c7 39942, ax-7 2041, ax-c9 39947, ax-c10 39943, ax-c11 39944, ax-8 2147, ax-9 2155, ax-c14 39948, ax-c15 39946, and ax-c16 39949: in that system, we can derive any instance of ax-5 1943 not containing wff variables by induction on formula length, using ax5eq 39989 and ax5el 39994 for the basis together with hbn 2329, hbal 2204, and hbim 2333. 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 39965	Generalization of antecedent. (Contributed by NM, 5-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	hbequid 39966	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 39943.) (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 39967	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 2041, ax-c9 39947, and ax-gen 1828. This shows that this can be proved without ax6 2414, even though Theorem equid 2045 cannot. A shorter proof using ax6 2414 is obtainable from equid 2045 and hbth 1836.) Remark added 2-Dec-2015 NM: This proof does implicitly use ax6v 2001, which is used for the derivation of axc9 2412, unless we consider ax-c9 39947 the starting axiom rather than ax-13 2402. (Contributed by NM, 13-Jan-2011.) (Revised by Mario Carneiro, 12-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑦 𝑥 = 𝑥
Theorem	axc5c7 39968	Proof of a single axiom that can replace ax-c5 39940 and ax-c7 39942. See axc5c7toc5 39969 and axc5c7toc7 39970 for the rederivation of those axioms. (Contributed by Scott Fenton, 12-Sep-2005.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((∀𝑥 ¬ ∀𝑥𝜑 → ∀𝑥𝜑) → 𝜑)
Theorem	axc5c7toc5 39969	Rederivation of ax-c5 39940 from axc5c7 39968. 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 39970	Rederivation of ax-c7 39942 from axc5c7 39968. 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 39971	Proof of a single axiom that can replace both ax-c7 39942 and ax-11 2194. See axc711toc7 39973 and axc711to11 39974 for the rederivation of those axioms. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 ¬ ∀𝑦∀𝑥𝜑 → ∀𝑦𝜑)
Theorem	nfa1-o 39972	𝑥 is not free in ∀𝑥𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥∀𝑥𝜑
Theorem	axc711toc7 39973	Rederivation of ax-c7 39942 from axc711 39971. Note that ax-c7 39942 and ax-11 2194 are not used by the rederivation. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑)
Theorem	axc711to11 39974	Rederivation of ax-11 2194 from axc711 39971. Note that ax-c7 39942 and ax-11 2194 are not used by the rederivation. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
Theorem	axc5c711 39975	Proof of a single axiom that can replace ax-c5 39940, ax-c7 39942, and ax-11 2194 in a subsystem that includes these axioms plus ax-c4 39941 and ax-gen 1828 (and propositional calculus). See axc5c711toc5 39976, axc5c711toc7 39977, and axc5c711to11 39978 for the rederivation of those axioms. This theorem extends the idea in Scott Fenton's axc5c7 39968. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑 → ∀𝑥𝜑) → 𝜑)
Theorem	axc5c711toc5 39976	Rederivation of ax-c5 39940 from axc5c711 39975. Only propositional calculus is used by the rederivation. (Contributed by NM, 19-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥𝜑 → 𝜑)
Theorem	axc5c711toc7 39977	Rederivation of ax-c7 39942 from axc5c711 39975. Note that ax-c7 39942 and ax-11 2194 are not used by the rederivation. The use of alimi 1844 (which uses ax-c5 39940) is allowed since we have already proved axc5c711toc5 39976. (Contributed by NM, 19-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑)
Theorem	axc5c711to11 39978	Rederivation of ax-11 2194 from axc5c711 39975. Note that ax-c7 39942 and ax-11 2194 are not used by the rederivation. The use of alimi 1844 (which uses ax-c5 39940) is allowed since we have already proved axc5c711toc5 39976. (Contributed by NM, 19-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
Theorem	equidqe 39979	equid 2045 with existential quantifier without using ax-c5 39940 or ax-5 1943. (Contributed by NM, 13-Jan-2011.) (Proof shortened by Wolf Lammen, 27-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ ∀𝑦 ¬ 𝑥 = 𝑥
Theorem	axc5sp1 39980	A special case of ax-c5 39940 without using ax-c5 39940 or ax-5 1943. (Contributed by NM, 13-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑦 ¬ 𝑥 = 𝑥 → ¬ 𝑥 = 𝑥)
Theorem	equidq 39981	equid 2045 with universal quantifier without using ax-c5 39940 or ax-5 1943. (Contributed by NM, 13-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∀𝑦 𝑥 = 𝑥
Theorem	equid1ALT 39982	Alternate proof of equid 2045 and equid1 39956 from older axioms ax-c7 39942, ax-c10 39943 and ax-c9 39947. (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑥 = 𝑥
Theorem	axc11nfromc11 39983	Rederivation of ax-c11n 39945 from original version ax-c11 39944. See Theorem axc11 2460 for the derivation of ax-c11 39944 from ax-c11n 39945. This theorem should not be referenced in any proof. Instead, use ax-c11n 39945 above so that uses of ax-c11n 39945 can be more easily identified, or use aecom-o 39958 when this form is needed for studies involving ax-c11 39944 and omitting ax-5 1943. (Contributed by NM, 16-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Theorem	naecoms-o 39984	A commutation rule for distinct variable specifiers. Version of naecoms 2459 using ax-c11 39944. (Contributed by NM, 2-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → 𝜑)
Theorem	hbnae-o 39985	All variables are effectively bound in a distinct variable specifier. Lemma L19 in [Megill] p. 446 (p. 14 of the preprint). Version of hbnae 2462 using ax-c11 39944. (Contributed by NM, 13-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦)
Theorem	dvelimf-o 39986	Proof of dvelimh 2480 that uses ax-c11 39944 but not ax-c15 39946, ax-c11n 39945, or ax-12 2213. Version of dvelimh 2480 using ax-c11 39944 instead of axc11 2460. (Contributed by NM, 12-Nov-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜓 → ∀𝑧𝜓)    &   ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓))
Theorem	dral2-o 39987	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 2468 using ax-c11 39944. (Contributed by NM, 27-Feb-2005.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑧𝜑 ↔ ∀𝑧𝜓))
Theorem	aev-o 39988*	A "distinctor elimination" lemma with no disjoint variable conditions on variables in the consequent, proved without using ax-c16 39949. Version of aev 2092 using ax-c11 39944. (Contributed by NM, 8-Nov-2006.) (Proof shortened by Andrew Salmon, 21-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑤 = 𝑣)
Theorem	ax5eq 39989*	Theorem to add distinct quantifier to atomic formula. (This theorem demonstrates the induction basis for ax-5 1943 considered as a metatheorem. Do not use it for later proofs - use ax-5 1943 instead, to avoid reference to the redundant axiom ax-c16 39949.) (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)
Theorem	dveeq2-o 39990*	Quantifier introduction when one pair of variables is distinct. Version of dveeq2 2408 using ax-c15 39946. (Contributed by NM, 2-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
Theorem	axc16g-o 39991*	A generalization of Axiom ax-c16 39949. Version of axc16g 2295 using ax-c11 39944. (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 39992*	Quantifier introduction when one pair of variables is distinct. Version of dveeq1 2410 using ax-c11 . (Contributed by NM, 2-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧))
Theorem	dveeq1-o16 39993*	Version of dveeq1 2410 using ax-c16 39949 instead of ax-5 1943. (Contributed by NM, 29-Apr-2008.) TODO: Recover proof from older set.mm to remove use of ax-5 1943. (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧))
Theorem	ax5el 39994*	Theorem to add distinct quantifier to atomic formula. This theorem demonstrates the induction basis for ax-5 1943 considered as a metatheorem.) (Contributed by NM, 22-Jun-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦)
Theorem	axc11n-16 39995*	This theorem shows that, given ax-c16 39949, we can derive a version of ax-c11n 39945. However, it is weaker than ax-c11n 39945 because it has a distinct variable requirement. (Contributed by Andrew Salmon, 27-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑧 → ∀𝑧 𝑧 = 𝑥)
Theorem	dveel2ALT 39996*	Alternate proof of dveel2 2492 using ax-c16 39949 instead of ax-5 1943. (Contributed by NM, 10-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 ∈ 𝑦 → ∀𝑥 𝑧 ∈ 𝑦))
Theorem	ax12f 39997	Basis step for constructing a substitution instance of ax-c15 39946 without using ax-c15 39946. 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 39998	Basis step for constructing a substitution instance of ax-c15 39946 without using ax-c15 39946. Atomic formula for equality predicate. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))
Theorem	ax12el 39999	Basis step for constructing a substitution instance of ax-c15 39946 without using ax-c15 39946. Atomic formula for membership predicate. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
Theorem	ax12indn 40000	Induction step for constructing a substitution instance of ax-c15 39946 without using ax-c15 39946. Negation case. (Contributed by NM, 21-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (¬ 𝜑 → ∀𝑥(𝑥 = 𝑦 → ¬ 𝜑))))