P. 389 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 38801-38900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	partimeq 38801	Partition implies that the class of coelements on the natural domain is equal to the class of cosets of the relation, cf. erimeq 38671. (Contributed by Peter Mazsa, 25-Dec-2024.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 Part 𝐴 → ∼ 𝐴 = ≀ 𝑅))
Theorem	eldisjlem19 38802*	Special case of disjlem19 38793 (together with membpartlem19 38803, this is former prtlem19 38871). (Contributed by Peter Mazsa, 21-Oct-2021.)
⊢ (𝐵 ∈ 𝑉 → ( ElDisj 𝐴 → ((𝑢 ∈ dom (◡ E ↾ 𝐴) ∧ 𝐵 ∈ 𝑢) → 𝑢 = [𝐵] ∼ 𝐴)))
Theorem	membpartlem19 38803*	Together with disjlem19 38793, this is former prtlem19 38871. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by Peter Mazsa, 21-Oct-2021.)
⊢ (𝐵 ∈ 𝑉 → ( MembPart 𝐴 → ((𝑢 ∈ 𝐴 ∧ 𝐵 ∈ 𝑢) → 𝑢 = [𝐵] ∼ 𝐴)))
Theorem	petlem 38804	If you can prove that the equivalence of cosets on their natural domain implies disjointness (e.g. eqvrelqseqdisj5 38825), or converse function (cf. dfdisjALTV 38705), then disjointness, and equivalence of cosets, both on their natural domain, are equivalent. Lemma for the Partition Equivalence Theorem pet2 38842. (Contributed by Peter Mazsa, 18-Sep-2021.)
⊢ (( EqvRel ≀ 𝑅 ∧ (dom ≀ 𝑅 / ≀ 𝑅) = 𝐴) → Disj 𝑅)    ⇒   ⊢ (( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ↔ ( EqvRel ≀ 𝑅 ∧ (dom ≀ 𝑅 / ≀ 𝑅) = 𝐴))
Theorem	petlemi 38805	If you can prove disjointness (e.g. disjALTV0 38746, disjALTVid 38747, disjALTVidres 38748, disjALTVxrnidres 38750, search for theorems containing the ' |- Disj ' string), or the same with converse function (cf. dfdisjALTV 38705), 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 38806	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 38807	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 38808	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 38809	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 38810	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 38811	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 38782. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ (( I ↾ 𝐴) Part 𝐴 ↔ ≀ ( I ↾ 𝐴) ErALTV 𝐴)
Theorem	petinidres2 38812	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 38813	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 38440, disjALTVinidres 38749 and eqvrel1cossinidres 38783. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ((𝑅 ∩ ( I ↾ 𝐴)) Part 𝐴 ↔ ≀ (𝑅 ∩ ( I ↾ 𝐴)) ErALTV 𝐴)
Theorem	petxrnidres2 38814	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 38815	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 38442, disjALTVxrnidres 38750 and eqvrel1cossxrnidres 38784. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ ((𝑅 ⋉ ( I ↾ 𝐴)) Part 𝐴 ↔ ≀ (𝑅 ⋉ ( I ↾ 𝐴)) ErALTV 𝐴)
Theorem	eqvreldisj1 38816*	The elements of the quotient set of an equivalence relation are disjoint (cf. eqvreldisj2 38817, eqvreldisj3 38818). (Contributed by Mario Carneiro, 10-Dec-2016.) (Revised by Peter Mazsa, 3-Dec-2024.)
⊢ ( EqvRel 𝑅 → ∀𝑥 ∈ (𝐴 / 𝑅)∀𝑦 ∈ (𝐴 / 𝑅)(𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅))
Theorem	eqvreldisj2 38817	The elements of the quotient set of an equivalence relation are disjoint (cf. eqvreldisj3 38818). (Contributed by Mario Carneiro, 10-Dec-2016.) (Revised by Peter Mazsa, 19-Sep-2021.)
⊢ ( EqvRel 𝑅 → ElDisj (𝐴 / 𝑅))
Theorem	eqvreldisj3 38818	The elements of the quotient set of an equivalence relation are disjoint (cf. qsdisj2 8768). (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 38819	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 38820	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 38821	Implication of eqvreldisj2 38817, lemma for The Main Theorem of Equivalences mainer 38826. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ (( EqvRel 𝑅 ∧ (𝐵 / 𝑅) = 𝐴) → ElDisj 𝐴)
Theorem	fences3 38822	Implication of eqvrelqseqdisj2 38821 and n0eldmqseq 38641, see comment of fences 38836. (Contributed by Peter Mazsa, 30-Dec-2024.)
⊢ (( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) → ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴))
Theorem	eqvrelqseqdisj3 38823	Implication of eqvreldisj3 38818, lemma for the Member Partition Equivalence Theorem mpet3 38828. (Contributed by Peter Mazsa, 27-Oct-2020.) (Revised by Peter Mazsa, 24-Sep-2021.)
⊢ (( EqvRel 𝑅 ∧ (𝐵 / 𝑅) = 𝐴) → Disj (◡ E ↾ 𝐴))
Theorem	eqvrelqseqdisj4 38824	Lemma for petincnvepres2 38840. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ (( EqvRel 𝑅 ∧ (𝐵 / 𝑅) = 𝐴) → Disj (𝑆 ∩ (◡ E ↾ 𝐴)))
Theorem	eqvrelqseqdisj5 38825	Lemma for the Partition-Equivalence Theorem pet2 38842. (Contributed by Peter Mazsa, 15-Jul-2020.) (Revised by Peter Mazsa, 22-Sep-2021.)
⊢ (( EqvRel 𝑅 ∧ (𝐵 / 𝑅) = 𝐴) → Disj (𝑆 ⋉ (◡ E ↾ 𝐴)))
Theorem	mainer 38826	The Main Theorem of Equivalences: every equivalence relation implies equivalent comembers. (Contributed by Peter Mazsa, 26-Sep-2021.)
⊢ (𝑅 ErALTV 𝐴 → CoMembEr 𝐴)
Theorem	partimcomember 38827	Partition with general 𝑅 (in addition to the member partition cf. mpet 38831 and mpet2 38832) implies equivalent comembers. (Contributed by Peter Mazsa, 23-Sep-2021.) (Revised by Peter Mazsa, 22-Dec-2024.)
⊢ (𝑅 Part 𝐴 → CoMembEr 𝐴)
Theorem	mpet3 38828	Member Partition-Equivalence Theorem. Together with mpet 38831 mpet2 38832, mostly in its conventional cpet 38830 and cpet2 38829 form, this is what we used to think of as the partition equivalence theorem (but cf. pet2 38842 with general 𝑅). (Contributed by Peter Mazsa, 4-May-2018.) (Revised by Peter Mazsa, 26-Sep-2021.)
⊢ (( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴) ↔ ( CoElEqvRel 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴))
Theorem	cpet2 38829	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 38830. Together with cpet 38830, mpet 38831 mpet2 38832, this is what we used to think of as the partition equivalence theorem (but cf. pet2 38842 with general 𝑅). (Contributed by Peter Mazsa, 30-Dec-2024.)
⊢ (( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴) ↔ ( EqvRel ∼ 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴))
Theorem	cpet 38830	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 38829. Cf. mpet 38831, mpet2 38832 and mpet3 38828 for unconventional forms of Member Partition-Equivalence Theorem. Cf. pet 38843 and pet2 38842 for Partition-Equivalence Theorem with general 𝑅. (Contributed by Peter Mazsa, 31-Dec-2024.)
⊢ ( MembPart 𝐴 ↔ ( EqvRel ∼ 𝐴 ∧ (∪ 𝐴 / ∼ 𝐴) = 𝐴))
Theorem	mpet 38831	Member Partition-Equivalence Theorem in almost its shortest possible form, cf. the 0-ary version mpets 38834. 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 38832, mpet3 38828, and with the conventional cpet 38830 and cpet2 38829, this is what we used to think of as the partition equivalence theorem (but cf. pet2 38842 with general 𝑅). (Contributed by Peter Mazsa, 24-Sep-2021.)
⊢ ( MembPart 𝐴 ↔ CoMembEr 𝐴)
Theorem	mpet2 38832	Member Partition-Equivalence Theorem in a shorter form. Together with mpet 38831 mpet3 38828, mostly in its conventional cpet 38830 and cpet2 38829 form, this is what we used to think of as the partition equivalence theorem (but cf. pet2 38842 with general 𝑅). (Contributed by Peter Mazsa, 24-Sep-2021.)
⊢ ((◡ E ↾ 𝐴) Part 𝐴 ↔ ≀ (◡ E ↾ 𝐴) ErALTV 𝐴)
Theorem	mpets2 38833	Member Partition-Equivalence Theorem with binary relations, cf. mpet2 38832. (Contributed by Peter Mazsa, 24-Sep-2021.)
⊢ (𝐴 ∈ 𝑉 → ((◡ E ↾ 𝐴) Parts 𝐴 ↔ ≀ (◡ E ↾ 𝐴) Ers 𝐴))
Theorem	mpets 38834	Member Partition-Equivalence Theorem in its shortest possible form: it shows that member partitions and comember equivalence relations are literally the same. Cf. pet 38843, the Partition-Equivalence Theorem, with general 𝑅. (Contributed by Peter Mazsa, 31-Dec-2024.)
⊢ MembParts = CoMembErs
Theorem	mainpart 38835	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 38836	The Theorem of Fences by Equivalences: all conceivable equivalence relations (besides the comember equivalence relation cf. mpet 38831) generate a partition of the members. (Contributed by Peter Mazsa, 26-Sep-2021.)
⊢ (𝑅 ErALTV 𝐴 → MembPart 𝐴)
Theorem	fences2 38837	The Theorem of Fences by Equivalences: all conceivable equivalence relations (besides the comember equivalence relation cf. mpet3 38828) 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 38838	The Main Theorem of Equivalences: every equivalence relation implies equivalent comembers. (Contributed by Peter Mazsa, 15-Oct-2021.)
⊢ (𝑅 ErALTV 𝐴 → ( CoElEqvRel 𝐴 ∧ ¬ ∅ ∈ 𝐴))
Theorem	mainerim 38839	Every equivalence relation implies equivalent coelements. (Contributed by Peter Mazsa, 20-Oct-2021.)
⊢ (𝑅 ErALTV 𝐴 → CoElEqvRel 𝐴)
Theorem	petincnvepres2 38840	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 38841	The shortest form of a partition-equivalence theorem with intersection and general 𝑅. Cf. br1cossincnvepres 38441. Cf. pet 38843. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ ((𝑅 ∩ (◡ E ↾ 𝐴)) Part 𝐴 ↔ ≀ (𝑅 ∩ (◡ E ↾ 𝐴)) ErALTV 𝐴)
Theorem	pet2 38842	Partition-Equivalence Theorem, with general 𝑅. This theorem (together with pet 38843 and pets 38844) is the main result of my investigation into set theory, see the comment of pet 38843. (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 38843	Partition-Equivalence Theorem with general 𝑅 while preserving the restricted converse epsilon relation of mpet2 38832 (as opposed to petincnvepres 38841). 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 38443. This theorem (together with pets 38844 and pet2 38842) is the main result of my investigation into set theory. It is no more general than the conventional Member Partition-Equivalence Theorem mpet 38831, mpet2 38832 and mpet3 38828 (because you cannot set 𝑅 in this theorem in such a way that you get mpet2 38832), i.e., it is not the hypothetical General Partition-Equivalence Theorem gpet ⊢ (𝑅 Part 𝐴 ↔ ≀ 𝑅 ErALTV 𝐴), but this one has a general part that mpet2 38832 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 38844	Partition-Equivalence Theorem with general 𝑅, with binary relations. This theorem (together with pet 38843 and pet2 38842) is the main result of my investigation into set theory, cf. the comment of pet 38843. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → ((𝑅 ⋉ (◡ E ↾ 𝐴)) Parts 𝐴 ↔ ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) Ers 𝐴))
Theorem	dmqsblocks 38845*	If the pet 38843 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 38640). It makes explicit that pet 38843 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 38846	Lemma for prter3 38875. (Contributed by Rodolfo Medina, 9-Oct-2010.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜓 → (𝜃 → 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏)))
Theorem	bicomdd 38847	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 38848	Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 17-Oct-2010.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜓 → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜃 ∧ 𝜒)))
Theorem	jca3 38849	Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 14-Oct-2010.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜃 → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜃 → (𝜒 ∧ 𝜏))))
Theorem	prtlem70 38850	Lemma for prter3 38875: a rearrangement of conjuncts. (Contributed by Rodolfo Medina, 20-Oct-2010.)
⊢ ((((𝜓 ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜑) ↔ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ (𝜃 ∧ 𝜏)))) ∧ 𝜂))
Theorem	ibdr 38851	Reverse of ibd 269. (Contributed by Rodolfo Medina, 30-Sep-2010.)
⊢ (𝜑 → (𝜒 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (𝜒 → 𝜓))
Theorem	prtlem100 38852	Lemma for prter3 38875. (Contributed by Rodolfo Medina, 19-Oct-2010.)
⊢ (∃𝑥 ∈ 𝐴 (𝐵 ∈ 𝑥 ∧ 𝜑) ↔ ∃𝑥 ∈ (𝐴 ∖ {∅})(𝐵 ∈ 𝑥 ∧ 𝜑))
Theorem	prtlem5 38853*	Lemma for prter1 38872, prter2 38874, prter3 38875 and prtex 38873. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
⊢ ([𝑠 / 𝑣][𝑟 / 𝑢]∃𝑥 ∈ 𝐴 (𝑢 ∈ 𝑥 ∧ 𝑣 ∈ 𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝑟 ∈ 𝑥 ∧ 𝑠 ∈ 𝑥))
Theorem	prtlem80 38854	Lemma for prter2 38874. (Contributed by Rodolfo Medina, 17-Oct-2010.)
⊢ (𝐴 ∈ 𝐵 → ¬ 𝐴 ∈ (𝐶 ∖ {𝐴}))
Theorem	brabsb2 38855*	A closed form of brabsb 5491. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ (𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑} → (𝑧𝑅𝑤 ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑))
Theorem	eqbrrdv2 38856*	Other version of eqbrrdiv 5757. (Contributed by Rodolfo Medina, 30-Sep-2010.)
⊢ (((Rel 𝐴 ∧ Rel 𝐵) ∧ 𝜑) → (𝑥𝐴𝑦 ↔ 𝑥𝐵𝑦))    ⇒   ⊢ (((Rel 𝐴 ∧ Rel 𝐵) ∧ 𝜑) → 𝐴 = 𝐵)
Theorem	prtlem9 38857*	Lemma for prter3 38875. (Contributed by Rodolfo Medina, 25-Sep-2010.)
⊢ (𝐴 ∈ 𝐵 → ∃𝑥 ∈ 𝐵 [𝑥] ∼ = [𝐴] ∼ )
Theorem	prtlem10 38858*	Lemma for prter3 38875. (Contributed by Rodolfo Medina, 14-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ( ∼ Er 𝐴 → (𝑧 ∈ 𝐴 → (𝑧 ∼ 𝑤 ↔ ∃𝑣 ∈ 𝐴 (𝑧 ∈ [𝑣] ∼ ∧ 𝑤 ∈ [𝑣] ∼ ))))
Theorem	prtlem11 38859	Lemma for prter2 38874. (Contributed by Rodolfo Medina, 12-Oct-2010.)
⊢ (𝐵 ∈ 𝐷 → (𝐶 ∈ 𝐴 → (𝐵 = [𝐶] ∼ → 𝐵 ∈ (𝐴 / ∼ ))))
Theorem	prtlem12 38860*	Lemma for prtex 38873 and prter3 38875. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ ( ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} → Rel ∼ )
Theorem	prtlem13 38861*	Lemma for prter1 38872, prter2 38874, prter3 38875 and prtex 38873. (Contributed by Rodolfo Medina, 13-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ (𝑧 ∼ 𝑤 ↔ ∃𝑣 ∈ 𝐴 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))
Theorem	prtlem16 38862*	Lemma for prtex 38873, prter2 38874 and prter3 38875. (Contributed by Rodolfo Medina, 14-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ dom ∼ = ∪ 𝐴
Theorem	prtlem400 38863*	Lemma for prter2 38874 and also a property of partitions . (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ ¬ ∅ ∈ (∪ 𝐴 / ∼ )
Syntax	wprt 38864	Extend the definition of a wff to include the partition predicate.
wff Prt 𝐴
Definition	df-prt 38865*	Define the partition predicate. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ (Prt 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅))
Theorem	erprt 38866	The quotient set of an equivalence relation is a partition. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ ( ∼ Er 𝑋 → Prt (𝐴 / ∼ ))
Theorem	prtlem14 38867*	Lemma for prter1 38872, prter2 38874 and prtex 38873. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ (Prt 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑤 ∈ 𝑥 ∧ 𝑤 ∈ 𝑦) → 𝑥 = 𝑦)))
Theorem	prtlem15 38868*	Lemma for prter1 38872 and prtex 38873. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ (Prt 𝐴 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑢 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) ∧ (𝑤 ∈ 𝑦 ∧ 𝑣 ∈ 𝑦)) → ∃𝑧 ∈ 𝐴 (𝑢 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧)))
Theorem	prtlem17 38869*	Lemma for prter2 38874. (Contributed by Rodolfo Medina, 15-Oct-2010.)
⊢ (Prt 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥) → (∃𝑦 ∈ 𝐴 (𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦) → 𝑤 ∈ 𝑥)))
Theorem	prtlem18 38870*	Lemma for prter2 38874. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ (Prt 𝐴 → ((𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣) → (𝑤 ∈ 𝑣 ↔ 𝑧 ∼ 𝑤)))
Theorem	prtlem19 38871*	Lemma for prter2 38874. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ (Prt 𝐴 → ((𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣) → 𝑣 = [𝑧] ∼ ))
Theorem	prter1 38872*	Every partition generates an equivalence relation. (Contributed by Rodolfo Medina, 13-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ (Prt 𝐴 → ∼ Er ∪ 𝐴)
Theorem	prtex 38873*	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 38874*	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 38875*	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 2184, axc7 2316, axc10 2383, axc11 2428, axc11n 2424, axc15 2420, axc9 2380, axc14 2461, and axc16 2262.
Axiom	ax-c5 38876	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 1795. Conditional forms of the converse are given by ax-13 2370, ax-c14 38884, ax-c16 38885, and ax-5 1910. 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 2069). An interesting alternate axiomatization uses axc5c711 38911 and ax-c4 38877 in place of ax-c5 38876, ax-4 1809, ax-10 2142, and ax-11 2158. This axiom is obsolete and should no longer be used. It is proved above as Theorem sp 2184. (Contributed by NM, 3-Jan-1993.) Use sp 2184 instead. (New usage is discouraged.)
⊢ (∀𝑥𝜑 → 𝜑)
Axiom	ax-c4 38877	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 2320. (Contributed by NM, 3-Jan-1993.) (New usage is discouraged.)
⊢ (∀𝑥(∀𝑥𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
Axiom	ax-c7 38878	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 38911 in place of ax-c5 38876, ax-c7 38878, and ax-11 2158. This axiom is obsolete and should no longer be used. It is proved above as Theorem axc7 2316. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑)
Axiom	ax-c10 38879	A variant of ax6 2382. 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 2383. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.)
⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) → 𝜑)
Axiom	ax-c11 38880	Axiom ax-c11 38880 was the original version of ax-c11n 38881 ("n" for "new"), before it was discovered (in May 2008) that the shorter ax-c11n 38881 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 2428. (Contributed by NM, 10-May-1993.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑))
Axiom	ax-c11n 38881	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 38880 and was replaced with this shorter ax-c11n 38881 ("n" for "new") in May 2008. The old axiom is proved from this one as Theorem axc11 2428. Conversely, this axiom is proved from ax-c11 38880 as Theorem axc11nfromc11 38919. This axiom was proved redundant in July 2015. See Theorem axc11n 2424. This axiom is obsolete and should no longer be used. It is proved above as Theorem axc11n 2424. (Contributed by NM, 16-May-2008.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Axiom	ax-c15 38882	Axiom ax-c15 38882 was the original version of ax-12 2178, before it was discovered (in Jan. 2007) that the shorter ax-12 2178 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 38882 (from which the ax-12 2178 instance follows by Theorem ax12 2421.) The proof is by induction on formula length, using ax12eq 38934 and ax12el 38935 for the basis steps and ax12indn 38936, ax12indi 38937, and ax12inda 38941 for the induction steps. (This paragraph is true provided we use ax-c11 38880 in place of ax-c11n 38881.) This axiom is obsolete and should no longer be used. It is proved above as Theorem axc15 2420, which should be used instead. (Contributed by NM, 14-May-1993.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))
Axiom	ax-c9 38883	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 2380. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.)
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
Axiom	ax-c14 38884	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 1910; see Theorem axc14 2461. Alternately, ax-5 1910 becomes unnecessary in principle with this axiom, but we lose the more powerful metalogic afforded by ax-5 1910. We retain ax-c14 38884 here to provide completeness for systems with the simpler metalogic that results from omitting ax-5 1910, 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 2461. (Contributed by NM, 24-Jun-1993.) (New usage is discouraged.)
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦)))
Axiom	ax-c16 38885*	Axiom of Distinct Variables. The only axiom of predicate calculus requiring that variables be distinct (if we consider ax-5 1910 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 5396), but nonetheless it is technically necessary as you can see from its uses. This axiom is redundant if we include ax-5 1910; see Theorem axc16 2262. Alternately, ax-5 1910 becomes logically redundant in the presence of this axiom, but without ax-5 1910 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 38885 here to provide logical completeness for systems with the simpler metalogic that results from omitting ax-5 1910, 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 2262. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑))
21.28.2  Rederive new axioms ax-4, ax-10, ax-6, ax-12, ax-13 from old Theorems ax12fromc15 38898 and ax13fromc9 38899 require some intermediate theorems that are included in this section.
Theorem	axc5 38886	This theorem repeats sp 2184 under the name axc5 38886, so that the Metamath program "MM> VERIFY MARKUP" command will check that it matches axiom scheme ax-c5 38876. (Contributed by NM, 18-Aug-2017.) (Proof modification is discouraged.) Use sp 2184 instead. (New usage is discouraged.)
⊢ (∀𝑥𝜑 → 𝜑)
Theorem	ax4fromc4 38887	Rederivation of Axiom ax-4 1809 from ax-c4 38877, ax-c5 38876, ax-gen 1795 and minimal implicational calculus { ax-mp 5, ax-1 6, ax-2 7 }. See axc4 2320 for the derivation of ax-c4 38877 from ax-4 1809. (Contributed by NM, 23-May-2008.) (Proof modification is discouraged.) Use ax-4 1809 instead. (New usage is discouraged.)
⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
Theorem	ax10fromc7 38888	Rederivation of Axiom ax-10 2142 from ax-c7 38878, ax-c4 38877, ax-c5 38876, ax-gen 1795 and propositional calculus. See axc7 2316 for the derivation of ax-c7 38878 from ax-10 2142. (Contributed by NM, 23-May-2008.) (Proof modification is discouraged.) Use ax-10 2142 instead. (New usage is discouraged.)
⊢ (¬ ∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑)
Theorem	ax6fromc10 38889	Rederivation of Axiom ax-6 1967 from ax-c7 38878, ax-c10 38879, ax-gen 1795 and propositional calculus. See axc10 2383 for the derivation of ax-c10 38879 from ax-6 1967. Lemma L18 in [Megill] p. 446 (p. 14 of the preprint). (Contributed by NM, 14-May-1993.) (Proof modification is discouraged.) Use ax-6 1967 instead. (New usage is discouraged.)
⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦
Theorem	hba1-o 38890	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 38891	Inference version of ax-c4 38877. (Contributed by NM, 3-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑥𝜓)
Theorem	equid1 38892	Proof of equid 2012 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 1910; see the proof of equid 2012. See equid1ALT 38918 for an alternate proof. (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑥 = 𝑥
Theorem	equcomi1 38893	Proof of equcomi 2017 from equid1 38892, avoiding use of ax-5 1910 (the only use of ax-5 1910 is via ax7 2016, so using ax-7 2008 instead would remove dependency on ax-5 1910). (Contributed by BJ, 8-Jul-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
Theorem	aecom-o 38894	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 2425 using ax-c11 38880. Unlike axc11nfromc11 38919, this version does not require ax-5 1910 (see comment of equcomi1 38893). (Contributed by NM, 10-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Theorem	aecoms-o 38895	A commutation rule for identical variable specifiers. Version of aecoms 2426 using ax-c11 38880. (Contributed by NM, 10-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ (∀𝑦 𝑦 = 𝑥 → 𝜑)
Theorem	hbae-o 38896	All variables are effectively bound in an identical variable specifier. Version of hbae 2429 using ax-c11 38880. (Contributed by NM, 13-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦)
Theorem	dral1-o 38897	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 2437 using ax-c11 38880. (Contributed by NM, 24-Nov-1994.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 ↔ ∀𝑦𝜓))
Theorem	ax12fromc15 38898	Rederivation of Axiom ax-12 2178 from ax-c15 38882, ax-c11 38880 (used through dral1-o 38897), and other older axioms. See Theorem axc15 2420 for the derivation of ax-c15 38882 from ax-12 2178. An open problem is whether we can prove this using ax-c11n 38881 instead of ax-c11 38880. This proof uses newer axioms ax-4 1809 and ax-6 1967, 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 38877 and ax-c10 38879. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	ax13fromc9 38899	Derive ax-13 2370 from ax-c9 38883 and other older axioms. This proof uses newer axioms ax-4 1809 and ax-6 1967, 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 38877 and ax-c10 38879. (Contributed by NM, 21-Dec-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧))
21.28.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 38900*	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 1910 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 1795, ax-c4 38877, ax-c5 38876, ax-11 2158, ax-c7 38878, ax-7 2008, ax-c9 38883, ax-c10 38879, ax-c11 38880, ax-8 2111, ax-9 2119, ax-c14 38884, ax-c15 38882, and ax-c16 38885: in that system, we can derive any instance of ax-5 1910 not containing wff variables by induction on formula length, using ax5eq 38925 and ax5el 38930 for the basis together with hbn 2295, hbal 2168, and hbim 2299. 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.)
⊢ (𝜑 → ∀𝑥𝜑)