P. 390 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 38901-39000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	detid 38901	The cosets by the identity relation are in equivalence relation if and only if the identity relation is disjoint. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ( Disj I ↔ EqvRel ≀ I )
Theorem	eqvrelcossid 38902	The cosets by the identity class are in equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2024.)
⊢ EqvRel ≀ I
Theorem	detidres 38903	The cosets by the restricted identity relation are in equivalence relation if and only if the restricted identity relation is disjoint. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ( Disj ( I ↾ 𝐴) ↔ EqvRel ≀ ( I ↾ 𝐴))
Theorem	detinidres 38904	The cosets by the intersection with the restricted identity relation are in equivalence relation if and only if the intersection with the restricted identity relation is disjoint. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ( Disj (𝑅 ∩ ( I ↾ 𝐴)) ↔ EqvRel ≀ (𝑅 ∩ ( I ↾ 𝐴)))
Theorem	detxrnidres 38905	The cosets by the range Cartesian product with the restricted identity relation are in equivalence relation if and only if the range Cartesian product with the restricted identity relation is disjoint. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ( Disj (𝑅 ⋉ ( I ↾ 𝐴)) ↔ EqvRel ≀ (𝑅 ⋉ ( I ↾ 𝐴)))
Theorem	disjlem14 38906*	Lemma for disjdmqseq 38913, partim2 38915 and petlem 38920 via disjlem17 38907, (general version of the former prtlem14 38983). (Contributed by Peter Mazsa, 10-Sep-2021.)
⊢ ( Disj 𝑅 → ((𝑥 ∈ dom 𝑅 ∧ 𝑦 ∈ dom 𝑅) → ((𝐴 ∈ [𝑥]𝑅 ∧ 𝐴 ∈ [𝑦]𝑅) → [𝑥]𝑅 = [𝑦]𝑅)))
Theorem	disjlem17 38907*	Lemma for disjdmqseq 38913, partim2 38915 and petlem 38920 via disjlem18 38908, (general version of the former prtlem17 38985). (Contributed by Peter Mazsa, 10-Sep-2021.)
⊢ ( Disj 𝑅 → ((𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [𝑥]𝑅) → (∃𝑦 ∈ dom 𝑅(𝐴 ∈ [𝑦]𝑅 ∧ 𝐵 ∈ [𝑦]𝑅) → 𝐵 ∈ [𝑥]𝑅)))
Theorem	disjlem18 38908*	Lemma for disjdmqseq 38913, partim2 38915 and petlem 38920 via disjlem19 38909, (general version of the former prtlem18 38986). (Contributed by Peter Mazsa, 16-Sep-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ( Disj 𝑅 → ((𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [𝑥]𝑅) → (𝐵 ∈ [𝑥]𝑅 ↔ 𝐴 ≀ 𝑅𝐵))))
Theorem	disjlem19 38909*	Lemma for disjdmqseq 38913, partim2 38915 and petlem 38920 via disjdmqs 38912, (general version of the former prtlem19 38987). (Contributed by Peter Mazsa, 16-Sep-2021.)
⊢ (𝐴 ∈ 𝑉 → ( Disj 𝑅 → ((𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [𝑥]𝑅) → [𝑥]𝑅 = [𝐴] ≀ 𝑅)))
Theorem	disjdmqsss 38910	Lemma for disjdmqseq 38913 via disjdmqs 38912. (Contributed by Peter Mazsa, 16-Sep-2021.)
⊢ ( Disj 𝑅 → (dom 𝑅 / 𝑅) ⊆ (dom ≀ 𝑅 / ≀ 𝑅))
Theorem	disjdmqscossss 38911	Lemma for disjdmqseq 38913 via disjdmqs 38912. (Contributed by Peter Mazsa, 16-Sep-2021.)
⊢ ( Disj 𝑅 → (dom ≀ 𝑅 / ≀ 𝑅) ⊆ (dom 𝑅 / 𝑅))
Theorem	disjdmqs 38912	If a relation is disjoint, its domain quotient is equal to the domain quotient of the cosets by it. Lemma for partim2 38915 and petlem 38920 via disjdmqseq 38913. (Contributed by Peter Mazsa, 16-Sep-2021.)
⊢ ( Disj 𝑅 → (dom 𝑅 / 𝑅) = (dom ≀ 𝑅 / ≀ 𝑅))
Theorem	disjdmqseq 38913	If a relation is disjoint, its domain quotient is equal to a class if and only if the domain quotient of the cosets by it is equal to the class. General version of eldisjn0el 38914 (which is the closest theorem to the former prter2 38990). Lemma for partim2 38915 and petlem 38920. (Contributed by Peter Mazsa, 16-Sep-2021.)
⊢ ( Disj 𝑅 → ((dom 𝑅 / 𝑅) = 𝐴 ↔ (dom ≀ 𝑅 / ≀ 𝑅) = 𝐴))
Theorem	eldisjn0el 38914	Special case of disjdmqseq 38913 (perhaps this is the closest theorem to the former prter2 38990). (Contributed by Peter Mazsa, 26-Sep-2021.)
⊢ ( ElDisj 𝐴 → (¬ ∅ ∈ 𝐴 ↔ (∪ 𝐴 / ∼ 𝐴) = 𝐴))
Theorem	partim2 38915	Disjoint relation on its natural domain implies an equivalence relation on the cosets of the relation, on its natural domain, cf. partim 38916. Lemma for petlem 38920. (Contributed by Peter Mazsa, 17-Sep-2021.)
⊢ (( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) → ( EqvRel ≀ 𝑅 ∧ (dom ≀ 𝑅 / ≀ 𝑅) = 𝐴))
Theorem	partim 38916	Partition implies equivalence relation by the cosets of the relation on its natural domain, cf. partim2 38915. (Contributed by Peter Mazsa, 17-Sep-2021.)
⊢ (𝑅 Part 𝐴 → ≀ 𝑅 ErALTV 𝐴)
Theorem	partimeq 38917	Partition implies that the class of coelements on the natural domain is equal to the class of cosets of the relation, cf. erimeq 38787. (Contributed by Peter Mazsa, 25-Dec-2024.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 Part 𝐴 → ∼ 𝐴 = ≀ 𝑅))
Theorem	eldisjlem19 38918*	Special case of disjlem19 38909 (together with membpartlem19 38919, this is former prtlem19 38987). (Contributed by Peter Mazsa, 21-Oct-2021.)
⊢ (𝐵 ∈ 𝑉 → ( ElDisj 𝐴 → ((𝑢 ∈ dom (◡ E ↾ 𝐴) ∧ 𝐵 ∈ 𝑢) → 𝑢 = [𝐵] ∼ 𝐴)))
Theorem	membpartlem19 38919*	Together with disjlem19 38909, this is former prtlem19 38987. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by Peter Mazsa, 21-Oct-2021.)
⊢ (𝐵 ∈ 𝑉 → ( MembPart 𝐴 → ((𝑢 ∈ 𝐴 ∧ 𝐵 ∈ 𝑢) → 𝑢 = [𝐵] ∼ 𝐴)))
Theorem	petlem 38920	If you can prove that the equivalence of cosets on their natural domain implies disjointness (e.g. eqvrelqseqdisj5 38941), or converse function (cf. dfdisjALTV 38821), then disjointness, and equivalence of cosets, both on their natural domain, are equivalent. Lemma for the Partition Equivalence Theorem pet2 38958. (Contributed by Peter Mazsa, 18-Sep-2021.)
⊢ (( EqvRel ≀ 𝑅 ∧ (dom ≀ 𝑅 / ≀ 𝑅) = 𝐴) → Disj 𝑅)    ⇒   ⊢ (( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ↔ ( EqvRel ≀ 𝑅 ∧ (dom ≀ 𝑅 / ≀ 𝑅) = 𝐴))
Theorem	petlemi 38921	If you can prove disjointness (e.g. disjALTV0 38862, disjALTVid 38863, disjALTVidres 38864, disjALTVxrnidres 38866, search for theorems containing the ' |- Disj ' string), or the same with converse function (cf. dfdisjALTV 38821), then disjointness, and equivalence of cosets, both on their natural domain, are equivalent. (Contributed by Peter Mazsa, 18-Sep-2021.)
⊢ Disj 𝑅    ⇒   ⊢ (( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ↔ ( EqvRel ≀ 𝑅 ∧ (dom ≀ 𝑅 / ≀ 𝑅) = 𝐴))
Theorem	pet02 38922	Class 𝐴 is a partition by the null class if and only if the cosets by the null class are in equivalence relation on it. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ (( Disj ∅ ∧ (dom ∅ / ∅) = 𝐴) ↔ ( EqvRel ≀ ∅ ∧ (dom ≀ ∅ / ≀ ∅) = 𝐴))
Theorem	pet0 38923	Class 𝐴 is a partition by the null class if and only if the cosets by the null class are in equivalence relation on it. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ (∅ Part 𝐴 ↔ ≀ ∅ ErALTV 𝐴)
Theorem	petid2 38924	Class 𝐴 is a partition by the identity class if and only if the cosets by the identity class are in equivalence relation on it. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ (( Disj I ∧ (dom I / I ) = 𝐴) ↔ ( EqvRel ≀ I ∧ (dom ≀ I / ≀ I ) = 𝐴))
Theorem	petid 38925	A class is a partition by the identity class if and only if the cosets by the identity class are in equivalence relation on it. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ( I Part 𝐴 ↔ ≀ I ErALTV 𝐴)
Theorem	petidres2 38926	Class 𝐴 is a partition by the identity class restricted to it if and only if the cosets by the restricted identity class are in equivalence relation on it. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ (( Disj ( I ↾ 𝐴) ∧ (dom ( I ↾ 𝐴) / ( I ↾ 𝐴)) = 𝐴) ↔ ( EqvRel ≀ ( I ↾ 𝐴) ∧ (dom ≀ ( I ↾ 𝐴) / ≀ ( I ↾ 𝐴)) = 𝐴))
Theorem	petidres 38927	A class is a partition by identity class restricted to it if and only if the cosets by the restricted identity class are in equivalence relation on it, cf. eqvrel1cossidres 38898. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ (( I ↾ 𝐴) Part 𝐴 ↔ ≀ ( I ↾ 𝐴) ErALTV 𝐴)
Theorem	petinidres2 38928	Class 𝐴 is a partition by an intersection with the identity class restricted to it if and only if the cosets by the intersection are in equivalence relation on it. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ (( Disj (𝑅 ∩ ( I ↾ 𝐴)) ∧ (dom (𝑅 ∩ ( I ↾ 𝐴)) / (𝑅 ∩ ( I ↾ 𝐴))) = 𝐴) ↔ ( EqvRel ≀ (𝑅 ∩ ( I ↾ 𝐴)) ∧ (dom ≀ (𝑅 ∩ ( I ↾ 𝐴)) / ≀ (𝑅 ∩ ( I ↾ 𝐴))) = 𝐴))
Theorem	petinidres 38929	A class is a partition by an intersection with the identity class restricted to it if and only if the cosets by the intersection are in equivalence relation on it. Cf. br1cossinidres 38561, disjALTVinidres 38865 and eqvrel1cossinidres 38899. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ((𝑅 ∩ ( I ↾ 𝐴)) Part 𝐴 ↔ ≀ (𝑅 ∩ ( I ↾ 𝐴)) ErALTV 𝐴)
Theorem	petxrnidres2 38930	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. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ (( Disj (𝑅 ⋉ ( I ↾ 𝐴)) ∧ (dom (𝑅 ⋉ ( I ↾ 𝐴)) / (𝑅 ⋉ ( I ↾ 𝐴))) = 𝐴) ↔ ( EqvRel ≀ (𝑅 ⋉ ( I ↾ 𝐴)) ∧ (dom ≀ (𝑅 ⋉ ( I ↾ 𝐴)) / ≀ (𝑅 ⋉ ( I ↾ 𝐴))) = 𝐴))
Theorem	petxrnidres 38931	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 38563, disjALTVxrnidres 38866 and eqvrel1cossxrnidres 38900. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ((𝑅 ⋉ ( I ↾ 𝐴)) Part 𝐴 ↔ ≀ (𝑅 ⋉ ( I ↾ 𝐴)) ErALTV 𝐴)
Theorem	eqvreldisj1 38932*	The elements of the quotient set of an equivalence relation are disjoint (cf. eqvreldisj2 38933, eqvreldisj3 38934). (Contributed by Mario Carneiro, 10-Dec-2016.) (Revised by Peter Mazsa, 3-Dec-2024.)
⊢ ( EqvRel 𝑅 → ∀𝑥 ∈ (𝐴 / 𝑅)∀𝑦 ∈ (𝐴 / 𝑅)(𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅))
Theorem	eqvreldisj2 38933	The elements of the quotient set of an equivalence relation are disjoint (cf. eqvreldisj3 38934). (Contributed by Mario Carneiro, 10-Dec-2016.) (Revised by Peter Mazsa, 19-Sep-2021.)
⊢ ( EqvRel 𝑅 → ElDisj (𝐴 / 𝑅))
Theorem	eqvreldisj3 38934	The elements of the quotient set of an equivalence relation are disjoint (cf. qsdisj2 8728). (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 38935	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 38936	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 38937	Implication of eqvreldisj2 38933, lemma for The Main Theorem of Equivalences mainer 38942. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ (( EqvRel 𝑅 ∧ (𝐵 / 𝑅) = 𝐴) → ElDisj 𝐴)
Theorem	fences3 38938	Implication of eqvrelqseqdisj2 38937 and n0eldmqseq 38757, see comment of fences 38952. (Contributed by Peter Mazsa, 30-Dec-2024.)
⊢ (( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) → ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴))
Theorem	eqvrelqseqdisj3 38939	Implication of eqvreldisj3 38934, lemma for the Member Partition Equivalence Theorem mpet3 38944. (Contributed by Peter Mazsa, 27-Oct-2020.) (Revised by Peter Mazsa, 24-Sep-2021.)
⊢ (( EqvRel 𝑅 ∧ (𝐵 / 𝑅) = 𝐴) → Disj (◡ E ↾ 𝐴))
Theorem	eqvrelqseqdisj4 38940	Lemma for petincnvepres2 38956. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ (( EqvRel 𝑅 ∧ (𝐵 / 𝑅) = 𝐴) → Disj (𝑆 ∩ (◡ E ↾ 𝐴)))
Theorem	eqvrelqseqdisj5 38941	Lemma for the Partition-Equivalence Theorem pet2 38958. (Contributed by Peter Mazsa, 15-Jul-2020.) (Revised by Peter Mazsa, 22-Sep-2021.)
⊢ (( EqvRel 𝑅 ∧ (𝐵 / 𝑅) = 𝐴) → Disj (𝑆 ⋉ (◡ E ↾ 𝐴)))
Theorem	mainer 38942	The Main Theorem of Equivalences: every equivalence relation implies equivalent comembers. (Contributed by Peter Mazsa, 26-Sep-2021.)
⊢ (𝑅 ErALTV 𝐴 → CoMembEr 𝐴)
Theorem	partimcomember 38943	Partition with general 𝑅 (in addition to the member partition cf. mpet 38947 and mpet2 38948) implies equivalent comembers. (Contributed by Peter Mazsa, 23-Sep-2021.) (Revised by Peter Mazsa, 22-Dec-2024.)
⊢ (𝑅 Part 𝐴 → CoMembEr 𝐴)
Theorem	mpet3 38944	Member Partition-Equivalence Theorem. Together with mpet 38947 mpet2 38948, mostly in its conventional cpet 38946 and cpet2 38945 form, this is what we used to think of as the partition equivalence theorem (but cf. pet2 38958 with general 𝑅). (Contributed by Peter Mazsa, 4-May-2018.) (Revised by Peter Mazsa, 26-Sep-2021.)
⊢ (( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴) ↔ ( CoElEqvRel 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴))
Theorem	cpet2 38945	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 38946. Together with cpet 38946, mpet 38947 mpet2 38948, this is what we used to think of as the partition equivalence theorem (but cf. pet2 38958 with general 𝑅). (Contributed by Peter Mazsa, 30-Dec-2024.)
⊢ (( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴) ↔ ( EqvRel ∼ 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴))
Theorem	cpet 38946	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 38945. Cf. mpet 38947, mpet2 38948 and mpet3 38944 for unconventional forms of Member Partition-Equivalence Theorem. Cf. pet 38959 and pet2 38958 for Partition-Equivalence Theorem with general 𝑅. (Contributed by Peter Mazsa, 31-Dec-2024.)
⊢ ( MembPart 𝐴 ↔ ( EqvRel ∼ 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴))
Theorem	mpet 38947	Member Partition-Equivalence Theorem in almost its shortest possible form, cf. the 0-ary version mpets 38950. 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 38948, mpet3 38944, and with the conventional cpet 38946 and cpet2 38945, this is what we used to think of as the partition equivalence theorem (but cf. pet2 38958 with general 𝑅). (Contributed by Peter Mazsa, 24-Sep-2021.)
⊢ ( MembPart 𝐴 ↔ CoMembEr 𝐴)
Theorem	mpet2 38948	Member Partition-Equivalence Theorem in a shorter form. Together with mpet 38947 mpet3 38944, mostly in its conventional cpet 38946 and cpet2 38945 form, this is what we used to think of as the partition equivalence theorem (but cf. pet2 38958 with general 𝑅). (Contributed by Peter Mazsa, 24-Sep-2021.)
⊢ ((◡ E ↾ 𝐴) Part 𝐴 ↔ ≀ (◡ E ↾ 𝐴) ErALTV 𝐴)
Theorem	mpets2 38949	Member Partition-Equivalence Theorem with binary relations, cf. mpet2 38948. (Contributed by Peter Mazsa, 24-Sep-2021.)
⊢ (𝐴 ∈ 𝑉 → ((◡ E ↾ 𝐴) Parts 𝐴 ↔ ≀ (◡ E ↾ 𝐴) Ers 𝐴))
Theorem	mpets 38950	Member Partition-Equivalence Theorem in its shortest possible form: it shows that member partitions and comember equivalence relations are literally the same. Cf. pet 38959, the Partition-Equivalence Theorem, with general 𝑅. (Contributed by Peter Mazsa, 31-Dec-2024.)
⊢ MembParts = CoMembErs
Theorem	mainpart 38951	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 38952	The Theorem of Fences by Equivalences: all conceivable equivalence relations (besides the comember equivalence relation cf. mpet 38947) generate a partition of the members. (Contributed by Peter Mazsa, 26-Sep-2021.)
⊢ (𝑅 ErALTV 𝐴 → MembPart 𝐴)
Theorem	fences2 38953	The Theorem of Fences by Equivalences: all conceivable equivalence relations (besides the comember equivalence relation cf. mpet3 38944) 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 38954	The Main Theorem of Equivalences: every equivalence relation implies equivalent comembers. (Contributed by Peter Mazsa, 15-Oct-2021.)
⊢ (𝑅 ErALTV 𝐴 → ( CoElEqvRel 𝐴 ∧ ¬ ∅ ∈ 𝐴))
Theorem	mainerim 38955	Every equivalence relation implies equivalent coelements. (Contributed by Peter Mazsa, 20-Oct-2021.)
⊢ (𝑅 ErALTV 𝐴 → CoElEqvRel 𝐴)
Theorem	petincnvepres2 38956	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 38957	The shortest form of a partition-equivalence theorem with intersection and general 𝑅. Cf. br1cossincnvepres 38562. Cf. pet 38959. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ ((𝑅 ∩ (◡ E ↾ 𝐴)) Part 𝐴 ↔ ≀ (𝑅 ∩ (◡ E ↾ 𝐴)) ErALTV 𝐴)
Theorem	pet2 38958	Partition-Equivalence Theorem, with general 𝑅. This theorem (together with pet 38959 and pets 38960) is the main result of my investigation into set theory, see the comment of pet 38959. (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 38959	Partition-Equivalence Theorem with general 𝑅 while preserving the restricted converse epsilon relation of mpet2 38948 (as opposed to petincnvepres 38957). 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 38564. This theorem (together with pets 38960 and pet2 38958) is the main result of my investigation into set theory. It is no more general than the conventional Member Partition-Equivalence Theorem mpet 38947, mpet2 38948 and mpet3 38944 (because you cannot set 𝑅 in this theorem in such a way that you get mpet2 38948), i.e., it is not the hypothetical General Partition-Equivalence Theorem gpet ⊢ (𝑅 Part 𝐴 ↔ ≀ 𝑅 ErALTV 𝐴), but this one has a general part that mpet2 38948 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 38960	Partition-Equivalence Theorem with general 𝑅, with binary relations. This theorem (together with pet 38959 and pet2 38958) is the main result of my investigation into set theory, cf. the comment of pet 38959. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → ((𝑅 ⋉ (◡ E ↾ 𝐴)) Parts 𝐴 ↔ ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) Ers 𝐴))
Theorem	dmqsblocks 38961*	If the pet 38959 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 38756). It makes explicit that pet 38959 gives active representatives for each block, without ever forcing 𝑣 = 𝑢. (Contributed by Peter Mazsa, 23-Nov-2025.)
⊢ ((dom (𝑅 ⋉ (◡ E ↾ 𝐴)) / (𝑅 ⋉ (◡ E ↾ 𝐴))) = 𝐴 → ∀𝑢 ∈ 𝐴 ∃𝑣 ∈ dom (𝑅 ⋉ (◡ E ↾ 𝐴))∃𝑏∃𝑐(𝑢 = [𝑣](𝑅 ⋉ (◡ E ↾ 𝐴)) ∧ 𝑐 ∈ 𝑣 ∧ 𝑣𝑅𝑏))
21.27  Mathbox for Rodolfo Medina
21.27.1  Partitions
Theorem	prtlem60 38962	Lemma for prter3 38991. (Contributed by Rodolfo Medina, 9-Oct-2010.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜓 → (𝜃 → 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏)))
Theorem	bicomdd 38963	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 38964	Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 17-Oct-2010.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜓 → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜃 ∧ 𝜒)))
Theorem	jca3 38965	Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 14-Oct-2010.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜃 → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜃 → (𝜒 ∧ 𝜏))))
Theorem	prtlem70 38966	Lemma for prter3 38991: a rearrangement of conjuncts. (Contributed by Rodolfo Medina, 20-Oct-2010.)
⊢ ((((𝜓 ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜑) ↔ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ (𝜃 ∧ 𝜏)))) ∧ 𝜂))
Theorem	ibdr 38967	Reverse of ibd 269. (Contributed by Rodolfo Medina, 30-Sep-2010.)
⊢ (𝜑 → (𝜒 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (𝜒 → 𝜓))
Theorem	prtlem100 38968	Lemma for prter3 38991. (Contributed by Rodolfo Medina, 19-Oct-2010.)
⊢ (∃𝑥 ∈ 𝐴 (𝐵 ∈ 𝑥 ∧ 𝜑) ↔ ∃𝑥 ∈ (𝐴 ∖ {∅})(𝐵 ∈ 𝑥 ∧ 𝜑))
Theorem	prtlem5 38969*	Lemma for prter1 38988, prter2 38990, prter3 38991 and prtex 38989. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
⊢ ([𝑠 / 𝑣][𝑟 / 𝑢]∃𝑥 ∈ 𝐴 (𝑢 ∈ 𝑥 ∧ 𝑣 ∈ 𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝑟 ∈ 𝑥 ∧ 𝑠 ∈ 𝑥))
Theorem	prtlem80 38970	Lemma for prter2 38990. (Contributed by Rodolfo Medina, 17-Oct-2010.)
⊢ (𝐴 ∈ 𝐵 → ¬ 𝐴 ∈ (𝐶 ∖ {𝐴}))
Theorem	brabsb2 38971*	A closed form of brabsb 5476. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ (𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑} → (𝑧𝑅𝑤 ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑))
Theorem	eqbrrdv2 38972*	Other version of eqbrrdiv 5740. (Contributed by Rodolfo Medina, 30-Sep-2010.)
⊢ (((Rel 𝐴 ∧ Rel 𝐵) ∧ 𝜑) → (𝑥𝐴𝑦 ↔ 𝑥𝐵𝑦))    ⇒   ⊢ (((Rel 𝐴 ∧ Rel 𝐵) ∧ 𝜑) → 𝐴 = 𝐵)
Theorem	prtlem9 38973*	Lemma for prter3 38991. (Contributed by Rodolfo Medina, 25-Sep-2010.)
⊢ (𝐴 ∈ 𝐵 → ∃𝑥 ∈ 𝐵 [𝑥] ∼ = [𝐴] ∼ )
Theorem	prtlem10 38974*	Lemma for prter3 38991. (Contributed by Rodolfo Medina, 14-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ( ∼ Er 𝐴 → (𝑧 ∈ 𝐴 → (𝑧 ∼ 𝑤 ↔ ∃𝑣 ∈ 𝐴 (𝑧 ∈ [𝑣] ∼ ∧ 𝑤 ∈ [𝑣] ∼ ))))
Theorem	prtlem11 38975	Lemma for prter2 38990. (Contributed by Rodolfo Medina, 12-Oct-2010.)
⊢ (𝐵 ∈ 𝐷 → (𝐶 ∈ 𝐴 → (𝐵 = [𝐶] ∼ → 𝐵 ∈ (𝐴 / ∼ ))))
Theorem	prtlem12 38976*	Lemma for prtex 38989 and prter3 38991. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ ( ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} → Rel ∼ )
Theorem	prtlem13 38977*	Lemma for prter1 38988, prter2 38990, prter3 38991 and prtex 38989. (Contributed by Rodolfo Medina, 13-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ (𝑧 ∼ 𝑤 ↔ ∃𝑣 ∈ 𝐴 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))
Theorem	prtlem16 38978*	Lemma for prtex 38989, prter2 38990 and prter3 38991. (Contributed by Rodolfo Medina, 14-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ dom ∼ = ∪ 𝐴
Theorem	prtlem400 38979*	Lemma for prter2 38990 and also a property of partitions . (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ ¬ ∅ ∈ (∪ 𝐴 / ∼ )
Syntax	wprt 38980	Extend the definition of a wff to include the partition predicate.
wff Prt 𝐴
Definition	df-prt 38981*	Define the partition predicate. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ (Prt 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅))
Theorem	erprt 38982	The quotient set of an equivalence relation is a partition. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ ( ∼ Er 𝑋 → Prt (𝐴 / ∼ ))
Theorem	prtlem14 38983*	Lemma for prter1 38988, prter2 38990 and prtex 38989. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ (Prt 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑤 ∈ 𝑥 ∧ 𝑤 ∈ 𝑦) → 𝑥 = 𝑦)))
Theorem	prtlem15 38984*	Lemma for prter1 38988 and prtex 38989. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ (Prt 𝐴 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑢 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) ∧ (𝑤 ∈ 𝑦 ∧ 𝑣 ∈ 𝑦)) → ∃𝑧 ∈ 𝐴 (𝑢 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧)))
Theorem	prtlem17 38985*	Lemma for prter2 38990. (Contributed by Rodolfo Medina, 15-Oct-2010.)
⊢ (Prt 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥) → (∃𝑦 ∈ 𝐴 (𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦) → 𝑤 ∈ 𝑥)))
Theorem	prtlem18 38986*	Lemma for prter2 38990. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ (Prt 𝐴 → ((𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣) → (𝑤 ∈ 𝑣 ↔ 𝑧 ∼ 𝑤)))
Theorem	prtlem19 38987*	Lemma for prter2 38990. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ (Prt 𝐴 → ((𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣) → 𝑣 = [𝑧] ∼ ))
Theorem	prter1 38988*	Every partition generates an equivalence relation. (Contributed by Rodolfo Medina, 13-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ (Prt 𝐴 → ∼ Er ∪ 𝐴)
Theorem	prtex 38989*	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 38990*	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 38991*	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.28  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.28.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 2188, axc7 2320, axc10 2387, axc11 2432, axc11n 2428, axc15 2424, axc9 2384, axc14 2465, and axc16 2266.
Axiom	ax-c5 38992	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 1796. Conditional forms of the converse are given by ax-13 2374, ax-c14 39000, ax-c16 39001, and ax-5 1911. 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 2073). An interesting alternate axiomatization uses axc5c711 39027 and ax-c4 38993 in place of ax-c5 38992, ax-4 1810, ax-10 2146, and ax-11 2162. This axiom is obsolete and should no longer be used. It is proved above as Theorem sp 2188. (Contributed by NM, 3-Jan-1993.) Use sp 2188 instead. (New usage is discouraged.)
⊢ (∀𝑥𝜑 → 𝜑)
Axiom	ax-c4 38993	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 2324. (Contributed by NM, 3-Jan-1993.) (New usage is discouraged.)
⊢ (∀𝑥(∀𝑥𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
Axiom	ax-c7 38994	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 39027 in place of ax-c5 38992, ax-c7 38994, and ax-11 2162. This axiom is obsolete and should no longer be used. It is proved above as Theorem axc7 2320. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑)
Axiom	ax-c10 38995	A variant of ax6 2386. 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 2387. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.)
⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) → 𝜑)
Axiom	ax-c11 38996	Axiom ax-c11 38996 was the original version of ax-c11n 38997 ("n" for "new"), before it was discovered (in May 2008) that the shorter ax-c11n 38997 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 2432. (Contributed by NM, 10-May-1993.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑))
Axiom	ax-c11n 38997	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 38996 and was replaced with this shorter ax-c11n 38997 ("n" for "new") in May 2008. The old axiom is proved from this one as Theorem axc11 2432. Conversely, this axiom is proved from ax-c11 38996 as Theorem axc11nfromc11 39035. This axiom was proved redundant in July 2015. See Theorem axc11n 2428. This axiom is obsolete and should no longer be used. It is proved above as Theorem axc11n 2428. (Contributed by NM, 16-May-2008.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Axiom	ax-c15 38998	Axiom ax-c15 38998 was the original version of ax-12 2182, before it was discovered (in Jan. 2007) that the shorter ax-12 2182 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 38998 (from which the ax-12 2182 instance follows by Theorem ax12 2425.) The proof is by induction on formula length, using ax12eq 39050 and ax12el 39051 for the basis steps and ax12indn 39052, ax12indi 39053, and ax12inda 39057 for the induction steps. (This paragraph is true provided we use ax-c11 38996 in place of ax-c11n 38997.) This axiom is obsolete and should no longer be used. It is proved above as Theorem axc15 2424, which should be used instead. (Contributed by NM, 14-May-1993.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))
Axiom	ax-c9 38999	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 2384. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.)
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
Axiom	ax-c14 39000	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 1911; see Theorem axc14 2465. Alternately, ax-5 1911 becomes unnecessary in principle with this axiom, but we lose the more powerful metalogic afforded by ax-5 1911. We retain ax-c14 39000 here to provide completeness for systems with the simpler metalogic that results from omitting ax-5 1911, 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 2465. (Contributed by NM, 24-Jun-1993.) (New usage is discouraged.)
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦)))