P. 389 of Theorem List - Metamath Proof Explorer

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

Type	Label	Description
Statement
Theorem	ac6s3f 38801*	Generalization of the Axiom of Choice to classes, with bound-variable hypothesis. (Contributed by Giovanni Mascellani, 19-Aug-2018.)
⊢ Ⅎ𝑦𝜓    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦𝜑 → ∃𝑓∀𝑥 ∈ 𝐴 𝜓)
Theorem	ac6s6 38802*	Generalization of the Axiom of Choice to classes, moving the existence condition in the consequent. (Contributed by Giovanni Mascellani, 19-Aug-2018.)
⊢ Ⅎ𝑦𝜓    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ∃𝑓∀𝑥 ∈ 𝐴 (∃𝑦𝜑 → 𝜓)
Theorem	ac6s6f 38803*	Generalization of the Axiom of Choice to classes, moving the existence condition in the consequent. (Contributed by Giovanni Mascellani, 20-Aug-2018.)
⊢ 𝐴 ∈ V    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓))    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ ∃𝑓∀𝑥 ∈ 𝐴 (∃𝑦𝜑 → 𝜓)
21.26  Mathbox for Peter Mazsa
21.26.1  Notations
Syntax	cxrn 38804	Extend the definition of a class to include the range Cartesian product class.
class (𝐴 ⋉ 𝐵)
Syntax	cqmap 38805	Extend the definition of a class to include the quotient map of a class.
class QMap 𝑅
Syntax	cadjliftmap 38806	Extend the definition of a class to include the class of adjoined lift maps.
class (𝑅 AdjLiftMap 𝐴)
Syntax	cblockliftmap 38807	Extend the definition of a class to include the class of block lift maps.
class (𝑅 BlockLiftMap 𝐴)
Syntax	csucmap 38808	Extend the definition of a class to include the class of successor maps.
class SucMap
Syntax	csuccl 38809	Extend the definition of a class to include the class of successors.
class Suc
Syntax	cpre 38810	Extend the definition of a class to include the predecessor of a class.
class pre 𝑁
Syntax	cblockliftfix 38811	Extend the definition of a class to include the class of equilibrium block lifts.
class BlockLiftFix
Syntax	cshiftstable 38812	Extend the definition of a class to include the shift stability class.
class (𝑆 ShiftStable 𝐹)
Syntax	ccoss 38813	Extend the definition of a class to include the class of cosets by a class. (Read: the class of cosets by 𝑅.)
class ≀ 𝑅
Syntax	ccoels 38814	Extend the definition of a class to include the class of coelements on a class. (Read: the class of coelements on 𝐴.)
class ∼ 𝐴
Syntax	crels 38815	Extend the definition of a class to include the relation class.
class Rels
Syntax	cssr 38816	Extend the definition of a class to include the subset class.
class S
Syntax	crefs 38817	Extend the definition of a class to include the reflexivity class.
class Refs
Syntax	crefrels 38818	Extend the definition of a class to include the reflexive relations class.
class RefRels
Syntax	wrefrel 38819	Extend the definition of a wff to include the reflexive relation predicate. (Read: 𝑅 is a reflexive relation.)
wff RefRel 𝑅
Syntax	ccnvrefs 38820	Extend the definition of a class to include the converse reflexivity class.
class CnvRefs
Syntax	ccnvrefrels 38821	Extend the definition of a class to include the converse reflexive relations class.
class CnvRefRels
Syntax	wcnvrefrel 38822	Extend the definition of a wff to include the converse reflexive relation predicate. (Read: 𝑅 is a converse reflexive relation.)
wff CnvRefRel 𝑅
Syntax	csyms 38823	Extend the definition of a class to include the symmetry class.
class Syms
Syntax	csymrels 38824	Extend the definition of a class to include the symmetry relations class.
class SymRels
Syntax	wsymrel 38825	Extend the definition of a wff to include the symmetry relation predicate. (Read: 𝑅 is a symmetric relation.)
wff SymRel 𝑅
Syntax	ctrs 38826	Extend the definition of a class to include the transitivity class (but cf. the transitive class defined in df-tr 5220).
class Trs
Syntax	ctrrels 38827	Extend the definition of a class to include the transitive relations class.
class TrRels
Syntax	wtrrel 38828	Extend the definition of a wff to include the transitive relation predicate. (Read: 𝑅 is a transitive relation.)
wff TrRel 𝑅
Syntax	ceqvrels 38829	Extend the definition of a class to include the equivalence relations class.
class EqvRels
Syntax	weqvrel 38830	Extend the definition of a wff to include the equivalence relation predicate. (Read: 𝑅 is an equivalence relation.)
wff EqvRel 𝑅
Syntax	ccoeleqvrels 38831	Extend the definition of a class to include the coelement equivalence relations class.
class CoElEqvRels
Syntax	wcoeleqvrel 38832	Extend the definition of a wff to include the coelement equivalence relation predicate. (Read: the coelement equivalence relation on 𝐴.)
wff CoElEqvRel 𝐴
Syntax	credunds 38833	Extend the definition of a class to include the redundancy class.
class Redunds
Syntax	wredund 38834	Extend the definition of a wff to include the redundancy predicate. (Read: 𝐴 is redundant with respect to 𝐵 in 𝐶.)
wff 𝐴 Redund ⟨𝐵, 𝐶⟩
Syntax	wredundp 38835	Extend wff definition to include the redundancy operator for propositions.
wff redund (𝜑, 𝜓, 𝜒)
Syntax	cdmqss 38836	Extend the definition of a class to include the domain quotients class.
class DomainQss
Syntax	wdmqs 38837	Extend the definition of a wff to include the domain quotient predicate. (Read: the domain quotient of 𝑅 is 𝐴.)
wff 𝑅 DomainQs 𝐴
Syntax	cers 38838	Extend the definition of a class to include the equivalence relations on their domain quotients class.
class Ers
Syntax	werALTV 38839	Extend the definition of a wff to include the equivalence relation on its domain quotient predicate. (Read: 𝑅 is an equivalence relation on its domain quotient 𝐴.)
wff 𝑅 ErALTV 𝐴
Syntax	cpeters 38840	Extend the definition of a class to include the blocklift-stable equivalence relations class.
class PetErs
Syntax	cpet2ers 38841	Extend the definition of a class to include the grade- and blocklift-stable equivalence relations class.
class Pet2Ers
Syntax	ccomembers 38842	Extend the definition of a class to include the comember equivalence relations class.
class CoMembErs
Syntax	wcomember 38843	Extend the definition of a wff to include the comember equivalence relation predicate. (Read: the comember equivalence relation on 𝐴, or, the restricted coelement equivalence relation on its domain quotient 𝐴.)
wff CoMembEr 𝐴
Syntax	cfunss 38844	Extend the definition of a class to include the function set class.
class Funss
Syntax	cfunsALTV 38845	Extend the definition of a class to include the functions class, i.e., the function relations class.
class FunsALTV
Syntax	wfunALTV 38846	Extend the definition of a wff to include the function predicate, i.e., the function relation predicate. (Read: 𝐹 is a function.)
wff FunALTV 𝐹
Syntax	cdisjss 38847	Extend the definition of a class to include the disjoint set class.
class Disjss
Syntax	cdisjs 38848	Extend the definition of a class to include the disjoints class, i.e., the disjoint relations class.
class Disjs
Syntax	wdisjALTV 38849	Extend the definition of a wff to include the disjoint predicate, i.e., the disjoint relation predicate. (Read: 𝑅 is a disjoint.)
wff Disj 𝑅
Syntax	celdisjs 38850	Extend the definition of a class to include the disjoint elements class, i.e., the disjoint element relations class.
class ElDisjs
Syntax	weldisj 38851	Extend the definition of a wff to include the disjoint element predicate, i.e., the disjoint element relation predicate. (Read: the elements of 𝐴 are disjoint.)
wff ElDisj 𝐴
Syntax	wantisymrel 38852	Extend the definition of a wff to include the antisymmetry relation predicate. (Read: 𝑅 is an antisymmetric relation.)
wff AntisymRel 𝑅
Syntax	cparts 38853	Extend the definition of a class to include the partitions class, i.e., the partition relations class.
class Parts
Syntax	wpart 38854	Extend the definition of a wff to include the partition predicate, i.e., the partition relation predicate. (Read: 𝐴 is a partition by 𝑅.)
wff 𝑅 Part 𝐴
Syntax	cmembparts 38855	Extend the definition of a class to include the member partitions class, i.e., the member partition relations class.
class MembParts
Syntax	wmembpart 38856	Extend the definition of a wff to include the member partition predicate, i.e., the member partition relation predicate. (Read: 𝐴 is a member partition.)
wff MembPart 𝐴
Syntax	cpetparts 38857	Extend the definition of a class to include the blocklift-stable partitions class.
class PetParts
Syntax	cpet2parts 38858	Extend the definition of a class to include the grade- and blocklift-stable partitions class.
class Pet2Parts
21.26.2  Preparatory theorems
Theorem	el2v1 38859	New way (elv 3460, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 23-Oct-2018.)
⊢ ((𝑥 ∈ V ∧ 𝜑) → 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	el3v1 38860	New way (elv 3460, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 16-Oct-2020.)
⊢ ((𝑥 ∈ V ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
Theorem	el3v2 38861	New way (elv 3460, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 16-Oct-2020.)
⊢ ((𝜑 ∧ 𝑦 ∈ V ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
Theorem	el3v12 38862	New way (elv 3460, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 11-Jul-2021.)
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜒 → 𝜃)
Theorem	el3v13 38863	New way (elv 3460, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 11-Jul-2021.)
⊢ ((𝑥 ∈ V ∧ 𝜓 ∧ 𝑧 ∈ V) → 𝜃)    ⇒   ⊢ (𝜓 → 𝜃)
Theorem	el3v23 38864	New way (elv 3460, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 11-Jul-2021.)
⊢ ((𝜑 ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	anan 38865	Multiple commutations in conjunction. (Contributed by Peter Mazsa, 7-Mar-2020.)
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ ((𝜑 ∧ 𝜃) ∧ 𝜏)) ↔ ((𝜓 ∧ 𝜃) ∧ (𝜑 ∧ (𝜒 ∧ 𝜏))))
Theorem	triantru3 38866	A wff is equivalent to its conjunctions with truths. (Contributed by Peter Mazsa, 30-Nov-2018.)
⊢ 𝜑    &   ⊢ 𝜓    ⇒   ⊢ (𝜒 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒))
Theorem	biorfd 38867	A wff is equivalent to its disjunction with falsehood, deduction form. (Contributed by Peter Mazsa, 22-Aug-2023.)
⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → (𝜒 ↔ (𝜓 ∨ 𝜒)))
Theorem	eqbrtr 38868	Substitution of equal classes in binary relation. (Contributed by Peter Mazsa, 14-Jun-2024.)
⊢ ((𝐴 = 𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶)
Theorem	eqbrb 38869	Substitution of equal classes in a binary relation. (Contributed by Peter Mazsa, 14-Jun-2024.)
⊢ ((𝐴 = 𝐵 ∧ 𝐴𝑅𝐶) ↔ (𝐴 = 𝐵 ∧ 𝐵𝑅𝐶))
Theorem	eqeltr 38870	Substitution of equal classes into element relation. (Contributed by Peter Mazsa, 22-Jul-2017.)
⊢ ((𝐴 = 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)
Theorem	eqelb 38871	Substitution of equal classes into element relation. (Contributed by Peter Mazsa, 17-Jul-2019.)
⊢ ((𝐴 = 𝐵 ∧ 𝐴 ∈ 𝐶) ↔ (𝐴 = 𝐵 ∧ 𝐵 ∈ 𝐶))
Theorem	eqeqan2d 38872	Implication of introducing a new equality. (Contributed by Peter Mazsa, 17-Apr-2019.)
⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ ((𝐴 = 𝐵 ∧ 𝜑) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))
Theorem	disjresin 38873	The restriction to a disjoint is the empty class. (Contributed by Peter Mazsa, 24-Jul-2024.)
⊢ ((𝐴 ∩ 𝐵) = ∅ → (𝑅 ↾ (𝐴 ∩ 𝐵)) = ∅)
Theorem	disjresdisj 38874	The intersection of restrictions to disjoint is the empty class. (Contributed by Peter Mazsa, 24-Jul-2024.)
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝑅 ↾ 𝐴) ∩ (𝑅 ↾ 𝐵)) = ∅)
Theorem	disjresdif 38875	The difference between restrictions to disjoint is the first restriction. (Contributed by Peter Mazsa, 24-Jul-2024.)
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝑅 ↾ 𝐴) ∖ (𝑅 ↾ 𝐵)) = (𝑅 ↾ 𝐴))
Theorem	disjresundif 38876	Lemma for ressucdifsn2 39117. (Contributed by Peter Mazsa, 24-Jul-2024.)
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝑅 ↾ (𝐴 ∪ 𝐵)) ∖ (𝑅 ↾ 𝐵)) = (𝑅 ↾ 𝐴))
Theorem	inres2 38877	Two ways of expressing the restriction of an intersection. (Contributed by Peter Mazsa, 5-Jun-2021.)
⊢ ((𝑅 ↾ 𝐴) ∩ 𝑆) = ((𝑅 ∩ 𝑆) ↾ 𝐴)
Theorem	coideq 38878	Equality theorem for composition of two classes. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐴) = (𝐵 ∘ 𝐵))
Theorem	nexmo1 38879	If there is no case where wff is true, it is true for at most one case. (Contributed by Peter Mazsa, 27-Sep-2021.)
⊢ (¬ ∃𝑥𝜑 → ∃*𝑥𝜑)
Theorem	eqab2 38880	Implication of a class abstraction. (Contributed by Peter Mazsa, 16-Apr-2019.)
⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝜑) → ∀𝑥 ∈ 𝐴 𝜑)
Theorem	r2alan 38881*	Double restricted universal quantification, special case. (Contributed by Peter Mazsa, 17-Jun-2020.)
⊢ (∀𝑥∀𝑦(((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → 𝜓) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝜓))
Theorem	ssrabi 38882	Inference of restricted abstraction subclass from implication. (Contributed by Peter Mazsa, 26-Oct-2022.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓}
Theorem	rabimbieq 38883	Restricted equivalent wff's correspond to restricted class abstractions which are equal with the same class. (Contributed by Peter Mazsa, 22-Jul-2021.)
⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜑}    &   ⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜓}
Theorem	abeqin 38884*	Intersection with class abstraction. (Contributed by Peter Mazsa, 21-Jul-2021.)
⊢ 𝐴 = (𝐵 ∩ 𝐶)    &   ⊢ 𝐵 = {𝑥 ∣ 𝜑}    ⇒   ⊢ 𝐴 = {𝑥 ∈ 𝐶 ∣ 𝜑}
Theorem	abeqinbi 38885*	Intersection with class abstraction and equivalent wff's. (Contributed by Peter Mazsa, 21-Jul-2021.)
⊢ 𝐴 = (𝐵 ∩ 𝐶)    &   ⊢ 𝐵 = {𝑥 ∣ 𝜑}    &   ⊢ (𝑥 ∈ 𝐶 → (𝜑 ↔ 𝜓))    ⇒   ⊢ 𝐴 = {𝑥 ∈ 𝐶 ∣ 𝜓}
Theorem	eqrabi 38886*	Class element of a restricted class abstraction. (Contributed by Peter Mazsa, 24-Jul-2021.)
⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐵 ∧ 𝜑))    ⇒   ⊢ 𝐴 = {𝑥 ∈ 𝐵 ∣ 𝜑}
Theorem	rabeqel 38887*	Class element of a restricted class abstraction. (Contributed by Peter Mazsa, 24-Jul-2021.)
⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜑}    &   ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐶 ∈ 𝐵 ↔ (𝜓 ∧ 𝐶 ∈ 𝐴))
Theorem	eqrelf 38888*	The equality connective between relations. (Contributed by Peter Mazsa, 25-Jun-2019.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    ⇒   ⊢ ((Rel 𝐴 ∧ Rel 𝐵) → (𝐴 = 𝐵 ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐵)))
Theorem	br1cnvinxp 38889	Binary relation on the converse of an intersection with a Cartesian product. (Contributed by Peter Mazsa, 27-Jul-2019.)
⊢ (𝐶◡(𝑅 ∩ (𝐴 × 𝐵))𝐷 ↔ ((𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐴) ∧ 𝐷𝑅𝐶))
Theorem	releleccnv 38890	Elementhood in a converse 𝑅-coset when 𝑅 is a relation. (Contributed by Peter Mazsa, 9-Dec-2018.)
⊢ (Rel 𝑅 → (𝐴 ∈ [𝐵]◡𝑅 ↔ 𝐴𝑅𝐵))
Theorem	releccnveq 38891*	Equality of converse 𝑅-coset and converse 𝑆-coset when 𝑅 and 𝑆 are relations. (Contributed by Peter Mazsa, 27-Jul-2019.)
⊢ ((Rel 𝑅 ∧ Rel 𝑆) → ([𝐴]◡𝑅 = [𝐵]◡𝑆 ↔ ∀𝑥(𝑥𝑅𝐴 ↔ 𝑥𝑆𝐵)))
Theorem	xpv 38892*	Cartesian product of a class and the universe. (Contributed by Peter Mazsa, 6-Oct-2020.)
⊢ (𝐴 × V) = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ 𝐴}
Theorem	vxp 38893*	Cartesian product of the universe and a class. (Contributed by Peter Mazsa, 3-Dec-2020.)
⊢ (V × 𝐴) = {⟨𝑥, 𝑦⟩ ∣ 𝑦 ∈ 𝐴}
Theorem	opelvvdif 38894	Negated elementhood of ordered pair. (Contributed by Peter Mazsa, 14-Jan-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ ∈ ((V × V) ∖ 𝑅) ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ 𝑅))
Theorem	vvdifopab 38895*	Ordered-pair class abstraction defined by a negation. (Contributed by Peter Mazsa, 25-Jun-2019.)
⊢ ((V × V) ∖ {⟨𝑥, 𝑦⟩ ∣ 𝜑}) = {⟨𝑥, 𝑦⟩ ∣ ¬ 𝜑}
Theorem	brvdif 38896	Binary relation with universal complement is the negation of the relation. (Contributed by Peter Mazsa, 1-Jul-2018.)
⊢ (𝐴(V ∖ 𝑅)𝐵 ↔ ¬ 𝐴𝑅𝐵)
Theorem	brvdif2 38897	Binary relation with universal complement. (Contributed by Peter Mazsa, 14-Jul-2018.)
⊢ (𝐴(V ∖ 𝑅)𝐵 ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
Theorem	brvvdif 38898	Binary relation with the complement under the universal class of ordered pairs. (Contributed by Peter Mazsa, 9-Nov-2018.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴((V × V) ∖ 𝑅)𝐵 ↔ ¬ 𝐴𝑅𝐵))
Theorem	brvbrvvdif 38899	Binary relation with the complement under the universal class of ordered pairs is the same as with universal complement. (Contributed by Peter Mazsa, 28-Nov-2018.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴((V × V) ∖ 𝑅)𝐵 ↔ 𝐴(V ∖ 𝑅)𝐵))
Theorem	brcnvep 38900	The converse of the binary epsilon relation. (Contributed by Peter Mazsa, 30-Jan-2018.)
⊢ (𝐴 ∈ 𝑉 → (𝐴◡ E 𝐵 ↔ 𝐵 ∈ 𝐴))