P. 393 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 39201-39300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mpets 39201	Member Partition-Equivalence Theorem in its shortest possible form: it shows that member partitions and comember equivalence relations are literally the same. Cf. pet 39210, the Partition-Equivalence Theorem, with general 𝑅. (Contributed by Peter Mazsa, 31-Dec-2024.)
⊢ MembParts = CoMembErs
Theorem	mainpart 39202	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 39203	The Theorem of Fences by Equivalences: all conceivable equivalence relations (besides the comember equivalence relation cf. mpet 39198) generate a partition of the members. (Contributed by Peter Mazsa, 26-Sep-2021.)
⊢ (𝑅 ErALTV 𝐴 → MembPart 𝐴)
Theorem	fences2 39204	The Theorem of Fences by Equivalences: all conceivable equivalence relations (besides the comember equivalence relation cf. mpet3 39195) 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 39205	The Main Theorem of Equivalences: every equivalence relation implies equivalent comembers. (Contributed by Peter Mazsa, 15-Oct-2021.)
⊢ (𝑅 ErALTV 𝐴 → ( CoElEqvRel 𝐴 ∧ ¬ ∅ ∈ 𝐴))
Theorem	mainerim 39206	Every equivalence relation implies equivalent coelements. (Contributed by Peter Mazsa, 20-Oct-2021.)
⊢ (𝑅 ErALTV 𝐴 → CoElEqvRel 𝐴)
Theorem	petincnvepres2 39207	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 39208	The shortest form of a partition-equivalence theorem with intersection and general 𝑅. Cf. br1cossincnvepres 38785. Cf. pet 39210. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ ((𝑅 ∩ (◡ E ↾ 𝐴)) Part 𝐴 ↔ ≀ (𝑅 ∩ (◡ E ↾ 𝐴)) ErALTV 𝐴)
Theorem	pet2 39209	Partition-Equivalence Theorem, with general 𝑅. This theorem (together with pet 39210 and pets 39211) is the main result of my investigation into set theory, see the comment of pet 39210. (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 39210	Partition-Equivalence Theorem with general 𝑅 while preserving the restricted converse epsilon relation of mpet2 39199 (as opposed to petincnvepres 39208). 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 38787. This theorem (together with pets 39211 and pet2 39209) is the main result of my investigation into set theory. It is no more general than the conventional Member Partition-Equivalence Theorem mpet 39198, mpet2 39199 and mpet3 39195 (because you cannot set 𝑅 in this theorem in such a way that you get mpet2 39199), i.e., it is not the hypothetical General Partition-Equivalence Theorem gpet ⊢ (𝑅 Part 𝐴 ↔ ≀ 𝑅 ErALTV 𝐴), but this one has a general part that mpet2 39199 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 39211	Partition-Equivalence Theorem with general 𝑅, with binary relations. This theorem (together with pet 39210 and pet2 39209) is the main result of my investigation into set theory, cf. the comment of pet 39210. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → ((𝑅 ⋉ (◡ E ↾ 𝐴)) Parts 𝐴 ↔ ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) Ers 𝐴))
Theorem	dmqsblocks 39212*	If the pet 39210 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 38978). It makes explicit that pet 39210 gives active representatives for each block, without ever forcing 𝑣 = 𝑢. (Contributed by Peter Mazsa, 23-Nov-2025.)
⊢ ((dom (𝑅 ⋉ (◡ E ↾ 𝐴)) / (𝑅 ⋉ (◡ E ↾ 𝐴))) = 𝐴 → ∀𝑢 ∈ 𝐴 ∃𝑣 ∈ dom (𝑅 ⋉ (◡ E ↾ 𝐴))∃𝑏∃𝑐(𝑢 = [𝑣](𝑅 ⋉ (◡ E ↾ 𝐴)) ∧ 𝑐 ∈ 𝑣 ∧ 𝑣𝑅𝑏))
21.26.23  Type-safe Partition-Equivalence: PetParts, PetErs, Pet2Parts, Pet2Ers
Definition	df-petparts 39213*	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 39217 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 39214*	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 39221 (using typesafepets 39220 and mpets 39201). The explicit typing (𝑟 ∈ Rels ∧ 𝑛 ∈ CoMembErs ) is included for the same reason as in df-petparts 39213: 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 39215	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 39210 (see dfpet2parts2 39218): 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 39217). Pet2Parts adds the external grade (tower) stability axis via df-shiftstable 38727 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 39187 / dfdisjs7 39188, whereas pet 39210 has an additional grade axis that must be imposed separately. (Contributed by Peter Mazsa, 19-Feb-2026.)
⊢ Pet2Parts = ( SucMap ShiftStable PetParts )
Definition	df-pet2ers 39216	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 39222). (Contributed by Peter Mazsa, 19-Feb-2026.)
⊢ Pet2Ers = ( SucMap ShiftStable PetErs )
Theorem	dfpetparts2 39217*	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 39187 / dfdisjs7 39188): 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 39218*	Grade stability applied to the decomposed PetParts modules. Pet2Parts is obtained by applying the grade-stability operator SucMap ShiftStable (see df-shiftstable 38727) to the modular intersection from dfpetparts2 39217. 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 39187 / dfdisjs7 39188), 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 39219*	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 39217 on the partition side. (Contributed by Peter Mazsa, 25-Feb-2026.)
⊢ PetErs = ((( Rels × CoMembErs ) ∩ {⟨𝑟, 𝑛⟩ ∣ ≀ (𝑟 ⋉ (◡ E ↾ 𝑛)) ∈ EqvRels }) ∩ {⟨𝑟, 𝑛⟩ ∣ (dom ≀ (𝑟 ⋉ (◡ E ↾ 𝑛)) / ≀ (𝑟 ⋉ (◡ E ↾ 𝑛))) = 𝑛})
Theorem	typesafepets 39220	Type-safe pets 39211 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 39211: 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 39221), in complete parallel with the membership bridge mpets 39201. This theorem is intentionally not the definition of PetParts; it is the bridge used by petseq 39221 after typedness is enforced by the "Pet*" definitions. (Contributed by Peter Mazsa, 19-Feb-2026.)
⊢ ((𝐴 ∈ MembParts ∧ 𝑅 ∈ 𝑉) → ((𝑅 ⋉ (◡ E ↾ 𝐴)) Parts 𝐴 ↔ ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) Ers 𝐴))
Theorem	petseq 39221	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 39201 plays for carriers: mpets 39201 identifies MembParts with CoMembErs at the membership-carrier level, while petseq 39221 identifies the corresponding span-level predicates built from Parts and Ers. Unlike the earlier broad pets 39211, the bridge used here is the type-safe span theorem typesafepets 39220, 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 39222	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.27  Mathbox for Rodolfo Medina
21.27.1  Partitions
Theorem	prtlem60 39223	Lemma for prter3 39252. (Contributed by Rodolfo Medina, 9-Oct-2010.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜓 → (𝜃 → 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏)))
Theorem	bicomdd 39224	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 39225	Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 17-Oct-2010.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜓 → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜃 ∧ 𝜒)))
Theorem	jca3 39226	Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 14-Oct-2010.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜃 → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜃 → (𝜒 ∧ 𝜏))))
Theorem	prtlem70 39227	Lemma for prter3 39252: a rearrangement of conjuncts. (Contributed by Rodolfo Medina, 20-Oct-2010.)
⊢ ((((𝜓 ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜑) ↔ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ (𝜃 ∧ 𝜏)))) ∧ 𝜂))
Theorem	ibdr 39228	Reverse of ibd 269. (Contributed by Rodolfo Medina, 30-Sep-2010.)
⊢ (𝜑 → (𝜒 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (𝜒 → 𝜓))
Theorem	prtlem100 39229	Lemma for prter3 39252. (Contributed by Rodolfo Medina, 19-Oct-2010.)
⊢ (∃𝑥 ∈ 𝐴 (𝐵 ∈ 𝑥 ∧ 𝜑) ↔ ∃𝑥 ∈ (𝐴 ∖ {∅})(𝐵 ∈ 𝑥 ∧ 𝜑))
Theorem	prtlem5 39230*	Lemma for prter1 39249, prter2 39251, prter3 39252 and prtex 39250. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
⊢ ([𝑠 / 𝑣][𝑟 / 𝑢]∃𝑥 ∈ 𝐴 (𝑢 ∈ 𝑥 ∧ 𝑣 ∈ 𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝑟 ∈ 𝑥 ∧ 𝑠 ∈ 𝑥))
Theorem	prtlem80 39231	Lemma for prter2 39251. (Contributed by Rodolfo Medina, 17-Oct-2010.)
⊢ (𝐴 ∈ 𝐵 → ¬ 𝐴 ∈ (𝐶 ∖ {𝐴}))
Theorem	brabsb2 39232*	A closed form of brabsb 5487. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ (𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑} → (𝑧𝑅𝑤 ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑))
Theorem	eqbrrdv2 39233*	Other version of eqbrrdiv 5751. (Contributed by Rodolfo Medina, 30-Sep-2010.)
⊢ (((Rel 𝐴 ∧ Rel 𝐵) ∧ 𝜑) → (𝑥𝐴𝑦 ↔ 𝑥𝐵𝑦))    ⇒   ⊢ (((Rel 𝐴 ∧ Rel 𝐵) ∧ 𝜑) → 𝐴 = 𝐵)
Theorem	prtlem9 39234*	Lemma for prter3 39252. (Contributed by Rodolfo Medina, 25-Sep-2010.)
⊢ (𝐴 ∈ 𝐵 → ∃𝑥 ∈ 𝐵 [𝑥] ∼ = [𝐴] ∼ )
Theorem	prtlem10 39235*	Lemma for prter3 39252. (Contributed by Rodolfo Medina, 14-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ( ∼ Er 𝐴 → (𝑧 ∈ 𝐴 → (𝑧 ∼ 𝑤 ↔ ∃𝑣 ∈ 𝐴 (𝑧 ∈ [𝑣] ∼ ∧ 𝑤 ∈ [𝑣] ∼ ))))
Theorem	prtlem11 39236	Lemma for prter2 39251. (Contributed by Rodolfo Medina, 12-Oct-2010.)
⊢ (𝐵 ∈ 𝐷 → (𝐶 ∈ 𝐴 → (𝐵 = [𝐶] ∼ → 𝐵 ∈ (𝐴 / ∼ ))))
Theorem	prtlem12 39237*	Lemma for prtex 39250 and prter3 39252. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ ( ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} → Rel ∼ )
Theorem	prtlem13 39238*	Lemma for prter1 39249, prter2 39251, prter3 39252 and prtex 39250. (Contributed by Rodolfo Medina, 13-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ (𝑧 ∼ 𝑤 ↔ ∃𝑣 ∈ 𝐴 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))
Theorem	prtlem16 39239*	Lemma for prtex 39250, prter2 39251 and prter3 39252. (Contributed by Rodolfo Medina, 14-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ dom ∼ = ∪ 𝐴
Theorem	prtlem400 39240*	Lemma for prter2 39251 and also a property of partitions . (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ ¬ ∅ ∈ (∪ 𝐴 / ∼ )
Syntax	wprt 39241	Extend the definition of a wff to include the partition predicate.
wff Prt 𝐴
Definition	df-prt 39242*	Define the partition predicate. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ (Prt 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅))
Theorem	erprt 39243	The quotient set of an equivalence relation is a partition. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ ( ∼ Er 𝑋 → Prt (𝐴 / ∼ ))
Theorem	prtlem14 39244*	Lemma for prter1 39249, prter2 39251 and prtex 39250. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ (Prt 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑤 ∈ 𝑥 ∧ 𝑤 ∈ 𝑦) → 𝑥 = 𝑦)))
Theorem	prtlem15 39245*	Lemma for prter1 39249 and prtex 39250. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ (Prt 𝐴 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑢 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) ∧ (𝑤 ∈ 𝑦 ∧ 𝑣 ∈ 𝑦)) → ∃𝑧 ∈ 𝐴 (𝑢 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧)))
Theorem	prtlem17 39246*	Lemma for prter2 39251. (Contributed by Rodolfo Medina, 15-Oct-2010.)
⊢ (Prt 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥) → (∃𝑦 ∈ 𝐴 (𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦) → 𝑤 ∈ 𝑥)))
Theorem	prtlem18 39247*	Lemma for prter2 39251. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ (Prt 𝐴 → ((𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣) → (𝑤 ∈ 𝑣 ↔ 𝑧 ∼ 𝑤)))
Theorem	prtlem19 39248*	Lemma for prter2 39251. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ (Prt 𝐴 → ((𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣) → 𝑣 = [𝑧] ∼ ))
Theorem	prter1 39249*	Every partition generates an equivalence relation. (Contributed by Rodolfo Medina, 13-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ (Prt 𝐴 → ∼ Er ∪ 𝐴)
Theorem	prtex 39250*	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 39251*	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 39252*	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 2191, axc7 2323, axc10 2390, axc11 2435, axc11n 2431, axc15 2427, axc9 2387, axc14 2468, and axc16 2269.
Axiom	ax-c5 39253	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 1797. Conditional forms of the converse are given by ax-13 2377, ax-c14 39261, ax-c16 39262, and ax-5 1912. 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 2074). An interesting alternate axiomatization uses axc5c711 39288 and ax-c4 39254 in place of ax-c5 39253, ax-4 1811, ax-10 2147, and ax-11 2163. This axiom is obsolete and should no longer be used. It is proved above as Theorem sp 2191. (Contributed by NM, 3-Jan-1993.) Use sp 2191 instead. (New usage is discouraged.)
⊢ (∀𝑥𝜑 → 𝜑)
Axiom	ax-c4 39254	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 2327. (Contributed by NM, 3-Jan-1993.) (New usage is discouraged.)
⊢ (∀𝑥(∀𝑥𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
Axiom	ax-c7 39255	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 39288 in place of ax-c5 39253, ax-c7 39255, and ax-11 2163. This axiom is obsolete and should no longer be used. It is proved above as Theorem axc7 2323. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑)
Axiom	ax-c10 39256	A variant of ax6 2389. 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 2390. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.)
⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) → 𝜑)
Axiom	ax-c11 39257	Axiom ax-c11 39257 was the original version of ax-c11n 39258 ("n" for "new"), before it was discovered (in May 2008) that the shorter ax-c11n 39258 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 2435. (Contributed by NM, 10-May-1993.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑))
Axiom	ax-c11n 39258	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 39257 and was replaced with this shorter ax-c11n 39258 ("n" for "new") in May 2008. The old axiom is proved from this one as Theorem axc11 2435. Conversely, this axiom is proved from ax-c11 39257 as Theorem axc11nfromc11 39296. This axiom was proved redundant in July 2015. See Theorem axc11n 2431. This axiom is obsolete and should no longer be used. It is proved above as Theorem axc11n 2431. (Contributed by NM, 16-May-2008.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Axiom	ax-c15 39259	Axiom ax-c15 39259 was the original version of ax-12 2185, before it was discovered (in Jan. 2007) that the shorter ax-12 2185 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 39259 (from which the ax-12 2185 instance follows by Theorem ax12 2428.) The proof is by induction on formula length, using ax12eq 39311 and ax12el 39312 for the basis steps and ax12indn 39313, ax12indi 39314, and ax12inda 39318 for the induction steps. (This paragraph is true provided we use ax-c11 39257 in place of ax-c11n 39258.) This axiom is obsolete and should no longer be used. It is proved above as Theorem axc15 2427, which should be used instead. (Contributed by NM, 14-May-1993.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))
Axiom	ax-c9 39260	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 2387. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.)
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
Axiom	ax-c14 39261	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 1912; see Theorem axc14 2468. Alternately, ax-5 1912 becomes unnecessary in principle with this axiom, but we lose the more powerful metalogic afforded by ax-5 1912. We retain ax-c14 39261 here to provide completeness for systems with the simpler metalogic that results from omitting ax-5 1912, 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 2468. (Contributed by NM, 24-Jun-1993.) (New usage is discouraged.)
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦)))
Axiom	ax-c16 39262*	Axiom of Distinct Variables. The only axiom of predicate calculus requiring that variables be distinct (if we consider ax-5 1912 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 5393), but nonetheless it is technically necessary as you can see from its uses. This axiom is redundant if we include ax-5 1912; see Theorem axc16 2269. Alternately, ax-5 1912 becomes logically redundant in the presence of this axiom, but without ax-5 1912 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 39262 here to provide logical completeness for systems with the simpler metalogic that results from omitting ax-5 1912, 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 2269. (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 39275 and ax13fromc9 39276 require some intermediate theorems that are included in this section.
Theorem	axc5 39263	This theorem repeats sp 2191 under the name axc5 39263, so that the Metamath program "MM> VERIFY MARKUP" command will check that it matches axiom scheme ax-c5 39253. (Contributed by NM, 18-Aug-2017.) (Proof modification is discouraged.) Use sp 2191 instead. (New usage is discouraged.)
⊢ (∀𝑥𝜑 → 𝜑)
Theorem	ax4fromc4 39264	Rederivation of Axiom ax-4 1811 from ax-c4 39254, ax-c5 39253, ax-gen 1797 and minimal implicational calculus { ax-mp 5, ax-1 6, ax-2 7 }. See axc4 2327 for the derivation of ax-c4 39254 from ax-4 1811. (Contributed by NM, 23-May-2008.) (Proof modification is discouraged.) Use ax-4 1811 instead. (New usage is discouraged.)
⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
Theorem	ax10fromc7 39265	Rederivation of Axiom ax-10 2147 from ax-c7 39255, ax-c4 39254, ax-c5 39253, ax-gen 1797 and propositional calculus. See axc7 2323 for the derivation of ax-c7 39255 from ax-10 2147. (Contributed by NM, 23-May-2008.) (Proof modification is discouraged.) Use ax-10 2147 instead. (New usage is discouraged.)
⊢ (¬ ∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑)
Theorem	ax6fromc10 39266	Rederivation of Axiom ax-6 1969 from ax-c7 39255, ax-c10 39256, ax-gen 1797 and propositional calculus. See axc10 2390 for the derivation of ax-c10 39256 from ax-6 1969. Lemma L18 in [Megill] p. 446 (p. 14 of the preprint). (Contributed by NM, 14-May-1993.) (Proof modification is discouraged.) Use ax-6 1969 instead. (New usage is discouraged.)
⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦
Theorem	hba1-o 39267	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 39268	Inference version of ax-c4 39254. (Contributed by NM, 3-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑥𝜓)
Theorem	equid1 39269	Proof of equid 2014 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 1912; see the proof of equid 2014. See equid1ALT 39295 for an alternate proof. (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑥 = 𝑥
Theorem	equcomi1 39270	Proof of equcomi 2019 from equid1 39269, avoiding use of ax-5 1912 (the only use of ax-5 1912 is via ax7 2018, so using ax-7 2010 instead would remove dependency on ax-5 1912). (Contributed by BJ, 8-Jul-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
Theorem	aecom-o 39271	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 2432 using ax-c11 39257. Unlike axc11nfromc11 39296, this version does not require ax-5 1912 (see comment of equcomi1 39270). (Contributed by NM, 10-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Theorem	aecoms-o 39272	A commutation rule for identical variable specifiers. Version of aecoms 2433 using ax-c11 39257. (Contributed by NM, 10-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ (∀𝑦 𝑦 = 𝑥 → 𝜑)
Theorem	hbae-o 39273	All variables are effectively bound in an identical variable specifier. Version of hbae 2436 using ax-c11 39257. (Contributed by NM, 13-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦)
Theorem	dral1-o 39274	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 2444 using ax-c11 39257. (Contributed by NM, 24-Nov-1994.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 ↔ ∀𝑦𝜓))
Theorem	ax12fromc15 39275	Rederivation of Axiom ax-12 2185 from ax-c15 39259, ax-c11 39257 (used through dral1-o 39274), and other older axioms. See Theorem axc15 2427 for the derivation of ax-c15 39259 from ax-12 2185. An open problem is whether we can prove this using ax-c11n 39258 instead of ax-c11 39257. This proof uses newer axioms ax-4 1811 and ax-6 1969, 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 39254 and ax-c10 39256. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	ax13fromc9 39276	Derive ax-13 2377 from ax-c9 39260 and other older axioms. This proof uses newer axioms ax-4 1811 and ax-6 1969, 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 39254 and ax-c10 39256. (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 39277*	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 1912 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 1797, ax-c4 39254, ax-c5 39253, ax-11 2163, ax-c7 39255, ax-7 2010, ax-c9 39260, ax-c10 39256, ax-c11 39257, ax-8 2116, ax-9 2124, ax-c14 39261, ax-c15 39259, and ax-c16 39262: in that system, we can derive any instance of ax-5 1912 not containing wff variables by induction on formula length, using ax5eq 39302 and ax5el 39307 for the basis together with hbn 2302, hbal 2173, and hbim 2306. However, if we omit this axiom, our development would be quite inconvenient since we could work only with specific instances of wffs containing no wff variables - this axiom introduces the concept of a setvar variable not occurring in a wff (as opposed to just two setvar variables being distinct). (Contributed by NM, 19-Aug-2017.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)
Theorem	sps-o 39278	Generalization of antecedent. (Contributed by NM, 5-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	hbequid 39279	Bound-variable hypothesis builder for 𝑥 = 𝑥. This theorem tells us that any variable, including 𝑥, is effectively not free in 𝑥 = 𝑥, even though 𝑥 is technically free according to the traditional definition of free variable. (The proof does not use ax-c10 39256.) (Contributed by NM, 13-Jan-2011.) (Proof shortened by Wolf Lammen, 23-Mar-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑥 → ∀𝑦 𝑥 = 𝑥)
Theorem	nfequid-o 39280	Bound-variable hypothesis builder for 𝑥 = 𝑥. This theorem tells us that any variable, including 𝑥, is effectively not free in 𝑥 = 𝑥, even though 𝑥 is technically free according to the traditional definition of free variable. (The proof uses only ax-4 1811, ax-7 2010, ax-c9 39260, and ax-gen 1797. This shows that this can be proved without ax6 2389, even though Theorem equid 2014 cannot. A shorter proof using ax6 2389 is obtainable from equid 2014 and hbth 1805.) Remark added 2-Dec-2015 NM: This proof does implicitly use ax6v 1970, which is used for the derivation of axc9 2387, unless we consider ax-c9 39260 the starting axiom rather than ax-13 2377. (Contributed by NM, 13-Jan-2011.) (Revised by Mario Carneiro, 12-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑦 𝑥 = 𝑥
Theorem	axc5c7 39281	Proof of a single axiom that can replace ax-c5 39253 and ax-c7 39255. See axc5c7toc5 39282 and axc5c7toc7 39283 for the rederivation of those axioms. (Contributed by Scott Fenton, 12-Sep-2005.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((∀𝑥 ¬ ∀𝑥𝜑 → ∀𝑥𝜑) → 𝜑)
Theorem	axc5c7toc5 39282	Rederivation of ax-c5 39253 from axc5c7 39281. Only propositional calculus is used for the rederivation. (Contributed by Scott Fenton, 12-Sep-2005.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥𝜑 → 𝜑)
Theorem	axc5c7toc7 39283	Rederivation of ax-c7 39255 from axc5c7 39281. Only propositional calculus is used for the rederivation. (Contributed by Scott Fenton, 12-Sep-2005.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑)
Theorem	axc711 39284	Proof of a single axiom that can replace both ax-c7 39255 and ax-11 2163. See axc711toc7 39286 and axc711to11 39287 for the rederivation of those axioms. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 ¬ ∀𝑦∀𝑥𝜑 → ∀𝑦𝜑)
Theorem	nfa1-o 39285	𝑥 is not free in ∀𝑥𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥∀𝑥𝜑
Theorem	axc711toc7 39286	Rederivation of ax-c7 39255 from axc711 39284. Note that ax-c7 39255 and ax-11 2163 are not used by the rederivation. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑)
Theorem	axc711to11 39287	Rederivation of ax-11 2163 from axc711 39284. Note that ax-c7 39255 and ax-11 2163 are not used by the rederivation. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
Theorem	axc5c711 39288	Proof of a single axiom that can replace ax-c5 39253, ax-c7 39255, and ax-11 2163 in a subsystem that includes these axioms plus ax-c4 39254 and ax-gen 1797 (and propositional calculus). See axc5c711toc5 39289, axc5c711toc7 39290, and axc5c711to11 39291 for the rederivation of those axioms. This theorem extends the idea in Scott Fenton's axc5c7 39281. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑 → ∀𝑥𝜑) → 𝜑)
Theorem	axc5c711toc5 39289	Rederivation of ax-c5 39253 from axc5c711 39288. Only propositional calculus is used by the rederivation. (Contributed by NM, 19-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥𝜑 → 𝜑)
Theorem	axc5c711toc7 39290	Rederivation of ax-c7 39255 from axc5c711 39288. Note that ax-c7 39255 and ax-11 2163 are not used by the rederivation. The use of alimi 1813 (which uses ax-c5 39253) is allowed since we have already proved axc5c711toc5 39289. (Contributed by NM, 19-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑)
Theorem	axc5c711to11 39291	Rederivation of ax-11 2163 from axc5c711 39288. Note that ax-c7 39255 and ax-11 2163 are not used by the rederivation. The use of alimi 1813 (which uses ax-c5 39253) is allowed since we have already proved axc5c711toc5 39289. (Contributed by NM, 19-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
Theorem	equidqe 39292	equid 2014 with existential quantifier without using ax-c5 39253 or ax-5 1912. (Contributed by NM, 13-Jan-2011.) (Proof shortened by Wolf Lammen, 27-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ ∀𝑦 ¬ 𝑥 = 𝑥
Theorem	axc5sp1 39293	A special case of ax-c5 39253 without using ax-c5 39253 or ax-5 1912. (Contributed by NM, 13-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑦 ¬ 𝑥 = 𝑥 → ¬ 𝑥 = 𝑥)
Theorem	equidq 39294	equid 2014 with universal quantifier without using ax-c5 39253 or ax-5 1912. (Contributed by NM, 13-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∀𝑦 𝑥 = 𝑥
Theorem	equid1ALT 39295	Alternate proof of equid 2014 and equid1 39269 from older axioms ax-c7 39255, ax-c10 39256 and ax-c9 39260. (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑥 = 𝑥
Theorem	axc11nfromc11 39296	Rederivation of ax-c11n 39258 from original version ax-c11 39257. See Theorem axc11 2435 for the derivation of ax-c11 39257 from ax-c11n 39258. This theorem should not be referenced in any proof. Instead, use ax-c11n 39258 above so that uses of ax-c11n 39258 can be more easily identified, or use aecom-o 39271 when this form is needed for studies involving ax-c11 39257 and omitting ax-5 1912. (Contributed by NM, 16-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Theorem	naecoms-o 39297	A commutation rule for distinct variable specifiers. Version of naecoms 2434 using ax-c11 39257. (Contributed by NM, 2-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → 𝜑)
Theorem	hbnae-o 39298	All variables are effectively bound in a distinct variable specifier. Lemma L19 in [Megill] p. 446 (p. 14 of the preprint). Version of hbnae 2437 using ax-c11 39257. (Contributed by NM, 13-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦)
Theorem	dvelimf-o 39299	Proof of dvelimh 2455 that uses ax-c11 39257 but not ax-c15 39259, ax-c11n 39258, or ax-12 2185. Version of dvelimh 2455 using ax-c11 39257 instead of axc11 2435. (Contributed by NM, 12-Nov-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜓 → ∀𝑧𝜓)    &   ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓))
Theorem	dral2-o 39300	Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). Version of dral2 2443 using ax-c11 39257. (Contributed by NM, 27-Feb-2005.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑧𝜑 ↔ ∀𝑧𝜓))