P. 366 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36501-36600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	elfunsALTV5 36501*	Elementhood in the class of functions. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ (𝐹 ∈ FunsALTV ↔ (∀𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹(𝑥 = 𝑦 ∨ ([𝑥]◡𝐹 ∩ [𝑦]◡𝐹) = ∅) ∧ 𝐹 ∈ Rels ))
Theorem	elfunsALTVfunALTV 36502	The element of the class of functions and the function predicate are the same when 𝐹 is a set. (Contributed by Peter Mazsa, 26-Jul-2021.)
⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ FunsALTV ↔ FunALTV 𝐹))
Theorem	funALTVfun 36503	Our definition of the function predicate df-funALTV 36487 (based on a more general, converse reflexive, relation) and the original definition of function in set.mm df-fun 6371, are always the same and interchangeable. (Contributed by Peter Mazsa, 27-Jul-2021.)
⊢ ( FunALTV 𝐹 ↔ Fun 𝐹)
Theorem	funALTVss 36504	Subclass theorem for function. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Mario Carneiro, 24-Jun-2014.) (Revised by Peter Mazsa, 22-Sep-2021.)
⊢ (𝐴 ⊆ 𝐵 → ( FunALTV 𝐵 → FunALTV 𝐴))
Theorem	funALTVeq 36505	Equality theorem for function predicate. (Contributed by NM, 16-Aug-1994.)
⊢ (𝐴 = 𝐵 → ( FunALTV 𝐴 ↔ FunALTV 𝐵))
Theorem	funALTVeqi 36506	Equality inference for the function predicate. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ( FunALTV 𝐴 ↔ FunALTV 𝐵)
Theorem	funALTVeqd 36507	Equality deduction for the function predicate. (Contributed by NM, 23-Feb-2013.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ( FunALTV 𝐴 ↔ FunALTV 𝐵))
20.22.17  Disjoints vs. converse functions
Definition	df-disjss 36508	Define the class of all disjoint sets (but not necessarily disjoint relations, cf. df-disjs 36509). It is used only by df-disjs 36509. (Contributed by Peter Mazsa, 17-Jul-2021.)
⊢ Disjss = {𝑥 ∣ ≀ ◡𝑥 ∈ CnvRefRels }
Definition	df-disjs 36509	Define the disjoint relations class, i.e., the class of disjoints. We need Disjs for the definition of Parts and Part for the Partition-Equivalence Theorems: this need for Parts as disjoint relations on their domain quotients is the reason why we must define Disjs instead of simply using converse functions (cf. dfdisjALTV 36518). The element of the class of disjoints and the disjoint predicate are the same, that is (𝑅 ∈ Disjs ↔ Disj 𝑅) when 𝑅 is a set, see eldisjsdisj 36532. Alternate definitions are dfdisjs 36513, ... , dfdisjs5 36517. (Contributed by Peter Mazsa, 17-Jul-2021.)
⊢ Disjs = ( Disjss ∩ Rels )
Definition	df-disjALTV 36510	Define the disjoint relation predicate, i.e., the disjoint predicate. A disjoint relation is a converse function of the relation by dfdisjALTV 36518, see the comment of df-disjs 36509 why we need disjoint relations instead of converse functions anyway. The element of the class of disjoints and the disjoint predicate are the same, that is (𝑅 ∈ Disjs ↔ Disj 𝑅) when 𝑅 is a set, see eldisjsdisj 36532. Alternate definitions are dfdisjALTV 36518, ... , dfdisjALTV5 36522. (Contributed by Peter Mazsa, 17-Jul-2021.)
⊢ ( Disj 𝑅 ↔ ( CnvRefRel ≀ ◡𝑅 ∧ Rel 𝑅))
Definition	df-eldisjs 36511	Define the disjoint elementhood relations class, i.e., the disjoint elements class. The element of the disjoint elements class and the disjoint elementhood predicate are the same, that is (𝐴 ∈ ElDisjs ↔ ElDisj 𝐴) when 𝐴 is a set, see eleldisjseldisj 36534. (Contributed by Peter Mazsa, 28-Nov-2022.)
⊢ ElDisjs = {𝑎 ∣ (◡ E ↾ 𝑎) ∈ Disjs }
Definition	df-eldisj 36512	Define the disjoint elementhood relation predicate, i.e., the disjoint elementhood predicate. Read: the elements of 𝐴 are disjoint. The element of the disjoint elements class and the disjoint elementhood predicate are the same, that is (𝐴 ∈ ElDisjs ↔ ElDisj 𝐴) when 𝐴 is a set, see eleldisjseldisj 36534. As of now, disjoint elementhood is defined as "partition" in set.mm : compare df-prt 36580 with dfeldisj5 36526. See also the comments of ~? dfmembpart2 and of ~? df-parts . (Contributed by Peter Mazsa, 17-Jul-2021.)
⊢ ( ElDisj 𝐴 ↔ Disj (◡ E ↾ 𝐴))
Theorem	dfdisjs 36513	Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 18-Jul-2021.)
⊢ Disjs = {𝑟 ∈ Rels ∣ ≀ ◡𝑟 ∈ CnvRefRels }
Theorem	dfdisjs2 36514	Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ Disjs = {𝑟 ∈ Rels ∣ ≀ ◡𝑟 ⊆ I }
Theorem	dfdisjs3 36515*	Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ Disjs = {𝑟 ∈ Rels ∣ ∀𝑢∀𝑣∀𝑥((𝑢𝑟𝑥 ∧ 𝑣𝑟𝑥) → 𝑢 = 𝑣)}
Theorem	dfdisjs4 36516*	Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ Disjs = {𝑟 ∈ Rels ∣ ∀𝑥∃*𝑢 𝑢𝑟𝑥}
Theorem	dfdisjs5 36517*	Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ Disjs = {𝑟 ∈ Rels ∣ ∀𝑢 ∈ dom 𝑟∀𝑣 ∈ dom 𝑟(𝑢 = 𝑣 ∨ ([𝑢]𝑟 ∩ [𝑣]𝑟) = ∅)}
Theorem	dfdisjALTV 36518	Alternate definition of the disjoint relation predicate. A disjoint relation is a converse function of the relation, see the comment of df-disjs 36509 why we need disjoint relations instead of converse functions anyway. (Contributed by Peter Mazsa, 27-Jul-2021.)
⊢ ( Disj 𝑅 ↔ ( FunALTV ◡𝑅 ∧ Rel 𝑅))
Theorem	dfdisjALTV2 36519	Alternate definition of the disjoint relation predicate, cf. dffunALTV2 36493. (Contributed by Peter Mazsa, 27-Jul-2021.)
⊢ ( Disj 𝑅 ↔ ( ≀ ◡𝑅 ⊆ I ∧ Rel 𝑅))
Theorem	dfdisjALTV3 36520*	Alternate definition of the disjoint relation predicate, cf. dffunALTV3 36494. (Contributed by Peter Mazsa, 28-Jul-2021.)
⊢ ( Disj 𝑅 ↔ (∀𝑢∀𝑣∀𝑥((𝑢𝑅𝑥 ∧ 𝑣𝑅𝑥) → 𝑢 = 𝑣) ∧ Rel 𝑅))
Theorem	dfdisjALTV4 36521*	Alternate definition of the disjoint relation predicate, cf. dffunALTV4 36495. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ ( Disj 𝑅 ↔ (∀𝑥∃*𝑢 𝑢𝑅𝑥 ∧ Rel 𝑅))
Theorem	dfdisjALTV5 36522*	Alternate definition of the disjoint relation predicate, cf. dffunALTV5 36496. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ ( Disj 𝑅 ↔ (∀𝑢 ∈ dom 𝑅∀𝑣 ∈ dom 𝑅(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ Rel 𝑅))
Theorem	dfeldisj2 36523	Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.)
⊢ ( ElDisj 𝐴 ↔ ≀ ◡(◡ E ↾ 𝐴) ⊆ I )
Theorem	dfeldisj3 36524*	Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.)
⊢ ( ElDisj 𝐴 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ∀𝑥 ∈ (𝑢 ∩ 𝑣)𝑢 = 𝑣)
Theorem	dfeldisj4 36525*	Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.)
⊢ ( ElDisj 𝐴 ↔ ∀𝑥∃*𝑢 ∈ 𝐴 𝑥 ∈ 𝑢)
Theorem	dfeldisj5 36526*	Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.)
⊢ ( ElDisj 𝐴 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ (𝑢 ∩ 𝑣) = ∅))
Theorem	eldisjs 36527	Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 24-Jul-2021.)
⊢ (𝑅 ∈ Disjs ↔ ( ≀ ◡𝑅 ∈ CnvRefRels ∧ 𝑅 ∈ Rels ))
Theorem	eldisjs2 36528	Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ (𝑅 ∈ Disjs ↔ ( ≀ ◡𝑅 ⊆ I ∧ 𝑅 ∈ Rels ))
Theorem	eldisjs3 36529*	Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ (𝑅 ∈ Disjs ↔ (∀𝑢∀𝑣∀𝑥((𝑢𝑅𝑥 ∧ 𝑣𝑅𝑥) → 𝑢 = 𝑣) ∧ 𝑅 ∈ Rels ))
Theorem	eldisjs4 36530*	Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ (𝑅 ∈ Disjs ↔ (∀𝑥∃*𝑢 𝑢𝑅𝑥 ∧ 𝑅 ∈ Rels ))
Theorem	eldisjs5 36531*	Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Disjs ↔ (∀𝑢 ∈ dom 𝑅∀𝑣 ∈ dom 𝑅(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ 𝑅 ∈ Rels )))
Theorem	eldisjsdisj 36532	The element of the class of disjoint relations and the disjoint relation predicate are the same, that is (𝑅 ∈ Disjs ↔ Disj 𝑅) when 𝑅 is a set. (Contributed by Peter Mazsa, 25-Jul-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Disjs ↔ Disj 𝑅))
Theorem	eleldisjs 36533	Elementhood in the disjoint elements class. (Contributed by Peter Mazsa, 23-Jul-2023.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ElDisjs ↔ (◡ E ↾ 𝐴) ∈ Disjs ))
Theorem	eleldisjseldisj 36534	The element of the disjoint elements class and the disjoint elementhood predicate are the same, that is (𝐴 ∈ ElDisjs ↔ ElDisj 𝐴) when 𝐴 is a set. (Contributed by Peter Mazsa, 23-Jul-2023.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ElDisjs ↔ ElDisj 𝐴))
Theorem	disjrel 36535	Disjoint relation is a relation. (Contributed by Peter Mazsa, 15-Sep-2021.)
⊢ ( Disj 𝑅 → Rel 𝑅)
Theorem	disjss 36536	Subclass theorem for disjoints. (Contributed by Peter Mazsa, 28-Oct-2020.) (Revised by Peter Mazsa, 22-Sep-2021.)
⊢ (𝐴 ⊆ 𝐵 → ( Disj 𝐵 → Disj 𝐴))
Theorem	disjssi 36537	Subclass theorem for disjoints, inference version. (Contributed by Peter Mazsa, 28-Sep-2021.)
⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ ( Disj 𝐵 → Disj 𝐴)
Theorem	disjssd 36538	Subclass theorem for disjoints, deduction version. (Contributed by Peter Mazsa, 28-Sep-2021.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → ( Disj 𝐵 → Disj 𝐴))
Theorem	disjeq 36539	Equality theorem for disjoints. (Contributed by Peter Mazsa, 22-Sep-2021.)
⊢ (𝐴 = 𝐵 → ( Disj 𝐴 ↔ Disj 𝐵))
Theorem	disjeqi 36540	Equality theorem for disjoints, inference version. (Contributed by Peter Mazsa, 22-Sep-2021.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ( Disj 𝐴 ↔ Disj 𝐵)
Theorem	disjeqd 36541	Equality theorem for disjoints, deduction version. (Contributed by Peter Mazsa, 22-Sep-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ( Disj 𝐴 ↔ Disj 𝐵))
Theorem	disjdmqseqeq1 36542	Lemma for the equality theorem for partition ~? parteq1 . (Contributed by Peter Mazsa, 5-Oct-2021.)
⊢ (𝑅 = 𝑆 → (( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ↔ ( Disj 𝑆 ∧ (dom 𝑆 / 𝑆) = 𝐴)))
Theorem	eldisjss 36543	Subclass theorem for disjoint elementhood. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ (𝐴 ⊆ 𝐵 → ( ElDisj 𝐵 → ElDisj 𝐴))
Theorem	eldisjssi 36544	Subclass theorem for disjoint elementhood, inference version. (Contributed by Peter Mazsa, 28-Sep-2021.)
⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ ( ElDisj 𝐵 → ElDisj 𝐴)
Theorem	eldisjssd 36545	Subclass theorem for disjoint elementhood, deduction version. (Contributed by Peter Mazsa, 28-Sep-2021.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → ( ElDisj 𝐵 → ElDisj 𝐴))
Theorem	eldisjeq 36546	Equality theorem for disjoint elementhood. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ (𝐴 = 𝐵 → ( ElDisj 𝐴 ↔ ElDisj 𝐵))
Theorem	eldisjeqi 36547	Equality theorem for disjoint elementhood, inference version. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ( ElDisj 𝐴 ↔ ElDisj 𝐵)
Theorem	eldisjeqd 36548	Equality theorem for disjoint elementhood, deduction version. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ( ElDisj 𝐴 ↔ ElDisj 𝐵))
Theorem	disjxrn 36549	Two ways of saying that a range Cartesian product is disjoint. (Contributed by Peter Mazsa, 17-Jun-2020.) (Revised by Peter Mazsa, 21-Sep-2021.)
⊢ ( Disj (𝑅 ⋉ 𝑆) ↔ ( ≀ ◡𝑅 ∩ ≀ ◡𝑆) ⊆ I )
Theorem	disjorimxrn 36550	Disjointness condition for range Cartesian product. (Contributed by Peter Mazsa, 12-Jul-2020.) (Revised by Peter Mazsa, 22-Sep-2021.)
⊢ (( Disj 𝑅 ∨ Disj 𝑆) → Disj (𝑅 ⋉ 𝑆))
Theorem	disjimxrn 36551	Disjointness condition for range Cartesian product. (Contributed by Peter Mazsa, 15-Dec-2020.) (Revised by Peter Mazsa, 22-Sep-2021.)
⊢ ( Disj 𝑆 → Disj (𝑅 ⋉ 𝑆))
Theorem	disjimres 36552	Disjointness condition for restriction. (Contributed by Peter Mazsa, 27-Sep-2021.)
⊢ ( Disj 𝑅 → Disj (𝑅 ↾ 𝐴))
Theorem	disjimin 36553	Disjointness condition for intersection. (Contributed by Peter Mazsa, 11-Jun-2021.) (Revised by Peter Mazsa, 28-Sep-2021.)
⊢ ( Disj 𝑆 → Disj (𝑅 ∩ 𝑆))
Theorem	disjiminres 36554	Disjointness condition for intersection with restriction. (Contributed by Peter Mazsa, 27-Sep-2021.)
⊢ ( Disj 𝑆 → Disj (𝑅 ∩ (𝑆 ↾ 𝐴)))
Theorem	disjimxrnres 36555	Disjointness condition for range Cartesian product with restriction. (Contributed by Peter Mazsa, 27-Sep-2021.)
⊢ ( Disj 𝑆 → Disj (𝑅 ⋉ (𝑆 ↾ 𝐴)))
Theorem	disjALTV0 36556	The null class is disjoint. (Contributed by Peter Mazsa, 27-Sep-2021.)
⊢ Disj ∅
Theorem	disjALTVid 36557	The class of identity relations is disjoint. (Contributed by Peter Mazsa, 20-Jun-2021.)
⊢ Disj I
Theorem	disjALTVidres 36558	The class of identity relations restricted is disjoint. (Contributed by Peter Mazsa, 28-Jun-2020.) (Revised by Peter Mazsa, 27-Sep-2021.)
⊢ Disj ( I ↾ 𝐴)
Theorem	disjALTVinidres 36559	The intersection with restricted identity relation is disjoint. (Contributed by Peter Mazsa, 31-Dec-2021.)
⊢ Disj (𝑅 ∩ ( I ↾ 𝐴))
Theorem	disjALTVxrnidres 36560	The class of range Cartesian product with restricted identity relation is disjoint. (Contributed by Peter Mazsa, 25-Jun-2020.) (Revised by Peter Mazsa, 27-Sep-2021.)
⊢ Disj (𝑅 ⋉ ( I ↾ 𝐴))
20.23  Mathbox for Rodolfo Medina
20.23.1  Partitions
Theorem	prtlem60 36561	Lemma for prter3 36590. (Contributed by Rodolfo Medina, 9-Oct-2010.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜓 → (𝜃 → 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏)))
Theorem	bicomdd 36562	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 36563	Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 17-Oct-2010.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜓 → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜃 ∧ 𝜒)))
Theorem	jca3 36564	Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 14-Oct-2010.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜃 → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜃 → (𝜒 ∧ 𝜏))))
Theorem	prtlem70 36565	Lemma for prter3 36590: a rearrangement of conjuncts. (Contributed by Rodolfo Medina, 20-Oct-2010.)
⊢ ((((𝜓 ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜑) ↔ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ (𝜃 ∧ 𝜏)))) ∧ 𝜂))
Theorem	ibdr 36566	Reverse of ibd 272. (Contributed by Rodolfo Medina, 30-Sep-2010.)
⊢ (𝜑 → (𝜒 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (𝜒 → 𝜓))
Theorem	prtlem100 36567	Lemma for prter3 36590. (Contributed by Rodolfo Medina, 19-Oct-2010.)
⊢ (∃𝑥 ∈ 𝐴 (𝐵 ∈ 𝑥 ∧ 𝜑) ↔ ∃𝑥 ∈ (𝐴 ∖ {∅})(𝐵 ∈ 𝑥 ∧ 𝜑))
Theorem	prtlem5 36568*	Lemma for prter1 36587, prter2 36589, prter3 36590 and prtex 36588. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
⊢ ([𝑠 / 𝑣][𝑟 / 𝑢]∃𝑥 ∈ 𝐴 (𝑢 ∈ 𝑥 ∧ 𝑣 ∈ 𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝑟 ∈ 𝑥 ∧ 𝑠 ∈ 𝑥))
Theorem	prtlem80 36569	Lemma for prter2 36589. (Contributed by Rodolfo Medina, 17-Oct-2010.)
⊢ (𝐴 ∈ 𝐵 → ¬ 𝐴 ∈ (𝐶 ∖ {𝐴}))
Theorem	brabsb2 36570*	A closed form of brabsb 5401. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ (𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑} → (𝑧𝑅𝑤 ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑))
Theorem	eqbrrdv2 36571*	Other version of eqbrrdiv 5653. (Contributed by Rodolfo Medina, 30-Sep-2010.)
⊢ (((Rel 𝐴 ∧ Rel 𝐵) ∧ 𝜑) → (𝑥𝐴𝑦 ↔ 𝑥𝐵𝑦))    ⇒   ⊢ (((Rel 𝐴 ∧ Rel 𝐵) ∧ 𝜑) → 𝐴 = 𝐵)
Theorem	prtlem9 36572*	Lemma for prter3 36590. (Contributed by Rodolfo Medina, 25-Sep-2010.)
⊢ (𝐴 ∈ 𝐵 → ∃𝑥 ∈ 𝐵 [𝑥] ∼ = [𝐴] ∼ )
Theorem	prtlem10 36573*	Lemma for prter3 36590. (Contributed by Rodolfo Medina, 14-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ( ∼ Er 𝐴 → (𝑧 ∈ 𝐴 → (𝑧 ∼ 𝑤 ↔ ∃𝑣 ∈ 𝐴 (𝑧 ∈ [𝑣] ∼ ∧ 𝑤 ∈ [𝑣] ∼ ))))
Theorem	prtlem11 36574	Lemma for prter2 36589. (Contributed by Rodolfo Medina, 12-Oct-2010.)
⊢ (𝐵 ∈ 𝐷 → (𝐶 ∈ 𝐴 → (𝐵 = [𝐶] ∼ → 𝐵 ∈ (𝐴 / ∼ ))))
Theorem	prtlem12 36575*	Lemma for prtex 36588 and prter3 36590. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ ( ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} → Rel ∼ )
Theorem	prtlem13 36576*	Lemma for prter1 36587, prter2 36589, prter3 36590 and prtex 36588. (Contributed by Rodolfo Medina, 13-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ (𝑧 ∼ 𝑤 ↔ ∃𝑣 ∈ 𝐴 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣))
Theorem	prtlem16 36577*	Lemma for prtex 36588, prter2 36589 and prter3 36590. (Contributed by Rodolfo Medina, 14-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ dom ∼ = ∪ 𝐴
Theorem	prtlem400 36578*	Lemma for prter2 36589 and also a property of partitions . (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ ¬ ∅ ∈ (∪ 𝐴 / ∼ )
Syntax	wprt 36579	Extend the definition of a wff to include the partition predicate.
wff Prt 𝐴
Definition	df-prt 36580*	Define the partition predicate. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ (Prt 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅))
Theorem	erprt 36581	The quotient set of an equivalence relation is a partition. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ ( ∼ Er 𝑋 → Prt (𝐴 / ∼ ))
Theorem	prtlem14 36582*	Lemma for prter1 36587, prter2 36589 and prtex 36588. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ (Prt 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑤 ∈ 𝑥 ∧ 𝑤 ∈ 𝑦) → 𝑥 = 𝑦)))
Theorem	prtlem15 36583*	Lemma for prter1 36587 and prtex 36588. (Contributed by Rodolfo Medina, 13-Oct-2010.)
⊢ (Prt 𝐴 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑢 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) ∧ (𝑤 ∈ 𝑦 ∧ 𝑣 ∈ 𝑦)) → ∃𝑧 ∈ 𝐴 (𝑢 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧)))
Theorem	prtlem17 36584*	Lemma for prter2 36589. (Contributed by Rodolfo Medina, 15-Oct-2010.)
⊢ (Prt 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥) → (∃𝑦 ∈ 𝐴 (𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦) → 𝑤 ∈ 𝑥)))
Theorem	prtlem18 36585*	Lemma for prter2 36589. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ (Prt 𝐴 → ((𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣) → (𝑤 ∈ 𝑣 ↔ 𝑧 ∼ 𝑤)))
Theorem	prtlem19 36586*	Lemma for prter2 36589. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ (Prt 𝐴 → ((𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣) → 𝑣 = [𝑧] ∼ ))
Theorem	prter1 36587*	Every partition generates an equivalence relation. (Contributed by Rodolfo Medina, 13-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)}    ⇒   ⊢ (Prt 𝐴 → ∼ Er ∪ 𝐴)
Theorem	prtex 36588*	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 36589*	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 36590*	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 ∪ 𝐴 ∧ (∪ 𝐴 / 𝑆) = (𝐴 ∖ {∅})) → ∼ = 𝑆)
20.24  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."
20.24.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 2180, axc7 2316, axc10 2382, axc11 2427, axc11n 2423, axc15 2419, axc9 2379, axc14 2460, and axc16 2258.
Axiom	ax-c5 36591	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 1803. Conditional forms of the converse are given by ax-13 2369, ax-c14 36599, ax-c16 36600, and ax-5 1918. 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 36626 and ax-c4 36592 in place of ax-c5 36591, ax-4 1817, ax-10 2141, and ax-11 2158. This axiom is obsolete and should no longer be used. It is proved above as Theorem sp 2180. (Contributed by NM, 3-Jan-1993.) Use sp 2180 instead. (New usage is discouraged.)
⊢ (∀𝑥𝜑 → 𝜑)
Axiom	ax-c4 36592	Axiom of Quantified Implication. This axiom moves a universal quantifier from outside to inside an implication, quantifying 𝜓. Notice that 𝑥 must not be a free variable in the antecedent of the quantified implication, and we express this by binding 𝜑 to "protect" the axiom from a 𝜑 containing a free 𝑥. Axiom scheme C4' in [Megill] p. 448 (p. 16 of the preprint). It is a special case of Lemma 5 of [Monk2] p. 108 and Axiom 5 of [Mendelson] p. 69. This axiom is obsolete and should no longer be used. It is proved above as Theorem axc4 2320. (Contributed by NM, 3-Jan-1993.) (New usage is discouraged.)
⊢ (∀𝑥(∀𝑥𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
Axiom	ax-c7 36593	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 36626 in place of ax-c5 36591, ax-c7 36593, and ax-11 2158. This axiom is obsolete and should no longer be used. It is proved above as Theorem axc7 2316. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑)
Axiom	ax-c10 36594	A variant of ax6 2381. 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 2382. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.)
⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) → 𝜑)
Axiom	ax-c11 36595	Axiom ax-c11 36595 was the original version of ax-c11n 36596 ("n" for "new"), before it was discovered (in May 2008) that the shorter ax-c11n 36596 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 2427. (Contributed by NM, 10-May-1993.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑))
Axiom	ax-c11n 36596	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 36595 and was replaced with this shorter ax-c11n 36596 ("n" for "new") in May 2008. The old axiom is proved from this one as Theorem axc11 2427. Conversely, this axiom is proved from ax-c11 36595 as Theorem axc11nfromc11 36634. This axiom was proved redundant in July 2015. See Theorem axc11n 2423. This axiom is obsolete and should no longer be used. It is proved above as Theorem axc11n 2423. (Contributed by NM, 16-May-2008.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Axiom	ax-c15 36597	Axiom ax-c15 36597 was the original version of ax-12 2175, before it was discovered (in Jan. 2007) that the shorter ax-12 2175 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 36597 (from which the ax-12 2175 instance follows by Theorem ax12 2420.) The proof is by induction on formula length, using ax12eq 36649 and ax12el 36650 for the basis steps and ax12indn 36651, ax12indi 36652, and ax12inda 36656 for the induction steps. (This paragraph is true provided we use ax-c11 36595 in place of ax-c11n 36596.) This axiom is obsolete and should no longer be used. It is proved above as Theorem axc15 2419, which should be used instead. (Contributed by NM, 14-May-1993.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))
Axiom	ax-c9 36598	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 2379. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.)
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
Axiom	ax-c14 36599	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 1918; see Theorem axc14 2460. Alternately, ax-5 1918 becomes unnecessary in principle with this axiom, but we lose the more powerful metalogic afforded by ax-5 1918. We retain ax-c14 36599 here to provide completeness for systems with the simpler metalogic that results from omitting ax-5 1918, 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 2460. (Contributed by NM, 24-Jun-1993.) (New usage is discouraged.)
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦)))
Axiom	ax-c16 36600*	Axiom of Distinct Variables. The only axiom of predicate calculus requiring that variables be distinct (if we consider ax-5 1918 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 5252), but nonetheless it is technically necessary as you can see from its uses. This axiom is redundant if we include ax-5 1918; see Theorem axc16 2258. Alternately, ax-5 1918 becomes logically redundant in the presence of this axiom, but without ax-5 1918 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 36600 here to provide logical completeness for systems with the simpler metalogic that results from omitting ax-5 1918, 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 2258. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑))