![]() |
Metamath
Proof Explorer Theorem List (p. 59 of 480) | < 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-30209) |
![]() (30210-31732) |
![]() (31733-47936) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | relsng 5801 | A singleton is a relation iff it is a singleton on an ordered pair. (Contributed by NM, 24-Sep-2013.) (Revised by BJ, 12-Feb-2022.) |
⊢ (𝐴 ∈ 𝑉 → (Rel {𝐴} ↔ 𝐴 ∈ (V × V))) | ||
Theorem | relsnb 5802 | An at-most-singleton is a relation iff it is empty (because it is a "singleton on a proper class") or it is a singleton of an ordered pair. (Contributed by BJ, 26-Feb-2023.) |
⊢ (Rel {𝐴} ↔ (¬ 𝐴 ∈ V ∨ 𝐴 ∈ (V × V))) | ||
Theorem | relsnopg 5803 | A singleton of an ordered pair is a relation. (Contributed by NM, 17-May-1998.) (Revised by BJ, 12-Feb-2022.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → Rel {⟨𝐴, 𝐵⟩}) | ||
Theorem | relsn 5804 | A singleton is a relation iff it is an ordered pair. (Contributed by NM, 24-Sep-2013.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (Rel {𝐴} ↔ 𝐴 ∈ (V × V)) | ||
Theorem | relsnop 5805 | A singleton of an ordered pair is a relation. (Contributed by NM, 17-May-1998.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ Rel {⟨𝐴, 𝐵⟩} | ||
Theorem | copsex2gb 5806* | Implicit substitution inference for ordered pairs. Compare copsex2ga 5807. (Contributed by NM, 12-Mar-2014.) |
⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜓) ↔ (𝐴 ∈ (V × V) ∧ 𝜑)) | ||
Theorem | copsex2ga 5807* | Implicit substitution inference for ordered pairs. Compare copsex2g 5493. (Contributed by NM, 26-Feb-2014.) (Proof shortened by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ (𝑉 × 𝑊) → (𝜑 ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜓))) | ||
Theorem | elopaba 5808* | Membership in an ordered-pair class abstraction. (Contributed by NM, 25-Feb-2014.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜓} ↔ (𝐴 ∈ (V × V) ∧ 𝜑)) | ||
Theorem | xpsspw 5809 | A Cartesian product is included in the power of the power of the union of its arguments. (Contributed by NM, 13-Sep-2006.) |
⊢ (𝐴 × 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝐵) | ||
Theorem | unixpss 5810 | The double class union of a Cartesian product is included in the union of its arguments. (Contributed by NM, 16-Sep-2006.) |
⊢ ∪ ∪ (𝐴 × 𝐵) ⊆ (𝐴 ∪ 𝐵) | ||
Theorem | relun 5811 | The union of two relations is a relation. Compare Exercise 5 of [TakeutiZaring] p. 25. (Contributed by NM, 12-Aug-1994.) |
⊢ (Rel (𝐴 ∪ 𝐵) ↔ (Rel 𝐴 ∧ Rel 𝐵)) | ||
Theorem | relin1 5812 | The intersection with a relation is a relation. (Contributed by NM, 16-Aug-1994.) |
⊢ (Rel 𝐴 → Rel (𝐴 ∩ 𝐵)) | ||
Theorem | relin2 5813 | The intersection with a relation is a relation. (Contributed by NM, 17-Jan-2006.) |
⊢ (Rel 𝐵 → Rel (𝐴 ∩ 𝐵)) | ||
Theorem | relinxp 5814 | Intersection with a Cartesian product is a relation. (Contributed by Peter Mazsa, 4-Mar-2019.) |
⊢ Rel (𝑅 ∩ (𝐴 × 𝐵)) | ||
Theorem | reldif 5815 | A difference cutting down a relation is a relation. (Contributed by NM, 31-Mar-1998.) |
⊢ (Rel 𝐴 → Rel (𝐴 ∖ 𝐵)) | ||
Theorem | reliun 5816 | An indexed union is a relation iff each member of its indexed family is a relation. (Contributed by NM, 19-Dec-2008.) |
⊢ (Rel ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 Rel 𝐵) | ||
Theorem | reliin 5817 | An indexed intersection is a relation if at least one of the member of the indexed family is a relation. (Contributed by NM, 8-Mar-2014.) |
⊢ (∃𝑥 ∈ 𝐴 Rel 𝐵 → Rel ∩ 𝑥 ∈ 𝐴 𝐵) | ||
Theorem | reluni 5818* | The union of a class is a relation iff any member is a relation. Exercise 6 of [TakeutiZaring] p. 25 and its converse. (Contributed by NM, 13-Aug-2004.) |
⊢ (Rel ∪ 𝐴 ↔ ∀𝑥 ∈ 𝐴 Rel 𝑥) | ||
Theorem | relint 5819* | The intersection of a class is a relation if at least one member is a relation. (Contributed by NM, 8-Mar-2014.) |
⊢ (∃𝑥 ∈ 𝐴 Rel 𝑥 → Rel ∩ 𝐴) | ||
Theorem | relopabiv 5820* | A class of ordered pairs is a relation. For a version without a disjoint variable condition, but a longer proof using ax-11 2154 and ax-12 2171, see relopabi 5822. (Contributed by BJ, 22-Jul-2023.) |
⊢ 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⇒ ⊢ Rel 𝐴 | ||
Theorem | relopabv 5821* | A class of ordered pairs is a relation. For a version without a disjoint variable condition, but using ax-11 2154 and ax-12 2171, see relopab 5824. (Contributed by SN, 8-Sep-2024.) |
⊢ Rel {⟨𝑥, 𝑦⟩ ∣ 𝜑} | ||
Theorem | relopabi 5822 | A class of ordered pairs is a relation. (Contributed by Mario Carneiro, 21-Dec-2013.) Remove dependency on ax-sep 5299, ax-nul 5306, ax-pr 5427. (Revised by KP, 25-Oct-2021.) |
⊢ 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⇒ ⊢ Rel 𝐴 | ||
Theorem | relopabiALT 5823 | Alternate proof of relopabi 5822 (shorter but uses more axioms). (Contributed by Mario Carneiro, 21-Dec-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⇒ ⊢ Rel 𝐴 | ||
Theorem | relopab 5824 | A class of ordered pairs is a relation. (Contributed by NM, 8-Mar-1995.) Remove disjoint variable conditions. (Revised by Alan Sare, 9-Jul-2013.) (Proof shortened by Mario Carneiro, 21-Dec-2013.) |
⊢ Rel {⟨𝑥, 𝑦⟩ ∣ 𝜑} | ||
Theorem | mptrel 5825 | The maps-to notation always describes a binary relation. (Contributed by Scott Fenton, 16-Apr-2012.) |
⊢ Rel (𝑥 ∈ 𝐴 ↦ 𝐵) | ||
Theorem | reli 5826 | The identity relation is a relation. Part of Exercise 4.12(p) of [Mendelson] p. 235. (Contributed by NM, 26-Apr-1998.) (Revised by Mario Carneiro, 21-Dec-2013.) |
⊢ Rel I | ||
Theorem | rele 5827 | The membership relation is a relation. (Contributed by NM, 26-Apr-1998.) (Revised by Mario Carneiro, 21-Dec-2013.) |
⊢ Rel E | ||
Theorem | opabid2 5828* | A relation expressed as an ordered pair abstraction. (Contributed by NM, 11-Dec-2006.) |
⊢ (Rel 𝐴 → {⟨𝑥, 𝑦⟩ ∣ ⟨𝑥, 𝑦⟩ ∈ 𝐴} = 𝐴) | ||
Theorem | inopab 5829* | Intersection of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002.) |
⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ∩ {⟨𝑥, 𝑦⟩ ∣ 𝜓}) = {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∧ 𝜓)} | ||
Theorem | difopab 5830* | Difference of two ordered-pair class abstractions. (Contributed by Stefan O'Rear, 17-Jan-2015.) (Proof shortened by SN, 19-Dec-2024.) |
⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ∖ {⟨𝑥, 𝑦⟩ ∣ 𝜓}) = {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∧ ¬ 𝜓)} | ||
Theorem | difopabOLD 5831* | Obsolete version of difopab 5830 as of 19-Dec-2024. (Contributed by Stefan O'Rear, 17-Jan-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ∖ {⟨𝑥, 𝑦⟩ ∣ 𝜓}) = {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∧ ¬ 𝜓)} | ||
Theorem | inxp 5832 | Intersection of two Cartesian products. Exercise 9 of [TakeutiZaring] p. 25. (Contributed by NM, 3-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ ((𝐴 × 𝐵) ∩ (𝐶 × 𝐷)) = ((𝐴 ∩ 𝐶) × (𝐵 ∩ 𝐷)) | ||
Theorem | xpindi 5833 | Distributive law for Cartesian product over intersection. Theorem 102 of [Suppes] p. 52. (Contributed by NM, 26-Sep-2004.) |
⊢ (𝐴 × (𝐵 ∩ 𝐶)) = ((𝐴 × 𝐵) ∩ (𝐴 × 𝐶)) | ||
Theorem | xpindir 5834 | Distributive law for Cartesian product over intersection. Similar to Theorem 102 of [Suppes] p. 52. (Contributed by NM, 26-Sep-2004.) |
⊢ ((𝐴 ∩ 𝐵) × 𝐶) = ((𝐴 × 𝐶) ∩ (𝐵 × 𝐶)) | ||
Theorem | xpiindi 5835* | Distributive law for Cartesian product over indexed intersection. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ (𝐴 ≠ ∅ → (𝐶 × ∩ 𝑥 ∈ 𝐴 𝐵) = ∩ 𝑥 ∈ 𝐴 (𝐶 × 𝐵)) | ||
Theorem | xpriindi 5836* | Distributive law for Cartesian product over relativized indexed intersection. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ (𝐶 × (𝐷 ∩ ∩ 𝑥 ∈ 𝐴 𝐵)) = ((𝐶 × 𝐷) ∩ ∩ 𝑥 ∈ 𝐴 (𝐶 × 𝐵)) | ||
Theorem | eliunxp 5837* | Membership in a union of Cartesian products. Analogue of elxp 5699 for nonconstant 𝐵(𝑥). (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ (𝐶 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ ∃𝑥∃𝑦(𝐶 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) | ||
Theorem | opeliunxp2 5838* | Membership in a union of Cartesian products. (Contributed by Mario Carneiro, 14-Feb-2015.) |
⊢ (𝑥 = 𝐶 → 𝐵 = 𝐸) ⇒ ⊢ (⟨𝐶, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸)) | ||
Theorem | raliunxp 5839* | Write a double restricted quantification as one universal quantifier. In this version of ralxp 5841, 𝐵(𝑦) is not assumed to be constant. (Contributed by Mario Carneiro, 29-Dec-2014.) |
⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜓) | ||
Theorem | rexiunxp 5840* | Write a double restricted quantification as one universal quantifier. In this version of rexxp 5842, 𝐵(𝑦) is not assumed to be constant. (Contributed by Mario Carneiro, 14-Feb-2015.) |
⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ({𝑦} × 𝐵)𝜑 ↔ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝜓) | ||
Theorem | ralxp 5841* | Universal quantification restricted to a Cartesian product is equivalent to a double restricted quantification. The hypothesis specifies an implicit substitution. (Contributed by NM, 7-Feb-2004.) (Revised by Mario Carneiro, 29-Dec-2014.) |
⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ (𝐴 × 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜓) | ||
Theorem | rexxp 5842* | Existential quantification restricted to a Cartesian product is equivalent to a double restricted quantification. (Contributed by NM, 11-Nov-1995.) (Revised by Mario Carneiro, 14-Feb-2015.) |
⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ (𝐴 × 𝐵)𝜑 ↔ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝜓) | ||
Theorem | exopxfr 5843* | Transfer ordered-pair existence from/to single variable existence. (Contributed by NM, 26-Feb-2014.) (Proof shortened by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ (V × V)𝜑 ↔ ∃𝑦∃𝑧𝜓) | ||
Theorem | exopxfr2 5844* | Transfer ordered-pair existence from/to single variable existence. (Contributed by NM, 26-Feb-2014.) |
⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝜑 ↔ 𝜓)) ⇒ ⊢ (Rel 𝐴 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦∃𝑧(⟨𝑦, 𝑧⟩ ∈ 𝐴 ∧ 𝜓))) | ||
Theorem | djussxp 5845* | Disjoint union is a subset of a Cartesian product. (Contributed by Stefan O'Rear, 21-Nov-2014.) |
⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ⊆ (𝐴 × V) | ||
Theorem | ralxpf 5846* | Version of ralxp 5841 with bound-variable hypotheses. (Contributed by NM, 18-Aug-2006.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ (𝐴 × 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜓) | ||
Theorem | rexxpf 5847* | Version of rexxp 5842 with bound-variable hypotheses. (Contributed by NM, 19-Dec-2008.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ (𝐴 × 𝐵)𝜑 ↔ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐵 𝜓) | ||
Theorem | iunxpf 5848* | Indexed union on a Cartesian product equals a double indexed union. The hypothesis specifies an implicit substitution. (Contributed by NM, 19-Dec-2008.) |
⊢ Ⅎ𝑦𝐶 & ⊢ Ⅎ𝑧𝐶 & ⊢ Ⅎ𝑥𝐷 & ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → 𝐶 = 𝐷) ⇒ ⊢ ∪ 𝑥 ∈ (𝐴 × 𝐵)𝐶 = ∪ 𝑦 ∈ 𝐴 ∪ 𝑧 ∈ 𝐵 𝐷 | ||
Theorem | opabbi2dv 5849* | Deduce equality of a relation and an ordered-pair class abstraction. Compare eqabdv 2867. (Contributed by NM, 24-Feb-2014.) |
⊢ Rel 𝐴 & ⊢ (𝜑 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ 𝜓)) ⇒ ⊢ (𝜑 → 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝜓}) | ||
Theorem | relop 5850* | A necessary and sufficient condition for a Kuratowski ordered pair to be a relation. (Contributed by NM, 3-Jun-2008.) A relation is a class of ordered pairs, so the fact that an ordered pair may sometimes be itself a relation is an "accident" depending on the specific encoding of ordered pairs as classes (in set.mm, the Kuratowski encoding). A more meaningful statement is relsnopg 5803, as funsng 6599 is to funop 7149. (New usage is discouraged.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (Rel ⟨𝐴, 𝐵⟩ ↔ ∃𝑥∃𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})) | ||
Theorem | ideqg 5851 | For sets, the identity relation is the same as equality. (Contributed by NM, 30-Apr-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 I 𝐵 ↔ 𝐴 = 𝐵)) | ||
Theorem | ideq 5852 | For sets, the identity relation is the same as equality. (Contributed by NM, 13-Aug-1995.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 I 𝐵 ↔ 𝐴 = 𝐵) | ||
Theorem | ididg 5853 | A set is identical to itself. (Contributed by NM, 28-May-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ (𝐴 ∈ 𝑉 → 𝐴 I 𝐴) | ||
Theorem | issetid 5854 | Two ways of expressing set existence. (Contributed by NM, 16-Feb-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ (𝐴 ∈ V ↔ 𝐴 I 𝐴) | ||
Theorem | coss1 5855 | Subclass theorem for composition. (Contributed by FL, 30-Dec-2010.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∘ 𝐶) ⊆ (𝐵 ∘ 𝐶)) | ||
Theorem | coss2 5856 | Subclass theorem for composition. (Contributed by NM, 5-Apr-2013.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∘ 𝐴) ⊆ (𝐶 ∘ 𝐵)) | ||
Theorem | coeq1 5857 | Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.) |
⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶)) | ||
Theorem | coeq2 5858 | Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.) |
⊢ (𝐴 = 𝐵 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵)) | ||
Theorem | coeq1i 5859 | Equality inference for composition of two classes. (Contributed by NM, 16-Nov-2000.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶) | ||
Theorem | coeq2i 5860 | Equality inference for composition of two classes. (Contributed by NM, 16-Nov-2000.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵) | ||
Theorem | coeq1d 5861 | Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶)) | ||
Theorem | coeq2d 5862 | Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵)) | ||
Theorem | coeq12i 5863 | Equality inference for composition of two classes. (Contributed by FL, 7-Jun-2012.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐷) | ||
Theorem | coeq12d 5864 | Equality deduction for composition of two classes. (Contributed by FL, 7-Jun-2012.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐷)) | ||
Theorem | nfco 5865 | Bound-variable hypothesis builder for function value. (Contributed by NM, 1-Sep-1999.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝐴 ∘ 𝐵) | ||
Theorem | brcog 5866* | Ordered pair membership in a composition. (Contributed by NM, 24-Feb-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵))) | ||
Theorem | opelco2g 5867* | Ordered pair membership in a composition. (Contributed by NM, 27-Jan-1997.) (Revised by Mario Carneiro, 24-Feb-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ ∈ (𝐶 ∘ 𝐷) ↔ ∃𝑥(⟨𝐴, 𝑥⟩ ∈ 𝐷 ∧ ⟨𝑥, 𝐵⟩ ∈ 𝐶))) | ||
Theorem | brcogw 5868 | Ordered pair membership in a composition. (Contributed by Thierry Arnoux, 14-Jan-2018.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑋 ∈ 𝑍) ∧ (𝐴𝐷𝑋 ∧ 𝑋𝐶𝐵)) → 𝐴(𝐶 ∘ 𝐷)𝐵) | ||
Theorem | eqbrrdva 5869* | Deduction from extensionality principle for relations, given an equivalence only on the relation domain and range. (Contributed by Thierry Arnoux, 28-Nov-2017.) |
⊢ (𝜑 → 𝐴 ⊆ (𝐶 × 𝐷)) & ⊢ (𝜑 → 𝐵 ⊆ (𝐶 × 𝐷)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (𝑥𝐴𝑦 ↔ 𝑥𝐵𝑦)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | brco 5870* | Binary relation on a composition. (Contributed by NM, 21-Sep-2004.) (Revised by Mario Carneiro, 24-Feb-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵)) | ||
Theorem | opelco 5871* | Ordered pair membership in a composition. (Contributed by NM, 27-Dec-1996.) (Revised by Mario Carneiro, 24-Feb-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 ∘ 𝐷) ↔ ∃𝑥(𝐴𝐷𝑥 ∧ 𝑥𝐶𝐵)) | ||
Theorem | cnvss 5872 | Subset theorem for converse. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Kyle Wyonch, 27-Apr-2021.) |
⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵) | ||
Theorem | cnveq 5873 | Equality theorem for converse relation. (Contributed by NM, 13-Aug-1995.) |
⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵) | ||
Theorem | cnveqi 5874 | Equality inference for converse relation. (Contributed by NM, 23-Dec-2008.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ◡𝐴 = ◡𝐵 | ||
Theorem | cnveqd 5875 | Equality deduction for converse relation. (Contributed by NM, 6-Dec-2013.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ◡𝐴 = ◡𝐵) | ||
Theorem | elcnv 5876* | Membership in a converse relation. Equation 5 of [Suppes] p. 62. (Contributed by NM, 24-Mar-1998.) |
⊢ (𝐴 ∈ ◡𝑅 ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝑦𝑅𝑥)) | ||
Theorem | elcnv2 5877* | Membership in a converse relation. Equation 5 of [Suppes] p. 62. (Contributed by NM, 11-Aug-2004.) |
⊢ (𝐴 ∈ ◡𝑅 ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ ⟨𝑦, 𝑥⟩ ∈ 𝑅)) | ||
Theorem | nfcnv 5878 | Bound-variable hypothesis builder for converse relation. (Contributed by NM, 31-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥◡𝐴 | ||
Theorem | brcnvg 5879 | The converse of a binary relation swaps arguments. Theorem 11 of [Suppes] p. 61. (Contributed by NM, 10-Oct-2005.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴)) | ||
Theorem | opelcnvg 5880 | Ordered-pair membership in converse relation. (Contributed by NM, 13-May-1999.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ ∈ ◡𝑅 ↔ ⟨𝐵, 𝐴⟩ ∈ 𝑅)) | ||
Theorem | opelcnv 5881 | Ordered-pair membership in converse relation. (Contributed by NM, 13-Aug-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (⟨𝐴, 𝐵⟩ ∈ ◡𝑅 ↔ ⟨𝐵, 𝐴⟩ ∈ 𝑅) | ||
Theorem | brcnv 5882 | The converse of a binary relation swaps arguments. Theorem 11 of [Suppes] p. 61. (Contributed by NM, 13-Aug-1995.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴) | ||
Theorem | csbcnv 5883 | Move class substitution in and out of the converse of a relation. Version of csbcnvgALT 5884 without a sethood antecedent but depending on more axioms. (Contributed by Thierry Arnoux, 8-Feb-2017.) (Revised by NM, 23-Aug-2018.) |
⊢ ◡⦋𝐴 / 𝑥⦌𝐹 = ⦋𝐴 / 𝑥⦌◡𝐹 | ||
Theorem | csbcnvgALT 5884 | Move class substitution in and out of the converse of a relation. Version of csbcnv 5883 with a sethood antecedent but depending on fewer axioms. (Contributed by Thierry Arnoux, 8-Feb-2017.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → ◡⦋𝐴 / 𝑥⦌𝐹 = ⦋𝐴 / 𝑥⦌◡𝐹) | ||
Theorem | cnvco 5885 | Distributive law of converse over class composition. Theorem 26 of [Suppes] p. 64. (Contributed by NM, 19-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ ◡(𝐴 ∘ 𝐵) = (◡𝐵 ∘ ◡𝐴) | ||
Theorem | cnvuni 5886* | The converse of a class union is the (indexed) union of the converses of its members. (Contributed by NM, 11-Aug-2004.) |
⊢ ◡∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 ◡𝑥 | ||
Theorem | dfdm3 5887* | Alternate definition of domain. Definition 6.5(1) of [TakeutiZaring] p. 24. (Contributed by NM, 28-Dec-1996.) |
⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴} | ||
Theorem | dfrn2 5888* | Alternate definition of range. Definition 4 of [Suppes] p. 60. (Contributed by NM, 27-Dec-1996.) |
⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} | ||
Theorem | dfrn3 5889* | Alternate definition of range. Definition 6.5(2) of [TakeutiZaring] p. 24. (Contributed by NM, 28-Dec-1996.) |
⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴} | ||
Theorem | elrn2g 5890* | Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ran 𝐵 ↔ ∃𝑥⟨𝑥, 𝐴⟩ ∈ 𝐵)) | ||
Theorem | elrng 5891* | Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ran 𝐵 ↔ ∃𝑥 𝑥𝐵𝐴)) | ||
Theorem | elrn2 5892* | Membership in a range. (Contributed by NM, 10-Jul-1994.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ ran 𝐵 ↔ ∃𝑥⟨𝑥, 𝐴⟩ ∈ 𝐵) | ||
Theorem | elrn 5893* | Membership in a range. (Contributed by NM, 2-Apr-2004.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ ran 𝐵 ↔ ∃𝑥 𝑥𝐵𝐴) | ||
Theorem | ssrelrn 5894* | If a relation is a subset of a cartesian product, then for each element of the range of the relation there is an element of the first set of the cartesian product which is related to the element of the range by the relation. (Contributed by AV, 24-Oct-2020.) |
⊢ ((𝑅 ⊆ (𝐴 × 𝐵) ∧ 𝑌 ∈ ran 𝑅) → ∃𝑎 ∈ 𝐴 𝑎𝑅𝑌) | ||
Theorem | dfdm4 5895 | Alternate definition of domain. (Contributed by NM, 28-Dec-1996.) |
⊢ dom 𝐴 = ran ◡𝐴 | ||
Theorem | dfdmf 5896* | Definition of domain, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 8-Mar-1995.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐴 ⇒ ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} | ||
Theorem | csbdm 5897 | Distribute proper substitution through the domain of a class. (Contributed by Alexander van der Vekens, 23-Jul-2017.) (Revised by NM, 24-Aug-2018.) |
⊢ ⦋𝐴 / 𝑥⦌dom 𝐵 = dom ⦋𝐴 / 𝑥⦌𝐵 | ||
Theorem | eldmg 5898* | Domain membership. Theorem 4 of [Suppes] p. 59. (Contributed by Mario Carneiro, 9-Jul-2014.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦)) | ||
Theorem | eldm2g 5899* | Domain membership. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 27-Jan-1997.) (Revised by Mario Carneiro, 9-Jul-2014.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦⟨𝐴, 𝑦⟩ ∈ 𝐵)) | ||
Theorem | eldm 5900* | Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 2-Apr-2004.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |