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
Theorem	petxrnidres 39901	A class is a partition by a range Cartesian product with the identity class restricted to it if and only if the cosets by the range Cartesian product are in equivalence relation on it. Cf. br1cossxrnidres 39516, disjALTVxrnidres 39833 and eqvrel1cossxrnidres 39870. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ((𝑅 ⋉ ( I ↾ 𝐴)) Part 𝐴 ↔ ≀ (𝑅 ⋉ ( I ↾ 𝐴)) ErALTV 𝐴)
Theorem	eqvreldisj1 39902*	The elements of the quotient set of an equivalence relation are disjoint (cf. eqvreldisj2 39903, eqvreldisj3 39904). (Contributed by Mario Carneiro, 10-Dec-2016.) (Revised by Peter Mazsa, 3-Dec-2024.)
⊢ ( EqvRel 𝑅 → ∀𝑥 ∈ (𝐴 / 𝑅)∀𝑦 ∈ (𝐴 / 𝑅)(𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅))
Theorem	eqvreldisj2 39903	The elements of the quotient set of an equivalence relation are disjoint (cf. eqvreldisj3 39904). (Contributed by Mario Carneiro, 10-Dec-2016.) (Revised by Peter Mazsa, 19-Sep-2021.)
⊢ ( EqvRel 𝑅 → ElDisj (𝐴 / 𝑅))
Theorem	eqvreldisj3 39904	The elements of the quotient set of an equivalence relation are disjoint (cf. qsdisj2 8816). (Contributed by Mario Carneiro, 10-Dec-2016.) (Revised by Peter Mazsa, 20-Jun-2019.) (Revised by Peter Mazsa, 19-Sep-2021.)
⊢ ( EqvRel 𝑅 → Disj (◡ E ↾ (𝐴 / 𝑅)))
Theorem	eqvreldisj4 39905	Intersection with the converse epsilon relation restricted to the quotient set of an equivalence relation is disjoint. (Contributed by Peter Mazsa, 30-May-2020.) (Revised by Peter Mazsa, 31-Dec-2021.)
⊢ ( EqvRel 𝑅 → Disj (𝑆 ∩ (◡ E ↾ (𝐵 / 𝑅))))
Theorem	eqvreldisj5 39906	Range Cartesian product with converse epsilon relation restricted to the quotient set of an equivalence relation is disjoint. (Contributed by Peter Mazsa, 30-May-2020.) (Revised by Peter Mazsa, 22-Sep-2021.)
⊢ ( EqvRel 𝑅 → Disj (𝑆 ⋉ (◡ E ↾ (𝐵 / 𝑅))))
Theorem	eqvrelqseqdisj2 39907	Implication of eqvreldisj2 39903, lemma for The Main Theorem of Equivalences mainer 39923. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ (( EqvRel 𝑅 ∧ (𝐵 / 𝑅) = 𝐴) → ElDisj 𝐴)
Theorem	disjimeldisjdmqs 39908	Disj implies element-disjoint quotient carrier. Supplies the carrier-disjointness half of the Disjs pattern: under Disj 𝑅, the coset family is element-disjoint. (Contributed by Peter Mazsa, 5-Feb-2026.)
⊢ ( Disj 𝑅 → ElDisj (dom 𝑅 / 𝑅))
Theorem	eldisjsim1 39909	An element of the class of disjoint relations is disjoint. (Contributed by Peter Mazsa, 11-Feb-2026.)
⊢ (𝑅 ∈ Disjs → Disj 𝑅)
Theorem	eldisjsim2 39910	An element of the class of disjoint relations is an element of the class of relations. (Contributed by Peter Mazsa, 11-Feb-2026.)
⊢ (𝑅 ∈ Disjs → 𝑅 ∈ Rels )
Theorem	disjsssrels 39911	The class of disjoint relations is a subclass of the class of relations. (Contributed by Peter Mazsa, 11-Feb-2026.)
⊢ Disjs ⊆ Rels
Theorem	eldisjsim3 39912	Disjs implies element-disjoint quotient carrier. Exports the carrier-disjointness property in the ElDisjs packaging. (Contributed by Peter Mazsa, 11-Feb-2026.)
⊢ (𝑅 ∈ Disjs → (dom 𝑅 / 𝑅) ∈ ElDisjs )
Theorem	eldisjsim4 39913	Disjs implies element-disjoint range of QMap. Same as eldisjsim3 39912 but expressed using the block-map range ran QMap 𝑅 (often the more modular expression). (Contributed by Peter Mazsa, 15-Feb-2026.)
⊢ (𝑅 ∈ Disjs → ran QMap 𝑅 ∈ ElDisjs )
Theorem	eldisjsim5 39914	Disjs is closed under QMap. If a relation is "disjoint-structured" (Disjs), then its canonical block map is also "disjoint-structured". This is the second "structure level" in Disjs: it expresses that the property is stable under passing to the canonical block map, a theme that mirrors Pet-grade stability at a different axis. (Contributed by Peter Mazsa, 15-Feb-2026.)
⊢ (𝑅 ∈ Disjs → QMap 𝑅 ∈ Disjs )
Theorem	eldisjs6 39915	Elementhood in the class of disjoints. A relation 𝑅 is in Disjs iff: it is relation-typed, and its quotient-map QMap 𝑅 is itself disjoint, and its quotient-carrier ran QMap 𝑅 = (dom 𝑅 / 𝑅) lies in ElDisjs (element-disjoint carriers). This is the central "stability-by-decomposition" theorem for Disjs: it explains why Disjs is internally well-behaved without adding an external stability clause. It is the exact template that PetParts imitates: for pet 39940, the analogue of "map layer" is the disjointness of the lifted span, the analogue of "carrier layer" is the block-lift fixpoint (BlockLiftFix), and then adds external grade stability (SucMap ShiftStable) which Disjs does not need. (Contributed by Peter Mazsa, 16-Feb-2026.)
⊢ (𝑅 ∈ Disjs ↔ (𝑅 ∈ Rels ∧ (ran QMap 𝑅 ∈ ElDisjs ∧ QMap 𝑅 ∈ Disjs )))
Theorem	eldisjs7 39916*	Elementhood in the class of disjoints. 𝑅 ∈ Disjs iff: 𝑅 ∈ Rels, and every 𝑥 belongs to at most one block 𝑢 in the quotient-carrier (dom 𝑅 / 𝑅) (element-disjointness at the carrier), and every block 𝑢 in the quotient-carrier has a unique representative 𝑡 ∈ dom 𝑅 such that 𝑢 = [𝑡]𝑅. Provides the "fully expanded" quantifier characterization of the same decomposition as eldisjs6 39915, but without explicitly mentioning QMap. This is the "E*/E!"" view that is closest in spirit to suc11reg 9620-style injectivity and to the "unique generator per block" narrative. It is also the right contrast-point to older one-line criteria like dfdisjs4 39771 (the "u R x" style), because it makes the carrier and representation discipline explicit and type-safe. (Contributed by Peter Mazsa, 16-Feb-2026.)
⊢ (𝑅 ∈ Disjs ↔ (𝑅 ∈ Rels ∧ (∀𝑥∃*𝑢 ∈ (dom 𝑅 / 𝑅)𝑥 ∈ 𝑢 ∧ ∀𝑢 ∈ (dom 𝑅 / 𝑅)∃!𝑡 ∈ dom 𝑅 𝑢 = [𝑡]𝑅)))
Theorem	dfdisjs6 39917	Alternate definition of the class of disjoints (via quotient-map stability). Disjs is the class of relations 𝑟 whose quotient-map QMap 𝑟 is again disjoint and whose induced quotient-carrier is element-disjoint. This is the definitional "stability-by-decomposition" packaging of disjointness: it builds Disjs from two internal layers (i) a carrier-layer constraint and (ii) a map-layer closure constraint. This is deliberately different from "u R x" style definitions: it makes the carrier of blocks and the uniqueness-of-representatives discipline first-class and reusable (via QMap) rather than implicit. (Contributed by Peter Mazsa, 16-Feb-2026.)
⊢ Disjs = {𝑟 ∈ Rels ∣ (ran QMap 𝑟 ∈ ElDisjs ∧ QMap 𝑟 ∈ Disjs )}
Theorem	dfdisjs7 39918*	Alternate definition of the class of disjoints (via carrier disjointness + unique representatives). Ideology-free normal form of dfdisjs6 39917: "blocks cover their elements" (∃*) and "each block has a unique generator" (∃!), expressed entirely at the quotient-carrier level. Same class as dfdisjs6 39917, but presented in fully expanded ∃* / ∃! form over the quotient-carrier (dom 𝑟 / 𝑟). Makes explicit (a) element-disjointness of the quotient-carrier and (b) unique representative existence for each block. These are exactly the two conditions that rule out type-confusions (blocks vs witnesses) and ensure canonical decomposition. This is the form that best supports analogy arguments with df-petparts 39943 and with successor-style uniqueness patterns. (Contributed by Peter Mazsa, 16-Feb-2026.)
⊢ Disjs = {𝑟 ∈ Rels ∣ (∀𝑥∃*𝑢 ∈ (dom 𝑟 / 𝑟)𝑥 ∈ 𝑢 ∧ ∀𝑢 ∈ (dom 𝑟 / 𝑟)∃!𝑡 ∈ dom 𝑟 𝑢 = [𝑡]𝑟)}
Theorem	fences3 39919	Implication of eqvrelqseqdisj2 39907 and n0eldmqseq 39709, see comment of fences 39933. (Contributed by Peter Mazsa, 30-Dec-2024.)
⊢ (( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) → ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴))
Theorem	eqvrelqseqdisj3 39920	Implication of eqvreldisj3 39904, lemma for the Member Partition Equivalence Theorem mpet3 39925. (Contributed by Peter Mazsa, 27-Oct-2020.) (Revised by Peter Mazsa, 24-Sep-2021.)
⊢ (( EqvRel 𝑅 ∧ (𝐵 / 𝑅) = 𝐴) → Disj (◡ E ↾ 𝐴))
Theorem	eqvrelqseqdisj4 39921	Lemma for petincnvepres2 39937. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ (( EqvRel 𝑅 ∧ (𝐵 / 𝑅) = 𝐴) → Disj (𝑆 ∩ (◡ E ↾ 𝐴)))
Theorem	eqvrelqseqdisj5 39922	Lemma for the Partition-Equivalence Theorem pet2 39939. (Contributed by Peter Mazsa, 15-Jul-2020.) (Revised by Peter Mazsa, 22-Sep-2021.)
⊢ (( EqvRel 𝑅 ∧ (𝐵 / 𝑅) = 𝐴) → Disj (𝑆 ⋉ (◡ E ↾ 𝐴)))
Theorem	mainer 39923	The Main Theorem of Equivalences: every equivalence relation implies equivalent comembers. (Contributed by Peter Mazsa, 26-Sep-2021.)
⊢ (𝑅 ErALTV 𝐴 → CoMembEr 𝐴)
Theorem	partimcomember 39924	Partition with general 𝑅 (in addition to the member partition cf. mpet 39928 and mpet2 39929) implies equivalent comembers. (Contributed by Peter Mazsa, 23-Sep-2021.) (Revised by Peter Mazsa, 22-Dec-2024.)
⊢ (𝑅 Part 𝐴 → CoMembEr 𝐴)
Theorem	mpet3 39925	Member Partition-Equivalence Theorem. Together with mpet 39928 mpet2 39929, mostly in its conventional cpet 39927 and cpet2 39926 form, this is what we used to think of as the partition equivalence theorem (but cf. pet2 39939 with general 𝑅). (Contributed by Peter Mazsa, 4-May-2018.) (Revised by Peter Mazsa, 26-Sep-2021.)
⊢ (( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴) ↔ ( CoElEqvRel 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴))
Theorem	cpet2 39926	The conventional form of the Member Partition-Equivalence Theorem. In the conventional case there is no (general) disjoint and no (general) partition concept: mathematicians have called disjoint or partition what we call element disjoint or member partition, see also cpet 39927. Together with cpet 39927, mpet 39928 mpet2 39929, this is what we used to think of as the partition equivalence theorem (but cf. pet2 39939 with general 𝑅). (Contributed by Peter Mazsa, 30-Dec-2024.)
⊢ (( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴) ↔ ( EqvRel ∼ 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴))
Theorem	cpet 39927	The conventional form of Member Partition-Equivalence Theorem. In the conventional case there is no (general) disjoint and no (general) partition concept: mathematicians have been calling disjoint or partition what we call element disjoint or member partition, see also cpet2 39926. Cf. mpet 39928, mpet2 39929 and mpet3 39925 for unconventional forms of Member Partition-Equivalence Theorem. Cf. pet 39940 and pet2 39939 for Partition-Equivalence Theorem with general 𝑅. (Contributed by Peter Mazsa, 31-Dec-2024.)
⊢ ( MembPart 𝐴 ↔ ( EqvRel ∼ 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴))
Theorem	mpet 39928	Member Partition-Equivalence Theorem in almost its shortest possible form, cf. the 0-ary version mpets 39931. Member partition and comember equivalence relation are the same (or: each element of 𝐴 have equivalent comembers if and only if 𝐴 is a member partition). Together with mpet2 39929, mpet3 39925, and with the conventional cpet 39927 and cpet2 39926, this is what we used to think of as the partition equivalence theorem (but cf. pet2 39939 with general 𝑅). (Contributed by Peter Mazsa, 24-Sep-2021.)
⊢ ( MembPart 𝐴 ↔ CoMembEr 𝐴)
Theorem	mpet2 39929	Member Partition-Equivalence Theorem in a shorter form. Together with mpet 39928 mpet3 39925, mostly in its conventional cpet 39927 and cpet2 39926 form, this is what we used to think of as the partition equivalence theorem (but cf. pet2 39939 with general 𝑅). (Contributed by Peter Mazsa, 24-Sep-2021.)
⊢ ((◡ E ↾ 𝐴) Part 𝐴 ↔ ≀ (◡ E ↾ 𝐴) ErALTV 𝐴)
Theorem	mpets2 39930	Member Partition-Equivalence Theorem with binary relations, cf. mpet2 39929. (Contributed by Peter Mazsa, 24-Sep-2021.)
⊢ (𝐴 ∈ 𝑉 → ((◡ E ↾ 𝐴) Parts 𝐴 ↔ ≀ (◡ E ↾ 𝐴) Ers 𝐴))
Theorem	mpets 39931	Member Partition-Equivalence Theorem in its shortest possible form: it shows that member partitions and comember equivalence relations are literally the same. Cf. pet 39940, the Partition-Equivalence Theorem, with general 𝑅. (Contributed by Peter Mazsa, 31-Dec-2024.)
⊢ MembParts = CoMembErs
Theorem	mainpart 39932	Partition with general 𝑅 also imply member partition. (Contributed by Peter Mazsa, 23-Sep-2021.) (Revised by Peter Mazsa, 22-Dec-2024.)
⊢ (𝑅 Part 𝐴 → MembPart 𝐴)
Theorem	fences 39933	The Theorem of Fences by Equivalences: all conceivable equivalence relations (besides the comember equivalence relation cf. mpet 39928) generate a partition of the members. (Contributed by Peter Mazsa, 26-Sep-2021.)
⊢ (𝑅 ErALTV 𝐴 → MembPart 𝐴)
Theorem	fences2 39934	The Theorem of Fences by Equivalences: all conceivable equivalence relations (besides the comember equivalence relation cf. mpet3 39925) 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 39935	The Main Theorem of Equivalences: every equivalence relation implies equivalent comembers. (Contributed by Peter Mazsa, 15-Oct-2021.)
⊢ (𝑅 ErALTV 𝐴 → ( CoElEqvRel 𝐴 ∧ ¬ ∅ ∈ 𝐴))
Theorem	mainerim 39936	Every equivalence relation implies equivalent coelements. (Contributed by Peter Mazsa, 20-Oct-2021.)
⊢ (𝑅 ErALTV 𝐴 → CoElEqvRel 𝐴)
Theorem	petincnvepres2 39937	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 39938	The shortest form of a partition-equivalence theorem with intersection and general 𝑅. Cf. br1cossincnvepres 39515. Cf. pet 39940. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ ((𝑅 ∩ (◡ E ↾ 𝐴)) Part 𝐴 ↔ ≀ (𝑅 ∩ (◡ E ↾ 𝐴)) ErALTV 𝐴)
Theorem	pet2 39939	Partition-Equivalence Theorem, with general 𝑅. This theorem (together with pet 39940 and pets 39941) is the main result of my investigation into set theory, see the comment of pet 39940. (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 39940	Partition-Equivalence Theorem with general 𝑅 while preserving the restricted converse epsilon relation of mpet2 39929 (as opposed to petincnvepres 39938). 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 39517. This theorem (together with pets 39941 and pet2 39939) is the main result of my investigation into set theory. It is no more general than the conventional Member Partition-Equivalence Theorem mpet 39928, mpet2 39929 and mpet3 39925 (because you cannot set 𝑅 in this theorem in such a way that you get mpet2 39929), i.e., it is not the hypothetical General Partition-Equivalence Theorem gpet ⊢ (𝑅 Part 𝐴 ↔ ≀ 𝑅 ErALTV 𝐴), but this one has a general part that mpet2 39929 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 39941	Partition-Equivalence Theorem with general 𝑅, with binary relations. This theorem (together with pet 39940 and pet2 39939) is the main result of my investigation into set theory, cf. the comment of pet 39940. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → ((𝑅 ⋉ (◡ E ↾ 𝐴)) Parts 𝐴 ↔ ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) Ers 𝐴))
Theorem	dmqsblocks 39942*	If the pet 39940 span (𝑅 ⋉ (◡ E ↾ 𝐴)) partitions 𝐴, then every block 𝑢 ∈ 𝐴 is of the form [𝑣] for some 𝑣 that not only lies in the domain but also has at least one internal element 𝑐 and at least one 𝑅-target 𝑏 (cf. also the comments of qseq 39708). It makes explicit that pet 39940 gives active representatives for each block, without ever forcing 𝑣 = 𝑢. (Contributed by Peter Mazsa, 23-Nov-2025.)
⊢ ((dom (𝑅 ⋉ (◡ E ↾ 𝐴)) / (𝑅 ⋉ (◡ E ↾ 𝐴))) = 𝐴 → ∀𝑢 ∈ 𝐴 ∃𝑣 ∈ dom (𝑅 ⋉ (◡ E ↾ 𝐴))∃𝑏∃𝑐(𝑢 = [𝑣](𝑅 ⋉ (◡ E ↾ 𝐴)) ∧ 𝑐 ∈ 𝑣 ∧ 𝑣𝑅𝑏))
21.28.23  Type-safe Partition-Equivalence: PetParts, PetErs, Pet2Parts, Pet2Ers
Definition	df-petparts 39943*	Define the class of partition-side general partition-equivalence spans. ⟨𝑟, 𝑛⟩ ∈ PetParts means: (1) 𝑟 is a set-relation (𝑟 ∈ Rels), and (2) 𝑛 is a membership block-carrier (𝑛 ∈ MembParts), and (3) the block-lift span (𝑟 ⋉ (◡ E ↾ 𝑛)) is a generalized partition on its natural quotient-carrier 𝑛 (i.e. (𝑟 ⋉ (◡ E ↾ 𝑛)) Parts 𝑛). This is the horizontal feasibility base object on the partition side, expressed in the type-safe Parts language. The explicit typing (𝑟 ∈ Rels ∧ 𝑛 ∈ MembParts ) is included at the definition level so later modular refinements can treat typedness as a first-class component (e.g. intersecting a typedness module with disjointness and equilibrium modules) without repeatedly restating it. In particular, it lets decompositions such as dfpetparts2 39947 be written as clean intersections whose first conjunct is exactly the typedness module ( Rels × MembParts ). (Contributed by Peter Mazsa, 19-Feb-2026.) (Revised by Peter Mazsa, 25-Feb-2026.)
⊢ PetParts = {⟨𝑟, 𝑛⟩ ∣ ((𝑟 ∈ Rels ∧ 𝑛 ∈ MembParts ) ∧ (𝑟 ⋉ (◡ E ↾ 𝑛)) Parts 𝑛)}
Definition	df-peters 39944*	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 39951 (using typesafepets 39950 and mpets 39931). The explicit typing (𝑟 ∈ Rels ∧ 𝑛 ∈ CoMembErs ) is included for the same reason as in df-petparts 39943: 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 39945	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 39940 (see dfpet2parts2 39948): 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 39947). Pet2Parts adds the external grade (tower) stability axis via df-shiftstable 39457 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 39917 / dfdisjs7 39918, whereas pet 39940 has an additional grade axis that must be imposed separately. (Contributed by Peter Mazsa, 19-Feb-2026.)
⊢ Pet2Parts = ( SucMap ShiftStable PetParts )
Definition	df-pet2ers 39946	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 39952). (Contributed by Peter Mazsa, 19-Feb-2026.)
⊢ Pet2Ers = ( SucMap ShiftStable PetErs )
Theorem	dfpetparts2 39947*	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 39917 / dfdisjs7 39918): 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 39948*	Grade stability applied to the decomposed PetParts modules. Pet2Parts is obtained by applying the grade-stability operator SucMap ShiftStable (see df-shiftstable 39457) to the modular intersection from dfpetparts2 39947. 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 39917 / dfdisjs7 39918), 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 39949*	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 39947 on the partition side. (Contributed by Peter Mazsa, 25-Feb-2026.)
⊢ PetErs = ((( Rels × CoMembErs ) ∩ {⟨𝑟, 𝑛⟩ ∣ ≀ (𝑟 ⋉ (◡ E ↾ 𝑛)) ∈ EqvRels }) ∩ {⟨𝑟, 𝑛⟩ ∣ (dom ≀ (𝑟 ⋉ (◡ E ↾ 𝑛)) / ≀ (𝑟 ⋉ (◡ E ↾ 𝑛))) = 𝑛})
Theorem	typesafepets 39950	Type-safe pets 39941 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 39941: 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 39951), in complete parallel with the membership bridge mpets 39931. This theorem is intentionally not the definition of PetParts; it is the bridge used by petseq 39951 after typedness is enforced by the "Pet*" definitions. (Contributed by Peter Mazsa, 19-Feb-2026.)
⊢ ((𝐴 ∈ MembParts ∧ 𝑅 ∈ 𝑉) → ((𝑅 ⋉ (◡ E ↾ 𝐴)) Parts 𝐴 ↔ ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) Ers 𝐴))
Theorem	petseq 39951	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 39931 plays for carriers: mpets 39931 identifies MembParts with CoMembErs at the membership-carrier level, while petseq 39951 identifies the corresponding span-level predicates built from Parts and Ers. Unlike the earlier broad pets 39941, the bridge used here is the type-safe span theorem typesafepets 39950, 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 39952	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 39953	Lemma for prter3 39982. (Contributed by Rodolfo Medina, 9-Oct-2010.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜓 → (𝜃 → 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏)))
Theorem	bicomdd 39954	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 39955	Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 17-Oct-2010.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜓 → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜃 ∧ 𝜒)))
Theorem	jca3 39956	Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 14-Oct-2010.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜃 → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜃 → (𝜒 ∧ 𝜏))))
Theorem	prtlem70 39957	Lemma for prter3 39982: a rearrangement of conjuncts. (Contributed by Rodolfo Medina, 20-Oct-2010.)
⊢ ((((𝜓 ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜑) ↔ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ (𝜃 ∧ 𝜏)))) ∧ 𝜂))
Theorem	ibdr 39958	Reverse of ibd 272. (Contributed by Rodolfo Medina, 30-Sep-2010.)
⊢ (𝜑 → (𝜒 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (𝜒 → 𝜓))
Theorem	prtlem100 39959	Lemma for prter3 39982. (Contributed by Rodolfo Medina, 19-Oct-2010.)
⊢ (∃𝑥 ∈ 𝐴 (𝐵 ∈ 𝑥 ∧ 𝜑) ↔ ∃𝑥 ∈ (𝐴 ∖ {∅})(𝐵 ∈ 𝑥 ∧ 𝜑))
Theorem	prtlem5 39960*	Lemma for prter1 39979, prter2 39981, prter3 39982 and prtex 39980. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
⊢ ([𝑠 / 𝑣][𝑟 / 𝑢]∃𝑥 ∈ 𝐴 (𝑢 ∈ 𝑥 ∧ 𝑣 ∈ 𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝑟 ∈ 𝑥 ∧ 𝑠 ∈ 𝑥))
Theorem	prtlem80 39961	Lemma for prter2 39981. (Contributed by Rodolfo Medina, 17-Oct-2010.)
⊢ (𝐴 ∈ 𝐵 → ¬ 𝐴 ∈ (𝐶 ∖ {𝐴}))
Theorem	brabsb2 39962*	A closed form of brabsb 5504. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ (𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑} → (𝑧𝑅𝑤 ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑))
Theorem	eqbrrdv2 39963*	Other version of eqbrrdiv 5769. (Contributed by Rodolfo Medina, 30-Sep-2010.)
⊢ (((Rel 𝐴 ∧ Rel 𝐵) ∧ 𝜑) → (𝑥𝐴𝑦 ↔ 𝑥𝐵𝑦))    ⇒   ⊢ (((Rel 𝐴 ∧ Rel 𝐵) ∧ 𝜑) → 𝐴 = 𝐵)
Theorem	prtlem9 39964*	Lemma for prter3 39982. (Contributed by Rodolfo Medina, 25-Sep-2010.)
⊢ (𝐴 ∈ 𝐵 → ∃𝑥 ∈ 𝐵 [𝑥] ∼ = [𝐴] ∼ )
Theorem	prtlem10 39965*	Lemma for prter3 39982. (Contributed by Rodolfo Medina, 14-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ( ∼ Er 𝐴 → (𝑧 ∈ 𝐴 → (𝑧 ∼ 𝑤 ↔ ∃𝑣 ∈ 𝐴 (𝑧 ∈ [𝑣] ∼ ∧ 𝑤 ∈ [𝑣] ∼ ))))
Theorem	prtlem11 39966	Lemma for prter2 39981. (Contributed by Rodolfo Medina, 12-Oct-2010.)
⊢ (𝐵 ∈ 𝐷 → (𝐶 ∈ 𝐴 → (𝐵 = [𝐶] ∼ → 𝐵 ∈ (𝐴 / ∼ ))))
Theorem	prtlem12 39967*	Lemma for prtex 39980 and prter3 39982. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ ( ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} → Rel ∼ )
Theorem	prtlem13 39968*	Lemma for prter1 39979, prter2 39981, prter3 39982 and prtex 39980. (Contributed by Rodolfo Medina, 13-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ (𝑧 ∼ 𝑤 ↔ ∃𝑣 ∈ 𝐴 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))
Theorem	prtlem16 39969*	Lemma for prtex 39980, prter2 39981 and prter3 39982. (Contributed by Rodolfo Medina, 14-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ dom ∼ = ∪ 𝐴
Theorem	prtlem400 39970*	Lemma for prter2 39981 and also a property of partitions . (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ ¬ ∅ ∈ (∪ 𝐴 / ∼ )
Syntax	wprt 39971	Extend the definition of a wff to include the partition predicate.
wff Prt 𝐴
Definition	df-prt 39972*	Define the partition predicate. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ (Prt 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅))
Theorem	erprt 39973	The quotient set of an equivalence relation is a partition. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ ( ∼ Er 𝑋 → Prt (𝐴 / ∼ ))
Theorem	prtlem14 39974*	Lemma for prter1 39979, prter2 39981 and prtex 39980. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ (Prt 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑤 ∈ 𝑥 ∧ 𝑤 ∈ 𝑦) → 𝑥 = 𝑦)))
Theorem	prtlem15 39975*	Lemma for prter1 39979 and prtex 39980. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ (Prt 𝐴 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑢 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) ∧ (𝑤 ∈ 𝑦 ∧ 𝑣 ∈ 𝑦)) → ∃𝑧 ∈ 𝐴 (𝑢 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧)))
Theorem	prtlem17 39976*	Lemma for prter2 39981. (Contributed by Rodolfo Medina, 15-Oct-2010.)
⊢ (Prt 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥) → (∃𝑦 ∈ 𝐴 (𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦) → 𝑤 ∈ 𝑥)))
Theorem	prtlem18 39977*	Lemma for prter2 39981. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ (Prt 𝐴 → ((𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣) → (𝑤 ∈ 𝑣 ↔ 𝑧 ∼ 𝑤)))
Theorem	prtlem19 39978*	Lemma for prter2 39981. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ (Prt 𝐴 → ((𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣) → 𝑣 = [𝑧] ∼ ))
Theorem	prter1 39979*	Every partition generates an equivalence relation. (Contributed by Rodolfo Medina, 13-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ (Prt 𝐴 → ∼ Er ∪ 𝐴)
Theorem	prtex 39980*	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 39981*	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 39982*	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 2219, axc7 2347, axc10 2414, axc11 2459, axc11n 2455, axc15 2451, axc9 2411, axc14 2492, and axc16 2295.
Axiom	ax-c5 39983	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 1827. Conditional forms of the converse are given by ax-13 2401, ax-c14 39991, ax-c16 39992, and ax-5 1942. 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 2104). An interesting alternate axiomatization uses axc5c711 40018 and ax-c4 39984 in place of ax-c5 39983, ax-4 1841, ax-10 2177, and ax-11 2193. This axiom is obsolete and should no longer be used. It is proved above as Theorem sp 2219. (Contributed by NM, 3-Jan-1993.) Use sp 2219 instead. (New usage is discouraged.)
⊢ (∀𝑥𝜑 → 𝜑)
Axiom	ax-c4 39984	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 2351. (Contributed by NM, 3-Jan-1993.) (New usage is discouraged.)
⊢ (∀𝑥(∀𝑥𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
Axiom	ax-c7 39985	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 40018 in place of ax-c5 39983, ax-c7 39985, and ax-11 2193. This axiom is obsolete and should no longer be used. It is proved above as Theorem axc7 2347. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑)
Axiom	ax-c10 39986	A variant of ax6 2413. 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 2414. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.)
⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) → 𝜑)
Axiom	ax-c11 39987	Axiom ax-c11 39987 was the original version of ax-c11n 39988 ("n" for "new"), before it was discovered (in May 2008) that the shorter ax-c11n 39988 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 2459. (Contributed by NM, 10-May-1993.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑))
Axiom	ax-c11n 39988	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 39987 and was replaced with this shorter ax-c11n 39988 ("n" for "new") in May 2008. The old axiom is proved from this one as Theorem axc11 2459. Conversely, this axiom is proved from ax-c11 39987 as Theorem axc11nfromc11 40026. This axiom was proved redundant in July 2015. See Theorem axc11n 2455. This axiom is obsolete and should no longer be used. It is proved above as Theorem axc11n 2455. (Contributed by NM, 16-May-2008.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Axiom	ax-c15 39989	Axiom ax-c15 39989 was the original version of ax-12 2212, before it was discovered (in Jan. 2007) that the shorter ax-12 2212 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 39989 (from which the ax-12 2212 instance follows by Theorem ax12 2452.) The proof is by induction on formula length, using ax12eq 40041 and ax12el 40042 for the basis steps and ax12indn 40043, ax12indi 40044, and ax12inda 40048 for the induction steps. (This paragraph is true provided we use ax-c11 39987 in place of ax-c11n 39988.) This axiom is obsolete and should no longer be used. It is proved above as Theorem axc15 2451, which should be used instead. (Contributed by NM, 14-May-1993.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))
Axiom	ax-c9 39990	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 2411. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.)
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
Axiom	ax-c14 39991	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 1942; see Theorem axc14 2492. Alternately, ax-5 1942 becomes unnecessary in principle with this axiom, but we lose the more powerful metalogic afforded by ax-5 1942. We retain ax-c14 39991 here to provide completeness for systems with the simpler metalogic that results from omitting ax-5 1942, 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 2492. (Contributed by NM, 24-Jun-1993.) (New usage is discouraged.)
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦)))
Axiom	ax-c16 39992*	Axiom of Distinct Variables. The only axiom of predicate calculus requiring that variables be distinct (if we consider ax-5 1942 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 5404), but nonetheless it is technically necessary as you can see from its uses. This axiom is redundant if we include ax-5 1942; see Theorem axc16 2295. Alternately, ax-5 1942 becomes logically redundant in the presence of this axiom, but without ax-5 1942 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 39992 here to provide logical completeness for systems with the simpler metalogic that results from omitting ax-5 1942, 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 2295. (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 40005 and ax13fromc9 40006 require some intermediate theorems that are included in this section.
Theorem	axc5 39993	This theorem repeats sp 2219 under the name axc5 39993, so that the Metamath program "MM> VERIFY MARKUP" command will check that it matches axiom scheme ax-c5 39983. (Contributed by NM, 18-Aug-2017.) (Proof modification is discouraged.) Use sp 2219 instead. (New usage is discouraged.)
⊢ (∀𝑥𝜑 → 𝜑)
Theorem	ax4fromc4 39994	Rederivation of Axiom ax-4 1841 from ax-c4 39984, ax-c5 39983, ax-gen 1827 and minimal implicational calculus { ax-mp 5, ax-1 6, ax-2 7 }. See axc4 2351 for the derivation of ax-c4 39984 from ax-4 1841. (Contributed by NM, 23-May-2008.) (Proof modification is discouraged.) Use ax-4 1841 instead. (New usage is discouraged.)
⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
Theorem	ax10fromc7 39995	Rederivation of Axiom ax-10 2177 from ax-c7 39985, ax-c4 39984, ax-c5 39983, ax-gen 1827 and propositional calculus. See axc7 2347 for the derivation of ax-c7 39985 from ax-10 2177. (Contributed by NM, 23-May-2008.) (Proof modification is discouraged.) Use ax-10 2177 instead. (New usage is discouraged.)
⊢ (¬ ∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑)
Theorem	ax6fromc10 39996	Rederivation of Axiom ax-6 1999 from ax-c7 39985, ax-c10 39986, ax-gen 1827 and propositional calculus. See axc10 2414 for the derivation of ax-c10 39986 from ax-6 1999. Lemma L18 in [Megill] p. 446 (p. 14 of the preprint). (Contributed by NM, 14-May-1993.) (Proof modification is discouraged.) Use ax-6 1999 instead. (New usage is discouraged.)
⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦
Theorem	hba1-o 39997	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 39998	Inference version of ax-c4 39984. (Contributed by NM, 3-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑥𝜓)
Theorem	equid1 39999	Proof of equid 2044 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 1942; see the proof of equid 2044. See equid1ALT 40025 for an alternate proof. (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑥 = 𝑥
Theorem	equcomi1 40000	Proof of equcomi 2049 from equid1 39999, avoiding use of ax-5 1942 (the only use of ax-5 1942 is via ax7 2048, so using ax-7 2040 instead would remove dependency on ax-5 1942). (Contributed by BJ, 8-Jul-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)