Home | Metamath
Proof Explorer Theorem List (p. 341 of 426) | < 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: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | eqeltr 34001 | Substitution of equal classes into elementhood relation. (Contributed by Peter Mazsa, 22-Jul-2017.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶) | ||
Theorem | eqelb 34002 | Substitution of equal classes into elementhood relation. (Contributed by Peter Mazsa, 17-Jul-2019.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐴 ∈ 𝐶) ↔ (𝐴 = 𝐵 ∧ 𝐵 ∈ 𝐶)) | ||
Theorem | eqeqan1d 34003 | Implication of introducing a new equality. (Contributed by Peter Mazsa, 17-Apr-2019.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ ((𝜑 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)) | ||
Theorem | eqeqan2d 34004 | Implication of introducing a new equality. (Contributed by Peter Mazsa, 17-Apr-2019.) |
⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ ((𝐴 = 𝐵 ∧ 𝜑) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)) | ||
Theorem | ineqcom 34005 | Two ways of saying that two classes are disjoint (when 𝐶 = ∅: ((𝐴 ∩ 𝐵) = ∅ ↔ (𝐵 ∩ 𝐴) = ∅)). (Contributed by Peter Mazsa, 22-Mar-2017.) |
⊢ ((𝐴 ∩ 𝐵) = 𝐶 ↔ (𝐵 ∩ 𝐴) = 𝐶) | ||
Theorem | ineqcomi 34006 | Disjointness inference (when 𝐶 = ∅), inference form of ineqcom 34005. (Contributed by Peter Mazsa, 26-Mar-2017.) |
⊢ (𝐴 ∩ 𝐵) = 𝐶 ⇒ ⊢ (𝐵 ∩ 𝐴) = 𝐶 | ||
Theorem | inres2 34007 | Two ways of expressing the restriction of an intersection. (Contributed by Peter Mazsa, 5-Jun-2021.) |
⊢ ((𝑅 ↾ 𝐴) ∩ 𝑆) = ((𝑅 ∩ 𝑆) ↾ 𝐴) | ||
Theorem | ssbr 34008 | Subclass theorem for binary relation, in a more searchable form: (𝑅 ⊆ 𝑆 → (𝐴𝑅𝐵 → 𝐴𝑆𝐵)). (Contributed by Peter Mazsa, 11-Nov-2019.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐶𝐴𝐷 → 𝐶𝐵𝐷)) | ||
Theorem | coideq 34009 | Equality theorem for composition of two classes. (Contributed by Peter Mazsa, 23-Sep-2021.) |
⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐴) = (𝐵 ∘ 𝐵)) | ||
Theorem | ralanid 34010 | Cancellation law for restriction. (Contributed by Peter Mazsa, 30-Dec-2018.) |
⊢ (∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | nexmo 34011 | 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 | 3albii 34012 | Inference adding three universal quantifiers to both sides of an equivalence. (Contributed by Peter Mazsa, 10-Aug-2018.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∀𝑥∀𝑦∀𝑧𝜑 ↔ ∀𝑥∀𝑦∀𝑧𝜓) | ||
Theorem | 3ralbii 34013 | Inference adding three restricted universal quantifiers to both sides of an equivalence. (Contributed by Peter Mazsa, 25-Jul-2019.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓) | ||
Theorem | rabbii 34014 | Equivalent wff's correspond to equal restricted class abstractions. (Contributed by Peter Mazsa, 1-Nov-2019.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓} | ||
Theorem | rabbieq 34015 | Equivalent wff's correspond to restricted class abstractions which are equal with the same class. (Contributed by Peter Mazsa, 8-Jul-2019.) |
⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜑} & ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜓} | ||
Theorem | rabimbieq 34016 | 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 34017* | Intersection with class abstraction. (Contributed by Peter Mazsa, 21-Jul-2021.) |
⊢ 𝐴 = (𝐵 ∩ 𝐶) & ⊢ 𝐵 = {𝑥 ∣ 𝜑} ⇒ ⊢ 𝐴 = {𝑥 ∈ 𝐶 ∣ 𝜑} | ||
Theorem | abeqinbi 34018* | Intersection with class abstraction and equivalent wff's. (Contributed by Peter Mazsa, 21-Jul-2021.) |
⊢ 𝐴 = (𝐵 ∩ 𝐶) & ⊢ 𝐵 = {𝑥 ∣ 𝜑} & ⊢ (𝑥 ∈ 𝐶 → (𝜑 ↔ 𝜓)) ⇒ ⊢ 𝐴 = {𝑥 ∈ 𝐶 ∣ 𝜓} | ||
Theorem | rabeqel 34019* | Class element of a restricted class abstraction. (Contributed by Peter Mazsa, 24-Jul-2021.) |
⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜑} & ⊢ (𝑥 = 𝐶 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐶 ∈ 𝐵 ↔ (𝜓 ∧ 𝐶 ∈ 𝐴)) | ||
Theorem | eqrelf 34020* | The equality connective between relations. (Contributed by Peter Mazsa, 25-Jun-2019.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝐵 ⇒ ⊢ ((Rel 𝐴 ∧ Rel 𝐵) → (𝐴 = 𝐵 ↔ ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 ↔ 〈𝑥, 𝑦〉 ∈ 𝐵))) | ||
Theorem | releleccnv 34021 | Elementhood in a converse 𝑅-coset when 𝑅 is a relation. (Contributed by Peter Mazsa, 9-Dec-2018.) |
⊢ (Rel 𝑅 → (𝐴 ∈ [𝐵]◡𝑅 ↔ 𝐴𝑅𝐵)) | ||
Theorem | releccnveq 34022* | Equality of converse 𝑅-coset and converse 𝑆-coset when 𝑅 and 𝑆 are relations. (Contributed by Peter Mazsa, 27-Jul-2019.) |
⊢ ((Rel 𝑅 ∧ Rel 𝑆) → ([𝐴]◡𝑅 = [𝐵]◡𝑆 ↔ ∀𝑥(𝑥𝑅𝐴 ↔ 𝑥𝑆𝐵))) | ||
Theorem | opelvvdif 34023 | Negated elementhood of ordered pair. (Contributed by Peter Mazsa, 14-Jan-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈𝐴, 𝐵〉 ∈ ((V × V) ∖ 𝑅) ↔ ¬ 〈𝐴, 𝐵〉 ∈ 𝑅)) | ||
Theorem | vvdifopab 34024* | Ordered-pair class abstraction defined by a negation. (Contributed by Peter Mazsa, 25-Jun-2019.) |
⊢ ((V × V) ∖ {〈𝑥, 𝑦〉 ∣ 𝜑}) = {〈𝑥, 𝑦〉 ∣ ¬ 𝜑} | ||
Theorem | brvdif 34025 | Binary relation with universal complement is the negation of the relation. (Contributed by Peter Mazsa, 1-Jul-2018.) |
⊢ (𝐴(V ∖ 𝑅)𝐵 ↔ ¬ 𝐴𝑅𝐵) | ||
Theorem | brvdif2 34026 | Binary relation with universal complement. (Contributed by Peter Mazsa, 14-Jul-2018.) |
⊢ (𝐴(V ∖ 𝑅)𝐵 ↔ ¬ 〈𝐴, 𝐵〉 ∈ 𝑅) | ||
Theorem | brvvdif 34027 | Binary relation with the complement under the universal class of ordered pairs. (Contributed by Peter Mazsa, 9-Nov-2018.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴((V × V) ∖ 𝑅)𝐵 ↔ ¬ 𝐴𝑅𝐵)) | ||
Theorem | brvbrvvdif 34028 | 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 34029 | The converse of the binary epsilon relation. (Contributed by Peter Mazsa, 30-Jan-2018.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴◡ E 𝐵 ↔ 𝐵 ∈ 𝐴)) | ||
Theorem | elecALTV 34030 | Elementhood in the 𝑅-coset of 𝐴. Theorem 72 of [Suppes] p. 82. (I think we should replace elecg 7785 with this original form of Suppes. Peter Mazsa) (Contributed by Mario Carneiro, 9-Jul-2014.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐵 ∈ [𝐴]𝑅 ↔ 𝐴𝑅𝐵)) | ||
Theorem | opelresALTV 34031 | Ordered pair elementhood in a restriction. Exercise 13 of [TakeutiZaring] p. 25. (Contributed by NM, 13-Nov-1995.) |
⊢ (𝐶 ∈ 𝑉 → (〈𝐵, 𝐶〉 ∈ (𝑅 ↾ 𝐴) ↔ (𝐵 ∈ 𝐴 ∧ 〈𝐵, 𝐶〉 ∈ 𝑅))) | ||
Theorem | brresALTV 34032 | Binary relation on a restriction. (Contributed by Mario Carneiro, 4-Nov-2015.) |
⊢ (𝐶 ∈ 𝑉 → (𝐵(𝑅 ↾ 𝐴)𝐶 ↔ (𝐵 ∈ 𝐴 ∧ 𝐵𝑅𝐶))) | ||
Theorem | brcnvepres 34033 | Restricted converse epsilon binary relation. (Contributed by Peter Mazsa, 10-Feb-2018.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐵(◡ E ↾ 𝐴)𝐶 ↔ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵))) | ||
Theorem | brinxp2ALTV 34034 | Intersection with cross product binary relation . (Contributed by NM, 3-Mar-2007.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ (𝐶(𝑅 ∩ (𝐴 × 𝐵))𝐷 ↔ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) ∧ 𝐶𝑅𝐷)) | ||
Theorem | brres2 34035 | Binary relation on a restriction. (Contributed by Peter Mazsa, 2-Jan-2019.) (Revised by Peter Mazsa, 16-Dec-2021.) |
⊢ (𝐵(𝑅 ↾ 𝐴)𝐶 ↔ 𝐵(𝑅 ∩ (𝐴 × ran (𝑅 ↾ 𝐴)))𝐶) | ||
Theorem | eldmres 34036* | Elementhood in the domain of a restriction. (Contributed by Peter Mazsa, 9-Jan-2019.) |
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom (𝑅 ↾ 𝐴) ↔ (𝐵 ∈ 𝐴 ∧ ∃𝑦 𝐵𝑅𝑦))) | ||
Theorem | eldm4 34037* | Elementhood in a domain. (Contributed by Peter Mazsa, 24-Oct-2018.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom 𝑅 ↔ ∃𝑦 𝑦 ∈ [𝐴]𝑅)) | ||
Theorem | eldmres2 34038* | Elementhood in the domain of a restriction. (Contributed by Peter Mazsa, 21-Aug-2020.) |
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ dom (𝑅 ↾ 𝐴) ↔ (𝐵 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ [𝐵]𝑅))) | ||
Theorem | eceq1i 34039 | Equality theorem for 𝐶-coset of 𝐴 and 𝐶-coset of 𝐵, inference version. (Contributed by Peter Mazsa, 11-May-2021.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ [𝐴]𝐶 = [𝐵]𝐶 | ||
Theorem | eceq2i 34040 | Equality theorem for the 𝐴-coset and 𝐵-coset of 𝐶, inference version. (Contributed by Peter Mazsa, 11-May-2021.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ [𝐶]𝐴 = [𝐶]𝐵 | ||
Theorem | eceq2d 34041 | Equality theorem for the 𝐴-coset and 𝐵-coset of 𝐶, deduction version. (Contributed by Peter Mazsa, 23-Apr-2021.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → [𝐶]𝐴 = [𝐶]𝐵) | ||
Theorem | elecres 34042 | Elementhood in the restricted coset of 𝐵. (Contributed by Peter Mazsa, 21-Sep-2018.) |
⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ [𝐵](𝑅 ↾ 𝐴) ↔ (𝐵 ∈ 𝐴 ∧ 𝐵𝑅𝐶))) | ||
Theorem | ecres 34043* | Restricted coset of 𝐵. (Contributed by Peter Mazsa, 9-Dec-2018.) |
⊢ [𝐵](𝑅 ↾ 𝐴) = {𝑥 ∣ (𝐵 ∈ 𝐴 ∧ 𝐵𝑅𝑥)} | ||
Theorem | ecres2 34044 | The restricted coset of 𝐵 when 𝐵 is an element of the restriction. (Contributed by Peter Mazsa, 16-Oct-2018.) |
⊢ (𝐵 ∈ 𝐴 → [𝐵](𝑅 ↾ 𝐴) = [𝐵]𝑅) | ||
Theorem | eccnvepres 34045* | Restricted converse epsilon coset of 𝐵. (Contributed by Peter Mazsa, 11-Feb-2018.) (Revised by Peter Mazsa, 21-Oct-2021.) |
⊢ (𝐵 ∈ 𝑉 → [𝐵](◡ E ↾ 𝐴) = {𝑥 ∈ 𝐵 ∣ 𝐵 ∈ 𝐴}) | ||
Theorem | eleccnvep 34046 | Elementhood in the converse epsilon coset of 𝐴 is elementhood in 𝐴. (Contributed by Peter Mazsa, 27-Jan-2019.) |
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ [𝐴]◡ E ↔ 𝐵 ∈ 𝐴)) | ||
Theorem | eccnvep 34047 | The converse epsilon coset of a set is the set. (Contributed by Peter Mazsa, 27-Jan-2019.) |
⊢ (𝐴 ∈ 𝑉 → [𝐴]◡ E = 𝐴) | ||
Theorem | extep 34048 | Property of epsilon relation, cf. extid 34081, ~? extssr and the comment of ~? df-ssr . (Contributed by Peter Mazsa, 10-Jul-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ([𝐴]◡ E = [𝐵]◡ E ↔ 𝐴 = 𝐵)) | ||
Theorem | eccnvepres2 34049 | 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 34050 | 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 34051* | Elementhood in a restricted domain quotient set. (Contributed by Peter Mazsa, 21-Aug-2020.) |
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ (dom (𝑅 ↾ 𝐴) / (𝑅 ↾ 𝐴)) ↔ ∃𝑢 ∈ 𝐴 (∃𝑥 𝑥 ∈ [𝑢]𝑅 ∧ 𝐵 = [𝑢]𝑅))) | ||
Theorem | eldmqsres2 34052* | Elementhood in a restricted domain quotient set. (Contributed by Peter Mazsa, 22-Aug-2020.) |
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ (dom (𝑅 ↾ 𝐴) / (𝑅 ↾ 𝐴)) ↔ ∃𝑢 ∈ 𝐴 ∃𝑥 ∈ [ 𝑢]𝑅𝐵 = [𝑢]𝑅)) | ||
Theorem | qsss1 34053 | Subclass theorem for quotient sets. (Contributed by Peter Mazsa, 12-Sep-2020.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐴 / 𝐶) ⊆ (𝐵 / 𝐶)) | ||
Theorem | qseq1i 34054 | Equality theorem for quotient set, inference form. (Contributed by Peter Mazsa, 3-Jun-2021.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 / 𝐶) = (𝐵 / 𝐶) | ||
Theorem | qseq1d 34055 | Equality theorem for quotient set, deduction form. (Contributed by Peter Mazsa, 27-May-2021.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 / 𝐶) = (𝐵 / 𝐶)) | ||
Theorem | qseq2i 34056 | Equality theorem for quotient set, inference form. (Contributed by Peter Mazsa, 3-Jun-2021.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 / 𝐴) = (𝐶 / 𝐵) | ||
Theorem | qseq2d 34057 | Equality theorem for quotient set, deduction form. (Contributed by Peter Mazsa, 27-May-2021.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 / 𝐴) = (𝐶 / 𝐵)) | ||
Theorem | qseq12 34058 | Equality theorem for quotient set. (Contributed by Peter Mazsa, 17-Apr-2019.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 / 𝐶) = (𝐵 / 𝐷)) | ||
Theorem | brinxprnres 34059 | Binary relation on a restriction. (Contributed by Peter Mazsa, 2-Jan-2019.) |
⊢ (𝐶 ∈ 𝑉 → (𝐵(𝑅 ∩ (𝐴 × ran (𝑅 ↾ 𝐴)))𝐶 ↔ (𝐵 ∈ 𝐴 ∧ 𝐵𝑅𝐶))) | ||
Theorem | inxprnres 34060* | Restriction of a class as a class of ordered pairs. (Contributed by Peter Mazsa, 2-Jan-2019.) |
⊢ (𝑅 ∩ (𝐴 × ran (𝑅 ↾ 𝐴))) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥𝑅𝑦)} | ||
Theorem | dfres4 34061 | Alternate definition of the restriction of a class. (Contributed by Peter Mazsa, 2-Jan-2019.) |
⊢ (𝑅 ↾ 𝐴) = (𝑅 ∩ (𝐴 × ran (𝑅 ↾ 𝐴))) | ||
Theorem | exan3 34062* | Equivalent expressions with existential quantification. (Contributed by Peter Mazsa, 10-Sep-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑢(𝐴 ∈ [𝑢]𝑅 ∧ 𝐵 ∈ [𝑢]𝑅) ↔ ∃𝑢(𝑢𝑅𝐴 ∧ 𝑢𝑅𝐵))) | ||
Theorem | exanres 34063* | Equivalent expressions with existential quantification. (Contributed by Peter Mazsa, 2-May-2021.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (∃𝑢(𝑢(𝑅 ↾ 𝐴)𝐵 ∧ 𝑢(𝑆 ↾ 𝐴)𝐶) ↔ ∃𝑢 ∈ 𝐴 (𝑢𝑅𝐵 ∧ 𝑢𝑆𝐶))) | ||
Theorem | exanres3 34064* | Equivalent expressions with restricted existential quantification. (Contributed by Peter Mazsa, 10-Sep-2021.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (∃𝑢 ∈ 𝐴 (𝐵 ∈ [𝑢]𝑅 ∧ 𝐶 ∈ [𝑢]𝑆) ↔ ∃𝑢 ∈ 𝐴 (𝑢𝑅𝐵 ∧ 𝑢𝑆𝐶))) | ||
Theorem | exanres2 34065* | Equivalent expressions with existential quantification. (Contributed by Peter Mazsa, 10-Sep-2021.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (∃𝑢(𝑢(𝑅 ↾ 𝐴)𝐵 ∧ 𝑢(𝑆 ↾ 𝐴)𝐶) ↔ ∃𝑢 ∈ 𝐴 (𝐵 ∈ [𝑢]𝑅 ∧ 𝐶 ∈ [𝑢]𝑆))) | ||
Theorem | cnvepres 34066* | Restricted converse epsilon relation as a class of ordered pairs. (Contributed by Peter Mazsa, 10-Feb-2018.) |
⊢ (◡ E ↾ 𝐴) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥)} | ||
Theorem | ssrel3 34067* | Subclass relation in another form when the subclass is a relation. (Contributed by Peter Mazsa, 16-Feb-2019.) |
⊢ (Rel 𝐴 → (𝐴 ⊆ 𝐵 ↔ ∀𝑥∀𝑦(𝑥𝐴𝑦 → 𝑥𝐵𝑦))) | ||
Theorem | eqrel2 34068* | Equality of relations. (Contributed by Peter Mazsa, 8-Mar-2019.) |
⊢ ((Rel 𝐴 ∧ Rel 𝐵) → (𝐴 = 𝐵 ↔ ∀𝑥∀𝑦(𝑥𝐴𝑦 ↔ 𝑥𝐵𝑦))) | ||
Theorem | relinxp 34069 | Intersection with a Cartesian product is a relation. (Contributed by Peter Mazsa, 4-Mar-2019.) |
⊢ Rel (𝑅 ∩ (𝐴 × 𝐵)) | ||
Theorem | rncnv 34070 | Range of converse is the domain. (Contributed by Peter Mazsa, 12-Feb-2018.) |
⊢ ran ◡𝐴 = dom 𝐴 | ||
Theorem | dfdm6 34071* | Alternate definition of domain. (Contributed by Peter Mazsa, 2-Mar-2018.) |
⊢ dom 𝑅 = {𝑥 ∣ [𝑥]𝑅 ≠ ∅} | ||
Theorem | dfrn6 34072* | Alternate definition of range. (Contributed by Peter Mazsa, 1-Aug-2018.) |
⊢ ran 𝑅 = {𝑥 ∣ [𝑥]◡𝑅 ≠ ∅} | ||
Theorem | rncnvepres 34073 | The range of the restricted converse epsilon is the union of the restriction. (Contributed by Peter Mazsa, 11-Feb-2018.) (Revised by Peter Mazsa, 26-Sep-2021.) |
⊢ ran (◡ E ↾ 𝐴) = ∪ 𝐴 | ||
Theorem | dmecd 34074 | Equality of the coset of 𝐵 and the coset of 𝐶 implies equivalence of domain elementhood (equivalence is not necessary as opposed to ereldm 7790). (Contributed by Peter Mazsa, 9-Oct-2018.) |
⊢ (𝜑 → dom 𝑅 = 𝐴) & ⊢ (𝜑 → [𝐵]𝑅 = [𝐶]𝑅) ⇒ ⊢ (𝜑 → (𝐵 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴)) | ||
Theorem | dmec2d 34075 | Equality of the coset of 𝐵 and the coset of 𝐶 implies equivalence of domain elementhood (equivalence is not necessary as opposed to ereldm 7790). (Contributed by Peter Mazsa, 12-Oct-2018.) |
⊢ (𝜑 → [𝐵]𝑅 = [𝐶]𝑅) ⇒ ⊢ (𝜑 → (𝐵 ∈ dom 𝑅 ↔ 𝐶 ∈ dom 𝑅)) | ||
Theorem | inxpssres 34076 | Intersection with a Cartesian product is a subclass of restriction. (Contributed by Peter Mazsa, 19-Jul-2019.) |
⊢ (𝑅 ∩ (𝐴 × 𝐵)) ⊆ (𝑅 ↾ 𝐴) | ||
Theorem | brid 34077 | Property of the identity binary relation. (Contributed by Peter Mazsa, 18-Dec-2021.) |
⊢ (𝐴 I 𝐵 ↔ 𝐵 I 𝐴) | ||
Theorem | ideq2 34078 | For sets, the identity binary relation is the same as equality. (Contributed by Peter Mazsa, 24-Jun-2020.) (Revised by Peter Mazsa, 18-Dec-2021.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 I 𝐵 ↔ 𝐴 = 𝐵)) | ||
Theorem | idresssidinxp 34079 | Condition for the identity restriction to be a subclass of identity intersection with a Cartesian product. (Contributed by Peter Mazsa, 19-Jul-2018.) |
⊢ (𝐴 ⊆ 𝐵 → ( I ↾ 𝐴) ⊆ ( I ∩ (𝐴 × 𝐵))) | ||
Theorem | idreseqidinxp 34080 | Condition for the identity restriction to be equal to the identity intersection with a Cartesian product. (Contributed by Peter Mazsa, 19-Jul-2018.) |
⊢ (𝐴 ⊆ 𝐵 → ( I ∩ (𝐴 × 𝐵)) = ( I ↾ 𝐴)) | ||
Theorem | extid 34081 | Property of identity relation, cf. extep 34048, ~? extssr and the comment of ~? df-ssr . (Contributed by Peter Mazsa, 5-Jul-2019.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴]◡ I = [𝐵]◡ I ↔ 𝐴 = 𝐵)) | ||
Theorem | inxpss 34082* | Two ways to say that an intersection with a Cartesian product is a subclass. (Contributed by Peter Mazsa, 16-Jul-2019.) |
⊢ ((𝑅 ∩ (𝐴 × 𝐵)) ⊆ 𝑆 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 → 𝑥𝑆𝑦)) | ||
Theorem | idinxpss 34083* | Two ways to say that an intersection of the identity relation with a Cartesian product is a subclass. (Contributed by Peter Mazsa, 16-Jul-2019.) |
⊢ (( I ∩ (𝐴 × 𝐵)) ⊆ 𝑅 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 = 𝑦 → 𝑥𝑅𝑦)) | ||
Theorem | inxpss3 34084* | Two ways to say that an intersection with a Cartesian product is a subclass (cf. inxpss 34082). (Contributed by Peter Mazsa, 8-Mar-2019.) |
⊢ (∀𝑥∀𝑦(𝑥(𝑅 ∩ (𝐴 × 𝐵))𝑦 → 𝑥(𝑆 ∩ (𝐴 × 𝐵))𝑦) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 → 𝑥𝑆𝑦)) | ||
Theorem | inxpss2 34085* | Two ways to say that intersections with Cartesian products are in a subclass relation. (Contributed by Peter Mazsa, 8-Mar-2019.) |
⊢ ((𝑅 ∩ (𝐴 × 𝐵)) ⊆ (𝑆 ∩ (𝐴 × 𝐵)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 → 𝑥𝑆𝑦)) | ||
Theorem | inxpssidinxp 34086* | Two ways to say that intersections with Cartesian products are in a subclass relation, special case of inxpss2 34085. (Contributed by Peter Mazsa, 4-Jul-2019.) |
⊢ ((𝑅 ∩ (𝐴 × 𝐵)) ⊆ ( I ∩ (𝐴 × 𝐵)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 → 𝑥 = 𝑦)) | ||
Theorem | idinxpssinxp 34087* | Two ways to say that intersections with Cartesian products are in a subclass relation, special case of inxpss2 34085. (Contributed by Peter Mazsa, 6-Mar-2019.) |
⊢ (( I ∩ (𝐴 × 𝐵)) ⊆ (𝑅 ∩ (𝐴 × 𝐵)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 = 𝑦 → 𝑥𝑅𝑦)) | ||
Theorem | idinxpres 34088 | The intersection of the identity function with a square cross product. (Contributed by FL, 2-Aug-2009.) |
⊢ ( I ∩ (𝐴 × 𝐴)) = ( I ↾ 𝐴) | ||
Theorem | idinxpssinxp2 34089* | Identity intersection with a square Cartesian product in subclass relation with an intersection with the same Cartesian product. (Contributed by Peter Mazsa, 4-Mar-2019.) |
⊢ (( I ∩ (𝐴 × 𝐴)) ⊆ (𝑅 ∩ (𝐴 × 𝐴)) ↔ ∀𝑥 ∈ 𝐴 𝑥𝑅𝑥) | ||
Theorem | idinxpssinxp3 34090 | Identity intersection with a square Cartesian product in subclass relation with an intersection with the same Cartesian product. (Contributed by Peter Mazsa, 16-Mar-2019.) |
⊢ (( I ∩ (𝐴 × 𝐴)) ⊆ (𝑅 ∩ (𝐴 × 𝐴)) ↔ ( I ↾ 𝐴) ⊆ 𝑅) | ||
Theorem | idinxpssinxp4 34091* | Identity intersection with a square Cartesian product in subclass relation with an intersection with the same Cartesian product (cf. idinxpssinxp2 34089). (Contributed by Peter Mazsa, 8-Mar-2019.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 = 𝑦 → 𝑥𝑅𝑦) ↔ ∀𝑥 ∈ 𝐴 𝑥𝑅𝑥) | ||
Theorem | relcnveq3 34092* | Two ways of saying a relation is symmetric. (Contributed by FL, 31-Aug-2009.) |
⊢ (Rel 𝑅 → (𝑅 = ◡𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥))) | ||
Theorem | relcnveq 34093 | Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 23-Aug-2018.) |
⊢ (Rel 𝑅 → (◡𝑅 ⊆ 𝑅 ↔ ◡𝑅 = 𝑅)) | ||
Theorem | relcnveq2 34094* | Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 28-Apr-2019.) |
⊢ (Rel 𝑅 → (◡𝑅 = 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥))) | ||
Theorem | relcnveq4 34095* | Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 28-Apr-2019.) |
⊢ (Rel 𝑅 → (◡𝑅 ⊆ 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥))) | ||
Theorem | qsresid 34096 | Simplification of a special quotient set. (Contributed by Peter Mazsa, 2-Sep-2020.) |
⊢ (𝐴 / (𝑅 ↾ 𝐴)) = (𝐴 / 𝑅) | ||
Theorem | nel02 34097 | The empty set has no elements. (Contributed by Peter Mazsa, 4-Jan-2018.) |
⊢ (𝐴 = ∅ → ¬ 𝐵 ∈ 𝐴) | ||
Theorem | n0elqs 34098 | Two ways of expressing that the empty set is not an element of a quotient set. (Contributed by Peter Mazsa, 5-Dec-2019.) |
⊢ (¬ ∅ ∈ (𝐴 / 𝑅) ↔ 𝐴 ⊆ dom 𝑅) | ||
Theorem | n0elqs2 34099 | Two ways of expressing that the empty set is not an element of a quotient set. (Contributed by Peter Mazsa, 25-Jul-2021.) |
⊢ (¬ ∅ ∈ (𝐴 / 𝑅) ↔ dom (𝑅 ↾ 𝐴) = 𝐴) | ||
Theorem | ecex2 34100 | Condition for a coset to be a set. (Contributed by Peter Mazsa, 4-May-2019.) |
⊢ ((𝑅 ↾ 𝐴) ∈ 𝑉 → (𝐵 ∈ 𝐴 → [𝐵]𝑅 ∈ V)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |