![]() |
Metamath
Proof Explorer Theorem List (p. 380 of 486) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30851) |
![]() (30852-32374) |
![]() (32375-48553) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | cers 37901 | Extend the definition of a class to include the equivalence relations on their domain quotients class. |
class Ers | ||
Syntax | werALTV 37902 | 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 | ccomembers 37903 | Extend the definition of a class to include the comember equivalence relations class. |
class CoMembErs | ||
Syntax | wcomember 37904 | 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 37905 | Extend the definition of a class to include the function set class. |
class Funss | ||
Syntax | cfunsALTV 37906 | Extend the definition of a class to include the functions class, i.e., the function relations class. |
class FunsALTV | ||
Syntax | wfunALTV 37907 | 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 37908 | Extend the definition of a class to include the disjoint set class. |
class Disjss | ||
Syntax | cdisjs 37909 | Extend the definition of a class to include the disjoints class, i.e., the disjoint relations class. |
class Disjs | ||
Syntax | wdisjALTV 37910 | 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 37911 | Extend the definition of a class to include the disjoint elements class, i.e., the disjoint element relations class. |
class ElDisjs | ||
Syntax | weldisj 37912 | 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 37913 | Extend the definition of a wff to include the antisymmetry relation predicate. (Read: 𝑅 is an antisymmetric relation.) |
wff AntisymRel 𝑅 | ||
Syntax | cparts 37914 | Extend the definition of a class to include the partitions class, i.e., the partition relations class. |
class Parts | ||
Syntax | wpart 37915 | 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 37916 | Extend the definition of a class to include the member partitions class, i.e., the member partition relations class. |
class MembParts | ||
Syntax | wmembpart 37917 | 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 𝐴 | ||
Theorem | el2v1 37918 | New way (elv 3468, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 23-Oct-2018.) |
⊢ ((𝑥 ∈ V ∧ 𝜑) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | el3v 37919 | New way (elv 3468, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. Inference forms (with ⊢ 𝐴 ∈ V, ⊢ 𝐵 ∈ V and ⊢ 𝐶 ∈ V hypotheses) of the general theorems (proving ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → assertions) may be superfluous. (Contributed by Peter Mazsa, 13-Oct-2018.) |
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → 𝜑) ⇒ ⊢ 𝜑 | ||
Theorem | el3v1 37920 | New way (elv 3468, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 16-Oct-2020.) |
⊢ ((𝑥 ∈ V ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜓 ∧ 𝜒) → 𝜃) | ||
Theorem | el3v2 37921 | New way (elv 3468, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 16-Oct-2020.) |
⊢ ((𝜑 ∧ 𝑦 ∈ V ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜒) → 𝜃) | ||
Theorem | el3v12 37922 | New way (elv 3468, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 11-Jul-2021.) |
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝜒) → 𝜃) ⇒ ⊢ (𝜒 → 𝜃) | ||
Theorem | el3v13 37923 | New way (elv 3468, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 11-Jul-2021.) |
⊢ ((𝑥 ∈ V ∧ 𝜓 ∧ 𝑧 ∈ V) → 𝜃) ⇒ ⊢ (𝜓 → 𝜃) | ||
Theorem | el3v23 37924 | New way (elv 3468, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. (Contributed by Peter Mazsa, 11-Jul-2021.) |
⊢ ((𝜑 ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → 𝜃) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | anan 37925 | Multiple commutations in conjunction. (Contributed by Peter Mazsa, 7-Mar-2020.) |
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ ((𝜑 ∧ 𝜃) ∧ 𝜏)) ↔ ((𝜓 ∧ 𝜃) ∧ (𝜑 ∧ (𝜒 ∧ 𝜏)))) | ||
Theorem | triantru3 37926 | A wff is equivalent to its conjunctions with truths. (Contributed by Peter Mazsa, 30-Nov-2018.) |
⊢ 𝜑 & ⊢ 𝜓 ⇒ ⊢ (𝜒 ↔ (𝜑 ∧ 𝜓 ∧ 𝜒)) | ||
Theorem | bianim 37927 | Exchanging conjunction in a biconditional. (Contributed by Peter Mazsa, 31-Jul-2023.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) & ⊢ (𝜒 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝜑 ↔ (𝜃 ∧ 𝜒)) | ||
Theorem | biorfd 37928 | A wff is equivalent to its disjunction with falsehood, deduction form. (Contributed by Peter Mazsa, 22-Aug-2023.) |
⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → (𝜒 ↔ (𝜓 ∨ 𝜒))) | ||
Theorem | eqbrtr 37929 | Substitution of equal classes in binary relation. (Contributed by Peter Mazsa, 14-Jun-2024.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶) | ||
Theorem | eqbrb 37930 | Substitution of equal classes in a binary relation. (Contributed by Peter Mazsa, 14-Jun-2024.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐴𝑅𝐶) ↔ (𝐴 = 𝐵 ∧ 𝐵𝑅𝐶)) | ||
Theorem | eqeltr 37931 | Substitution of equal classes into element relation. (Contributed by Peter Mazsa, 22-Jul-2017.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶) | ||
Theorem | eqelb 37932 | Substitution of equal classes into element relation. (Contributed by Peter Mazsa, 17-Jul-2019.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐴 ∈ 𝐶) ↔ (𝐴 = 𝐵 ∧ 𝐵 ∈ 𝐶)) | ||
Theorem | eqeqan2d 37933 | Implication of introducing a new equality. (Contributed by Peter Mazsa, 17-Apr-2019.) |
⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ ((𝐴 = 𝐵 ∧ 𝜑) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)) | ||
Theorem | suceqsneq 37934 | One-to-one relationship between the successor operation and the singleton. (Contributed by Peter Mazsa, 31-Dec-2024.) |
⊢ (𝐴 ∈ 𝑉 → (suc 𝐴 = suc 𝐵 ↔ {𝐴} = {𝐵})) | ||
Theorem | sucdifsn2 37935 | Absorption of union with a singleton by difference. (Contributed by Peter Mazsa, 24-Jul-2024.) |
⊢ ((𝐴 ∪ {𝐴}) ∖ {𝐴}) = 𝐴 | ||
Theorem | sucdifsn 37936 | The difference between the successor and the singleton of a class is the class. (Contributed by Peter Mazsa, 20-Sep-2024.) |
⊢ (suc 𝐴 ∖ {𝐴}) = 𝐴 | ||
Theorem | disjresin 37937 | The restriction to a disjoint is the empty class. (Contributed by Peter Mazsa, 24-Jul-2024.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ → (𝑅 ↾ (𝐴 ∩ 𝐵)) = ∅) | ||
Theorem | disjresdisj 37938 | The intersection of restrictions to disjoint is the empty class. (Contributed by Peter Mazsa, 24-Jul-2024.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝑅 ↾ 𝐴) ∩ (𝑅 ↾ 𝐵)) = ∅) | ||
Theorem | disjresdif 37939 | The difference between restrictions to disjoint is the first restriction. (Contributed by Peter Mazsa, 24-Jul-2024.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝑅 ↾ 𝐴) ∖ (𝑅 ↾ 𝐵)) = (𝑅 ↾ 𝐴)) | ||
Theorem | disjresundif 37940 | Lemma for ressucdifsn2 37941. (Contributed by Peter Mazsa, 24-Jul-2024.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝑅 ↾ (𝐴 ∪ 𝐵)) ∖ (𝑅 ↾ 𝐵)) = (𝑅 ↾ 𝐴)) | ||
Theorem | ressucdifsn2 37941 | The difference between restrictions to the successor and the singleton of a class is the restriction to the class, see ressucdifsn 37942. (Contributed by Peter Mazsa, 24-Jul-2024.) |
⊢ ((𝑅 ↾ (𝐴 ∪ {𝐴})) ∖ (𝑅 ↾ {𝐴})) = (𝑅 ↾ 𝐴) | ||
Theorem | ressucdifsn 37942 | The difference between restrictions to the successor and the singleton of a class is the restriction to the class. (Contributed by Peter Mazsa, 20-Sep-2024.) |
⊢ ((𝑅 ↾ suc 𝐴) ∖ (𝑅 ↾ {𝐴})) = (𝑅 ↾ 𝐴) | ||
Theorem | inres2 37943 | Two ways of expressing the restriction of an intersection. (Contributed by Peter Mazsa, 5-Jun-2021.) |
⊢ ((𝑅 ↾ 𝐴) ∩ 𝑆) = ((𝑅 ∩ 𝑆) ↾ 𝐴) | ||
Theorem | coideq 37944 | Equality theorem for composition of two classes. (Contributed by Peter Mazsa, 23-Sep-2021.) |
⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐴) = (𝐵 ∘ 𝐵)) | ||
Theorem | nexmo1 37945 | 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 | ralin 37946 | Restricted universal quantification over intersection. (Contributed by Peter Mazsa, 8-Sep-2023.) |
⊢ (∀𝑥 ∈ (𝐴 ∩ 𝐵)𝜑 ↔ ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝐵 → 𝜑)) | ||
Theorem | r2alan 37947* | Double restricted universal quantification, special case. (Contributed by Peter Mazsa, 17-Jun-2020.) |
⊢ (∀𝑥∀𝑦(((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → 𝜓) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝜓)) | ||
Theorem | ssrabi 37948 | Inference of restricted abstraction subclass from implication. (Contributed by Peter Mazsa, 26-Oct-2022.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓} | ||
Theorem | rabimbieq 37949 | 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 37950* | Intersection with class abstraction. (Contributed by Peter Mazsa, 21-Jul-2021.) |
⊢ 𝐴 = (𝐵 ∩ 𝐶) & ⊢ 𝐵 = {𝑥 ∣ 𝜑} ⇒ ⊢ 𝐴 = {𝑥 ∈ 𝐶 ∣ 𝜑} | ||
Theorem | abeqinbi 37951* | Intersection with class abstraction and equivalent wff's. (Contributed by Peter Mazsa, 21-Jul-2021.) |
⊢ 𝐴 = (𝐵 ∩ 𝐶) & ⊢ 𝐵 = {𝑥 ∣ 𝜑} & ⊢ (𝑥 ∈ 𝐶 → (𝜑 ↔ 𝜓)) ⇒ ⊢ 𝐴 = {𝑥 ∈ 𝐶 ∣ 𝜓} | ||
Theorem | rabeqel 37952* | Class element of a restricted class abstraction. (Contributed by Peter Mazsa, 24-Jul-2021.) |
⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜑} & ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐶 ∈ 𝐵 ↔ (𝜓 ∧ 𝐶 ∈ 𝐴)) | ||
Theorem | eqrelf 37953* | The equality connective between relations. (Contributed by Peter Mazsa, 25-Jun-2019.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝐵 ⇒ ⊢ ((Rel 𝐴 ∧ Rel 𝐵) → (𝐴 = 𝐵 ↔ ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 ↔ 〈𝑥, 𝑦〉 ∈ 𝐵))) | ||
Theorem | br1cnvinxp 37954 | Binary relation on the converse of an intersection with a Cartesian product. (Contributed by Peter Mazsa, 27-Jul-2019.) |
⊢ (𝐶◡(𝑅 ∩ (𝐴 × 𝐵))𝐷 ↔ ((𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐴) ∧ 𝐷𝑅𝐶)) | ||
Theorem | releleccnv 37955 | Elementhood in a converse 𝑅-coset when 𝑅 is a relation. (Contributed by Peter Mazsa, 9-Dec-2018.) |
⊢ (Rel 𝑅 → (𝐴 ∈ [𝐵]◡𝑅 ↔ 𝐴𝑅𝐵)) | ||
Theorem | releccnveq 37956* | Equality of converse 𝑅-coset and converse 𝑆-coset when 𝑅 and 𝑆 are relations. (Contributed by Peter Mazsa, 27-Jul-2019.) |
⊢ ((Rel 𝑅 ∧ Rel 𝑆) → ([𝐴]◡𝑅 = [𝐵]◡𝑆 ↔ ∀𝑥(𝑥𝑅𝐴 ↔ 𝑥𝑆𝐵))) | ||
Theorem | opelvvdif 37957 | Negated elementhood of ordered pair. (Contributed by Peter Mazsa, 14-Jan-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈𝐴, 𝐵〉 ∈ ((V × V) ∖ 𝑅) ↔ ¬ 〈𝐴, 𝐵〉 ∈ 𝑅)) | ||
Theorem | vvdifopab 37958* | Ordered-pair class abstraction defined by a negation. (Contributed by Peter Mazsa, 25-Jun-2019.) |
⊢ ((V × V) ∖ {〈𝑥, 𝑦〉 ∣ 𝜑}) = {〈𝑥, 𝑦〉 ∣ ¬ 𝜑} | ||
Theorem | brvdif 37959 | Binary relation with universal complement is the negation of the relation. (Contributed by Peter Mazsa, 1-Jul-2018.) |
⊢ (𝐴(V ∖ 𝑅)𝐵 ↔ ¬ 𝐴𝑅𝐵) | ||
Theorem | brvdif2 37960 | Binary relation with universal complement. (Contributed by Peter Mazsa, 14-Jul-2018.) |
⊢ (𝐴(V ∖ 𝑅)𝐵 ↔ ¬ 〈𝐴, 𝐵〉 ∈ 𝑅) | ||
Theorem | brvvdif 37961 | Binary relation with the complement under the universal class of ordered pairs. (Contributed by Peter Mazsa, 9-Nov-2018.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴((V × V) ∖ 𝑅)𝐵 ↔ ¬ 𝐴𝑅𝐵)) | ||
Theorem | brvbrvvdif 37962 | 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 37963 | The converse of the binary epsilon relation. (Contributed by Peter Mazsa, 30-Jan-2018.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴◡ E 𝐵 ↔ 𝐵 ∈ 𝐴)) | ||
Theorem | elecALTV 37964 | Elementhood in the 𝑅-coset of 𝐴. Theorem 72 of [Suppes] p. 82. (I think we should replace elecg 8778 with this original form of Suppes. Peter Mazsa). (Contributed by Mario Carneiro, 9-Jul-2014.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐵 ∈ [𝐴]𝑅 ↔ 𝐴𝑅𝐵)) | ||
Theorem | brcnvepres 37965 | Restricted converse epsilon binary relation. (Contributed by Peter Mazsa, 10-Feb-2018.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵(◡ E ↾ 𝐴)𝐶 ↔ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵))) | ||
Theorem | brres2 37966 | Binary relation on a restriction. (Contributed by Peter Mazsa, 2-Jan-2019.) (Revised by Peter Mazsa, 16-Dec-2021.) |
⊢ (𝐵(𝑅 ↾ 𝐴)𝐶 ↔ 𝐵(𝑅 ∩ (𝐴 × ran (𝑅 ↾ 𝐴)))𝐶) | ||
Theorem | br1cnvres 37967 | Binary relation on the converse of a restriction. (Contributed by Peter Mazsa, 27-Jul-2019.) |
⊢ (𝐵 ∈ 𝑉 → (𝐵◡(𝑅 ↾ 𝐴)𝐶 ↔ (𝐶 ∈ 𝐴 ∧ 𝐶𝑅𝐵))) | ||
Theorem | eldmres 37968* | Elementhood in the domain of a restriction. (Contributed by Peter Mazsa, 9-Jan-2019.) |
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom (𝑅 ↾ 𝐴) ↔ (𝐵 ∈ 𝐴 ∧ ∃𝑦 𝐵𝑅𝑦))) | ||
Theorem | elrnres 37969* | Element of the range of a restriction. (Contributed by Peter Mazsa, 26-Dec-2018.) |
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ ran (𝑅 ↾ 𝐴) ↔ ∃𝑥 ∈ 𝐴 𝑥𝑅𝐵)) | ||
Theorem | eldmressnALTV 37970 | Element of the domain of a restriction to a singleton. (Contributed by Peter Mazsa, 12-Jun-2024.) |
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom (𝑅 ↾ {𝐴}) ↔ (𝐵 = 𝐴 ∧ 𝐴 ∈ dom 𝑅))) | ||
Theorem | elrnressn 37971 | Element of the range of a restriction to a singleton. (Contributed by Peter Mazsa, 12-Jun-2024.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐵 ∈ ran (𝑅 ↾ {𝐴}) ↔ 𝐴𝑅𝐵)) | ||
Theorem | eldm4 37972* | Elementhood in a domain. (Contributed by Peter Mazsa, 24-Oct-2018.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom 𝑅 ↔ ∃𝑦 𝑦 ∈ [𝐴]𝑅)) | ||
Theorem | eldmres2 37973* | Elementhood in the domain of a restriction. (Contributed by Peter Mazsa, 21-Aug-2020.) |
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom (𝑅 ↾ 𝐴) ↔ (𝐵 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ [𝐵]𝑅))) | ||
Theorem | eceq1i 37974 | Equality theorem for 𝐶-coset of 𝐴 and 𝐶-coset of 𝐵, inference version. (Contributed by Peter Mazsa, 11-May-2021.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ [𝐴]𝐶 = [𝐵]𝐶 | ||
Theorem | elecres 37975 | Elementhood in the restricted coset of 𝐵. (Contributed by Peter Mazsa, 21-Sep-2018.) |
⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ [𝐵](𝑅 ↾ 𝐴) ↔ (𝐵 ∈ 𝐴 ∧ 𝐵𝑅𝐶))) | ||
Theorem | ecres 37976* | Restricted coset of 𝐵. (Contributed by Peter Mazsa, 9-Dec-2018.) |
⊢ [𝐵](𝑅 ↾ 𝐴) = {𝑥 ∣ (𝐵 ∈ 𝐴 ∧ 𝐵𝑅𝑥)} | ||
Theorem | ecres2 37977 | The restricted coset of 𝐵 when 𝐵 is an element of the restriction. (Contributed by Peter Mazsa, 16-Oct-2018.) |
⊢ (𝐵 ∈ 𝐴 → [𝐵](𝑅 ↾ 𝐴) = [𝐵]𝑅) | ||
Theorem | eccnvepres 37978* | Restricted converse epsilon coset of 𝐵. (Contributed by Peter Mazsa, 11-Feb-2018.) (Revised by Peter Mazsa, 21-Oct-2021.) |
⊢ (𝐵 ∈ 𝑉 → [𝐵](◡ E ↾ 𝐴) = {𝑥 ∈ 𝐵 ∣ 𝐵 ∈ 𝐴}) | ||
Theorem | eleccnvep 37979 | Elementhood in the converse epsilon coset of 𝐴 is elementhood in 𝐴. (Contributed by Peter Mazsa, 27-Jan-2019.) |
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ [𝐴]◡ E ↔ 𝐵 ∈ 𝐴)) | ||
Theorem | eccnvep 37980 | The converse epsilon coset of a set is the set. (Contributed by Peter Mazsa, 27-Jan-2019.) |
⊢ (𝐴 ∈ 𝑉 → [𝐴]◡ E = 𝐴) | ||
Theorem | extep 37981 | Property of epsilon relation, see also extid 38008, extssr 38207 and the comment of df-ssr 38196. (Contributed by Peter Mazsa, 10-Jul-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ([𝐴]◡ E = [𝐵]◡ E ↔ 𝐴 = 𝐵)) | ||
Theorem | disjeccnvep 37982 | Property of the epsilon relation. (Contributed by Peter Mazsa, 27-Apr-2020.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (([𝐴]◡ E ∩ [𝐵]◡ E ) = ∅ ↔ (𝐴 ∩ 𝐵) = ∅)) | ||
Theorem | eccnvepres2 37983 | The restricted converse epsilon coset of an element of the restriction is the element itself. (Contributed by Peter Mazsa, 16-Jul-2019.) |
⊢ (𝐵 ∈ 𝐴 → [𝐵](◡ E ↾ 𝐴) = 𝐵) | ||
Theorem | eccnvepres3 37984 | Condition for a restricted converse epsilon coset of a set to be the set itself. (Contributed by Peter Mazsa, 11-May-2021.) |
⊢ (𝐵 ∈ dom (◡ E ↾ 𝐴) → [𝐵](◡ E ↾ 𝐴) = 𝐵) | ||
Theorem | eldmqsres 37985* | Elementhood in a restricted domain quotient set. (Contributed by Peter Mazsa, 21-Aug-2020.) |
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ (dom (𝑅 ↾ 𝐴) / (𝑅 ↾ 𝐴)) ↔ ∃𝑢 ∈ 𝐴 (∃𝑥 𝑥 ∈ [𝑢]𝑅 ∧ 𝐵 = [𝑢]𝑅))) | ||
Theorem | eldmqsres2 37986* | Elementhood in a restricted domain quotient set. (Contributed by Peter Mazsa, 22-Aug-2020.) |
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ (dom (𝑅 ↾ 𝐴) / (𝑅 ↾ 𝐴)) ↔ ∃𝑢 ∈ 𝐴 ∃𝑥 ∈ [ 𝑢]𝑅𝐵 = [𝑢]𝑅)) | ||
Theorem | qsss1 37987 | Subclass theorem for quotient sets. (Contributed by Peter Mazsa, 12-Sep-2020.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐴 / 𝐶) ⊆ (𝐵 / 𝐶)) | ||
Theorem | qseq1i 37988 | Equality theorem for quotient set, inference form. (Contributed by Peter Mazsa, 3-Jun-2021.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 / 𝐶) = (𝐵 / 𝐶) | ||
Theorem | brinxprnres 37989 | Binary relation on a restriction. (Contributed by Peter Mazsa, 2-Jan-2019.) |
⊢ (𝐶 ∈ 𝑉 → (𝐵(𝑅 ∩ (𝐴 × ran (𝑅 ↾ 𝐴)))𝐶 ↔ (𝐵 ∈ 𝐴 ∧ 𝐵𝑅𝐶))) | ||
Theorem | inxprnres 37990* | Restriction of a class as a class of ordered pairs. (Contributed by Peter Mazsa, 2-Jan-2019.) |
⊢ (𝑅 ∩ (𝐴 × ran (𝑅 ↾ 𝐴))) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥𝑅𝑦)} | ||
Theorem | dfres4 37991 | Alternate definition of the restriction of a class. (Contributed by Peter Mazsa, 2-Jan-2019.) |
⊢ (𝑅 ↾ 𝐴) = (𝑅 ∩ (𝐴 × ran (𝑅 ↾ 𝐴))) | ||
Theorem | exan3 37992* | Equivalent expressions with existential quantification. (Contributed by Peter Mazsa, 10-Sep-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑢(𝐴 ∈ [𝑢]𝑅 ∧ 𝐵 ∈ [𝑢]𝑅) ↔ ∃𝑢(𝑢𝑅𝐴 ∧ 𝑢𝑅𝐵))) | ||
Theorem | exanres 37993* | Equivalent expressions with existential quantification. (Contributed by Peter Mazsa, 2-May-2021.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (∃𝑢(𝑢(𝑅 ↾ 𝐴)𝐵 ∧ 𝑢(𝑆 ↾ 𝐴)𝐶) ↔ ∃𝑢 ∈ 𝐴 (𝑢𝑅𝐵 ∧ 𝑢𝑆𝐶))) | ||
Theorem | exanres3 37994* | Equivalent expressions with restricted existential quantification. (Contributed by Peter Mazsa, 10-Sep-2021.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (∃𝑢 ∈ 𝐴 (𝐵 ∈ [𝑢]𝑅 ∧ 𝐶 ∈ [𝑢]𝑆) ↔ ∃𝑢 ∈ 𝐴 (𝑢𝑅𝐵 ∧ 𝑢𝑆𝐶))) | ||
Theorem | exanres2 37995* | Equivalent expressions with existential quantification. (Contributed by Peter Mazsa, 10-Sep-2021.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (∃𝑢(𝑢(𝑅 ↾ 𝐴)𝐵 ∧ 𝑢(𝑆 ↾ 𝐴)𝐶) ↔ ∃𝑢 ∈ 𝐴 (𝐵 ∈ [𝑢]𝑅 ∧ 𝐶 ∈ [𝑢]𝑆))) | ||
Theorem | cnvepres 37996* | Restricted converse epsilon relation as a class of ordered pairs. (Contributed by Peter Mazsa, 10-Feb-2018.) |
⊢ (◡ E ↾ 𝐴) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥)} | ||
Theorem | eqrel2 37997* | Equality of relations. (Contributed by Peter Mazsa, 8-Mar-2019.) |
⊢ ((Rel 𝐴 ∧ Rel 𝐵) → (𝐴 = 𝐵 ↔ ∀𝑥∀𝑦(𝑥𝐴𝑦 ↔ 𝑥𝐵𝑦))) | ||
Theorem | rncnv 37998 | Range of converse is the domain. (Contributed by Peter Mazsa, 12-Feb-2018.) |
⊢ ran ◡𝐴 = dom 𝐴 | ||
Theorem | dfdm6 37999* | Alternate definition of domain. (Contributed by Peter Mazsa, 2-Mar-2018.) |
⊢ dom 𝑅 = {𝑥 ∣ [𝑥]𝑅 ≠ ∅} | ||
Theorem | dfrn6 38000* | Alternate definition of range. (Contributed by Peter Mazsa, 1-Aug-2018.) |
⊢ ran 𝑅 = {𝑥 ∣ [𝑥]◡𝑅 ≠ ∅} |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |