P. 394 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 39301-39400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pets 39301	Partition-Equivalence Theorem with general 𝑅, with binary relations. This theorem (together with pet 39300 and pet2 39299) is the main result of my investigation into set theory, cf. the comment of pet 39300. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → ((𝑅 ⋉ (◡ E ↾ 𝐴)) Parts 𝐴 ↔ ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) Ers 𝐴))
Theorem	dmqsblocks 39302*	If the pet 39300 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 39068). It makes explicit that pet 39300 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 39303*	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 39307 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 39304*	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 39311 (using typesafepets 39310 and mpets 39291). The explicit typing (𝑟 ∈ Rels ∧ 𝑛 ∈ CoMembErs ) is included for the same reason as in df-petparts 39303: 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 39305	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 39300 (see dfpet2parts2 39308): 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 39307). Pet2Parts adds the external grade (tower) stability axis via df-shiftstable 38817 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 39277 / dfdisjs7 39278, whereas pet 39300 has an additional grade axis that must be imposed separately. (Contributed by Peter Mazsa, 19-Feb-2026.)
⊢ Pet2Parts = ( SucMap ShiftStable PetParts )
Definition	df-pet2ers 39306	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 39312). (Contributed by Peter Mazsa, 19-Feb-2026.)
⊢ Pet2Ers = ( SucMap ShiftStable PetErs )
Theorem	dfpetparts2 39307*	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 39277 / dfdisjs7 39278): 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 39308*	Grade stability applied to the decomposed PetParts modules. Pet2Parts is obtained by applying the grade-stability operator SucMap ShiftStable (see df-shiftstable 38817) to the modular intersection from dfpetparts2 39307. 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 39277 / dfdisjs7 39278), 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 39309*	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 39307 on the partition side. (Contributed by Peter Mazsa, 25-Feb-2026.)
⊢ PetErs = ((( Rels × CoMembErs ) ∩ {⟨𝑟, 𝑛⟩ ∣ ≀ (𝑟 ⋉ (◡ E ↾ 𝑛)) ∈ EqvRels }) ∩ {⟨𝑟, 𝑛⟩ ∣ (dom ≀ (𝑟 ⋉ (◡ E ↾ 𝑛)) / ≀ (𝑟 ⋉ (◡ E ↾ 𝑛))) = 𝑛})
Theorem	typesafepets 39310	Type-safe pets 39301 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 39301: 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 39311), in complete parallel with the membership bridge mpets 39291. This theorem is intentionally not the definition of PetParts; it is the bridge used by petseq 39311 after typedness is enforced by the "Pet*" definitions. (Contributed by Peter Mazsa, 19-Feb-2026.)
⊢ ((𝐴 ∈ MembParts ∧ 𝑅 ∈ 𝑉) → ((𝑅 ⋉ (◡ E ↾ 𝐴)) Parts 𝐴 ↔ ≀ (𝑅 ⋉ (◡ E ↾ 𝐴)) Ers 𝐴))
Theorem	petseq 39311	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 39291 plays for carriers: mpets 39291 identifies MembParts with CoMembErs at the membership-carrier level, while petseq 39311 identifies the corresponding span-level predicates built from Parts and Ers. Unlike the earlier broad pets 39301, the bridge used here is the type-safe span theorem typesafepets 39310, 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 39312	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 39313	Lemma for prter3 39342. (Contributed by Rodolfo Medina, 9-Oct-2010.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜓 → (𝜃 → 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏)))
Theorem	bicomdd 39314	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 39315	Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 17-Oct-2010.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜓 → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜃 ∧ 𝜒)))
Theorem	jca3 39316	Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 14-Oct-2010.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜃 → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜃 → (𝜒 ∧ 𝜏))))
Theorem	prtlem70 39317	Lemma for prter3 39342: a rearrangement of conjuncts. (Contributed by Rodolfo Medina, 20-Oct-2010.)
⊢ ((((𝜓 ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜑) ↔ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ (𝜃 ∧ 𝜏)))) ∧ 𝜂))
Theorem	ibdr 39318	Reverse of ibd 269. (Contributed by Rodolfo Medina, 30-Sep-2010.)
⊢ (𝜑 → (𝜒 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (𝜒 → 𝜓))
Theorem	prtlem100 39319	Lemma for prter3 39342. (Contributed by Rodolfo Medina, 19-Oct-2010.)
⊢ (∃𝑥 ∈ 𝐴 (𝐵 ∈ 𝑥 ∧ 𝜑) ↔ ∃𝑥 ∈ (𝐴 ∖ {∅})(𝐵 ∈ 𝑥 ∧ 𝜑))
Theorem	prtlem5 39320*	Lemma for prter1 39339, prter2 39341, prter3 39342 and prtex 39340. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
⊢ ([𝑠 / 𝑣][𝑟 / 𝑢]∃𝑥 ∈ 𝐴 (𝑢 ∈ 𝑥 ∧ 𝑣 ∈ 𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝑟 ∈ 𝑥 ∧ 𝑠 ∈ 𝑥))
Theorem	prtlem80 39321	Lemma for prter2 39341. (Contributed by Rodolfo Medina, 17-Oct-2010.)
⊢ (𝐴 ∈ 𝐵 → ¬ 𝐴 ∈ (𝐶 ∖ {𝐴}))
Theorem	brabsb2 39322*	A closed form of brabsb 5479. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ (𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑} → (𝑧𝑅𝑤 ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑))
Theorem	eqbrrdv2 39323*	Other version of eqbrrdiv 5743. (Contributed by Rodolfo Medina, 30-Sep-2010.)
⊢ (((Rel 𝐴 ∧ Rel 𝐵) ∧ 𝜑) → (𝑥𝐴𝑦 ↔ 𝑥𝐵𝑦))    ⇒   ⊢ (((Rel 𝐴 ∧ Rel 𝐵) ∧ 𝜑) → 𝐴 = 𝐵)
Theorem	prtlem9 39324*	Lemma for prter3 39342. (Contributed by Rodolfo Medina, 25-Sep-2010.)
⊢ (𝐴 ∈ 𝐵 → ∃𝑥 ∈ 𝐵 [𝑥] ∼ = [𝐴] ∼ )
Theorem	prtlem10 39325*	Lemma for prter3 39342. (Contributed by Rodolfo Medina, 14-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ( ∼ Er 𝐴 → (𝑧 ∈ 𝐴 → (𝑧 ∼ 𝑤 ↔ ∃𝑣 ∈ 𝐴 (𝑧 ∈ [𝑣] ∼ ∧ 𝑤 ∈ [𝑣] ∼ ))))
Theorem	prtlem11 39326	Lemma for prter2 39341. (Contributed by Rodolfo Medina, 12-Oct-2010.)
⊢ (𝐵 ∈ 𝐷 → (𝐶 ∈ 𝐴 → (𝐵 = [𝐶] ∼ → 𝐵 ∈ (𝐴 / ∼ ))))
Theorem	prtlem12 39327*	Lemma for prtex 39340 and prter3 39342. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ ( ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} → Rel ∼ )
Theorem	prtlem13 39328*	Lemma for prter1 39339, prter2 39341, prter3 39342 and prtex 39340. (Contributed by Rodolfo Medina, 13-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ (𝑧 ∼ 𝑤 ↔ ∃𝑣 ∈ 𝐴 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))
Theorem	prtlem16 39329*	Lemma for prtex 39340, prter2 39341 and prter3 39342. (Contributed by Rodolfo Medina, 14-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ dom ∼ = ∪ 𝐴
Theorem	prtlem400 39330*	Lemma for prter2 39341 and also a property of partitions . (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ ¬ ∅ ∈ (∪ 𝐴 / ∼ )
Syntax	wprt 39331	Extend the definition of a wff to include the partition predicate.
wff Prt 𝐴
Definition	df-prt 39332*	Define the partition predicate. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ (Prt 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅))
Theorem	erprt 39333	The quotient set of an equivalence relation is a partition. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ ( ∼ Er 𝑋 → Prt (𝐴 / ∼ ))
Theorem	prtlem14 39334*	Lemma for prter1 39339, prter2 39341 and prtex 39340. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ (Prt 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑤 ∈ 𝑥 ∧ 𝑤 ∈ 𝑦) → 𝑥 = 𝑦)))
Theorem	prtlem15 39335*	Lemma for prter1 39339 and prtex 39340. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ (Prt 𝐴 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑢 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) ∧ (𝑤 ∈ 𝑦 ∧ 𝑣 ∈ 𝑦)) → ∃𝑧 ∈ 𝐴 (𝑢 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧)))
Theorem	prtlem17 39336*	Lemma for prter2 39341. (Contributed by Rodolfo Medina, 15-Oct-2010.)
⊢ (Prt 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥) → (∃𝑦 ∈ 𝐴 (𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦) → 𝑤 ∈ 𝑥)))
Theorem	prtlem18 39337*	Lemma for prter2 39341. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ (Prt 𝐴 → ((𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣) → (𝑤 ∈ 𝑣 ↔ 𝑧 ∼ 𝑤)))
Theorem	prtlem19 39338*	Lemma for prter2 39341. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ (Prt 𝐴 → ((𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣) → 𝑣 = [𝑧] ∼ ))
Theorem	prter1 39339*	Every partition generates an equivalence relation. (Contributed by Rodolfo Medina, 13-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ (Prt 𝐴 → ∼ Er ∪ 𝐴)
Theorem	prtex 39340*	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 39341*	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 39342*	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 39343	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 39351, ax-c16 39352, 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 39378 and ax-c4 39344 in place of ax-c5 39343, 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 39344	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 39345	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 39378 in place of ax-c5 39343, ax-c7 39345, 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 39346	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 39347	Axiom ax-c11 39347 was the original version of ax-c11n 39348 ("n" for "new"), before it was discovered (in May 2008) that the shorter ax-c11n 39348 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 39348	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 39347 and was replaced with this shorter ax-c11n 39348 ("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 39347 as Theorem axc11nfromc11 39386. 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 39349	Axiom ax-c15 39349 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 39349 (from which the ax-12 2185 instance follows by Theorem ax12 2428.) The proof is by induction on formula length, using ax12eq 39401 and ax12el 39402 for the basis steps and ax12indn 39403, ax12indi 39404, and ax12inda 39408 for the induction steps. (This paragraph is true provided we use ax-c11 39347 in place of ax-c11n 39348.) 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 39350	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 39351	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 39351 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 39352*	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 5384), 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 39352 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 39365 and ax13fromc9 39366 require some intermediate theorems that are included in this section.
Theorem	axc5 39353	This theorem repeats sp 2191 under the name axc5 39353, so that the Metamath program "MM> VERIFY MARKUP" command will check that it matches axiom scheme ax-c5 39343. (Contributed by NM, 18-Aug-2017.) (Proof modification is discouraged.) Use sp 2191 instead. (New usage is discouraged.)
⊢ (∀𝑥𝜑 → 𝜑)
Theorem	ax4fromc4 39354	Rederivation of Axiom ax-4 1811 from ax-c4 39344, ax-c5 39343, 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 39344 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 39355	Rederivation of Axiom ax-10 2147 from ax-c7 39345, ax-c4 39344, ax-c5 39343, ax-gen 1797 and propositional calculus. See axc7 2323 for the derivation of ax-c7 39345 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 39356	Rederivation of Axiom ax-6 1969 from ax-c7 39345, ax-c10 39346, ax-gen 1797 and propositional calculus. See axc10 2390 for the derivation of ax-c10 39346 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 39357	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 39358	Inference version of ax-c4 39344. (Contributed by NM, 3-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑥𝜓)
Theorem	equid1 39359	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 39385 for an alternate proof. (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑥 = 𝑥
Theorem	equcomi1 39360	Proof of equcomi 2019 from equid1 39359, 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 39361	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 39347. Unlike axc11nfromc11 39386, this version does not require ax-5 1912 (see comment of equcomi1 39360). (Contributed by NM, 10-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Theorem	aecoms-o 39362	A commutation rule for identical variable specifiers. Version of aecoms 2433 using ax-c11 39347. (Contributed by NM, 10-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ (∀𝑦 𝑦 = 𝑥 → 𝜑)
Theorem	hbae-o 39363	All variables are effectively bound in an identical variable specifier. Version of hbae 2436 using ax-c11 39347. (Contributed by NM, 13-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦)
Theorem	dral1-o 39364	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 39347. (Contributed by NM, 24-Nov-1994.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 ↔ ∀𝑦𝜓))
Theorem	ax12fromc15 39365	Rederivation of Axiom ax-12 2185 from ax-c15 39349, ax-c11 39347 (used through dral1-o 39364), and other older axioms. See Theorem axc15 2427 for the derivation of ax-c15 39349 from ax-12 2185. An open problem is whether we can prove this using ax-c11n 39348 instead of ax-c11 39347. 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 39344 and ax-c10 39346. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	ax13fromc9 39366	Derive ax-13 2377 from ax-c9 39350 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 39344 and ax-c10 39346. (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 39367*	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 39344, ax-c5 39343, ax-11 2163, ax-c7 39345, ax-7 2010, ax-c9 39350, ax-c10 39346, ax-c11 39347, ax-8 2116, ax-9 2124, ax-c14 39351, ax-c15 39349, and ax-c16 39352: in that system, we can derive any instance of ax-5 1912 not containing wff variables by induction on formula length, using ax5eq 39392 and ax5el 39397 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 39368	Generalization of antecedent. (Contributed by NM, 5-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	hbequid 39369	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 39346.) (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 39370	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 39350, 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 39350 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 39371	Proof of a single axiom that can replace ax-c5 39343 and ax-c7 39345. See axc5c7toc5 39372 and axc5c7toc7 39373 for the rederivation of those axioms. (Contributed by Scott Fenton, 12-Sep-2005.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((∀𝑥 ¬ ∀𝑥𝜑 → ∀𝑥𝜑) → 𝜑)
Theorem	axc5c7toc5 39372	Rederivation of ax-c5 39343 from axc5c7 39371. 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 39373	Rederivation of ax-c7 39345 from axc5c7 39371. 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 39374	Proof of a single axiom that can replace both ax-c7 39345 and ax-11 2163. See axc711toc7 39376 and axc711to11 39377 for the rederivation of those axioms. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 ¬ ∀𝑦∀𝑥𝜑 → ∀𝑦𝜑)
Theorem	nfa1-o 39375	𝑥 is not free in ∀𝑥𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥∀𝑥𝜑
Theorem	axc711toc7 39376	Rederivation of ax-c7 39345 from axc711 39374. Note that ax-c7 39345 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 39377	Rederivation of ax-11 2163 from axc711 39374. Note that ax-c7 39345 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 39378	Proof of a single axiom that can replace ax-c5 39343, ax-c7 39345, and ax-11 2163 in a subsystem that includes these axioms plus ax-c4 39344 and ax-gen 1797 (and propositional calculus). See axc5c711toc5 39379, axc5c711toc7 39380, and axc5c711to11 39381 for the rederivation of those axioms. This theorem extends the idea in Scott Fenton's axc5c7 39371. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑 → ∀𝑥𝜑) → 𝜑)
Theorem	axc5c711toc5 39379	Rederivation of ax-c5 39343 from axc5c711 39378. Only propositional calculus is used by the rederivation. (Contributed by NM, 19-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥𝜑 → 𝜑)
Theorem	axc5c711toc7 39380	Rederivation of ax-c7 39345 from axc5c711 39378. Note that ax-c7 39345 and ax-11 2163 are not used by the rederivation. The use of alimi 1813 (which uses ax-c5 39343) is allowed since we have already proved axc5c711toc5 39379. (Contributed by NM, 19-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑)
Theorem	axc5c711to11 39381	Rederivation of ax-11 2163 from axc5c711 39378. Note that ax-c7 39345 and ax-11 2163 are not used by the rederivation. The use of alimi 1813 (which uses ax-c5 39343) is allowed since we have already proved axc5c711toc5 39379. (Contributed by NM, 19-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
Theorem	equidqe 39382	equid 2014 with existential quantifier without using ax-c5 39343 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 39383	A special case of ax-c5 39343 without using ax-c5 39343 or ax-5 1912. (Contributed by NM, 13-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑦 ¬ 𝑥 = 𝑥 → ¬ 𝑥 = 𝑥)
Theorem	equidq 39384	equid 2014 with universal quantifier without using ax-c5 39343 or ax-5 1912. (Contributed by NM, 13-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∀𝑦 𝑥 = 𝑥
Theorem	equid1ALT 39385	Alternate proof of equid 2014 and equid1 39359 from older axioms ax-c7 39345, ax-c10 39346 and ax-c9 39350. (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑥 = 𝑥
Theorem	axc11nfromc11 39386	Rederivation of ax-c11n 39348 from original version ax-c11 39347. See Theorem axc11 2435 for the derivation of ax-c11 39347 from ax-c11n 39348. This theorem should not be referenced in any proof. Instead, use ax-c11n 39348 above so that uses of ax-c11n 39348 can be more easily identified, or use aecom-o 39361 when this form is needed for studies involving ax-c11 39347 and omitting ax-5 1912. (Contributed by NM, 16-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Theorem	naecoms-o 39387	A commutation rule for distinct variable specifiers. Version of naecoms 2434 using ax-c11 39347. (Contributed by NM, 2-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → 𝜑)
Theorem	hbnae-o 39388	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 39347. (Contributed by NM, 13-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦)
Theorem	dvelimf-o 39389	Proof of dvelimh 2455 that uses ax-c11 39347 but not ax-c15 39349, ax-c11n 39348, or ax-12 2185. Version of dvelimh 2455 using ax-c11 39347 instead of axc11 2435. (Contributed by NM, 12-Nov-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜓 → ∀𝑧𝜓)    &   ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓))
Theorem	dral2-o 39390	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 39347. (Contributed by NM, 27-Feb-2005.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑧𝜑 ↔ ∀𝑧𝜓))
Theorem	aev-o 39391*	A "distinctor elimination" lemma with no disjoint variable conditions on variables in the consequent, proved without using ax-c16 39352. Version of aev 2061 using ax-c11 39347. (Contributed by NM, 8-Nov-2006.) (Proof shortened by Andrew Salmon, 21-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑤 = 𝑣)
Theorem	ax5eq 39392*	Theorem to add distinct quantifier to atomic formula. (This theorem demonstrates the induction basis for ax-5 1912 considered as a metatheorem. Do not use it for later proofs - use ax-5 1912 instead, to avoid reference to the redundant axiom ax-c16 39352.) (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)
Theorem	dveeq2-o 39393*	Quantifier introduction when one pair of variables is distinct. Version of dveeq2 2383 using ax-c15 39349. (Contributed by NM, 2-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
Theorem	axc16g-o 39394*	A generalization of Axiom ax-c16 39352. Version of axc16g 2268 using ax-c11 39347. (Contributed by NM, 15-May-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑧𝜑))
Theorem	dveeq1-o 39395*	Quantifier introduction when one pair of variables is distinct. Version of dveeq1 2385 using ax-c11 . (Contributed by NM, 2-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧))
Theorem	dveeq1-o16 39396*	Version of dveeq1 2385 using ax-c16 39352 instead of ax-5 1912. (Contributed by NM, 29-Apr-2008.) TODO: Recover proof from older set.mm to remove use of ax-5 1912. (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧))
Theorem	ax5el 39397*	Theorem to add distinct quantifier to atomic formula. This theorem demonstrates the induction basis for ax-5 1912 considered as a metatheorem.) (Contributed by NM, 22-Jun-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦)
Theorem	axc11n-16 39398*	This theorem shows that, given ax-c16 39352, we can derive a version of ax-c11n 39348. However, it is weaker than ax-c11n 39348 because it has a distinct variable requirement. (Contributed by Andrew Salmon, 27-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑧 → ∀𝑧 𝑧 = 𝑥)
Theorem	dveel2ALT 39399*	Alternate proof of dveel2 2467 using ax-c16 39352 instead of ax-5 1912. (Contributed by NM, 10-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 ∈ 𝑦 → ∀𝑥 𝑧 ∈ 𝑦))
Theorem	ax12f 39400	Basis step for constructing a substitution instance of ax-c15 39349 without using ax-c15 39349. We can start with any formula 𝜑 in which 𝑥 is not free. (Contributed by NM, 21-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))