HomeHome Intuitionistic Logic Explorer
Theorem List (p. 39 of 113)
< Previous  Next >
Bad symbols? Try the
GIF version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 3801-3900   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremdisjeq12d 3801* Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐶 = 𝐷)       (𝜑 → (Disj 𝑥𝐴 𝐶Disj 𝑥𝐵 𝐷))
 
Theoremcbvdisj 3802* Change bound variables in a disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
𝑦𝐵    &   𝑥𝐶    &   (𝑥 = 𝑦𝐵 = 𝐶)       (Disj 𝑥𝐴 𝐵Disj 𝑦𝐴 𝐶)
 
Theoremcbvdisjv 3803* Change bound variables in a disjoint collection. (Contributed by Mario Carneiro, 11-Dec-2016.)
(𝑥 = 𝑦𝐵 = 𝐶)       (Disj 𝑥𝐴 𝐵Disj 𝑦𝐴 𝐶)
 
Theoremnfdisjv 3804* Bound-variable hypothesis builder for disjoint collection. (Contributed by Jim Kingdon, 19-Aug-2018.)
𝑦𝐴    &   𝑦𝐵       𝑦Disj 𝑥𝐴 𝐵
 
Theoremnfdisj1 3805 Bound-variable hypothesis builder for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
𝑥Disj 𝑥𝐴 𝐵
 
Theoreminvdisj 3806* If there is a function 𝐶(𝑦) such that 𝐶(𝑦) = 𝑥 for all 𝑦𝐵(𝑥), then the sets 𝐵(𝑥) for distinct 𝑥𝐴 are disjoint. (Contributed by Mario Carneiro, 10-Dec-2016.)
(∀𝑥𝐴𝑦𝐵 𝐶 = 𝑥Disj 𝑥𝐴 𝐵)
 
Theoremsndisj 3807 Any collection of singletons is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
Disj 𝑥𝐴 {𝑥}
 
Theorem0disj 3808 Any collection of empty sets is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
Disj 𝑥𝐴
 
Theoremdisjxsn 3809* A singleton collection is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
Disj 𝑥 ∈ {𝐴}𝐵
 
Theoremdisjx0 3810 An empty collection is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
Disj 𝑥 ∈ ∅ 𝐵
 
2.1.22  Binary relations
 
Syntaxwbr 3811 Extend wff notation to include the general binary relation predicate. Note that the syntax is simply three class symbols in a row. Since binary relations are the only possible wff expressions consisting of three class expressions in a row, the syntax is unambiguous.
wff 𝐴𝑅𝐵
 
Definitiondf-br 3812 Define a general binary relation. Note that the syntax is simply three class symbols in a row. Definition 6.18 of [TakeutiZaring] p. 29 generalized to arbitrary classes. This definition of relations is well-defined, although not very meaningful, when classes 𝐴 and/or 𝐵 are proper classes (i.e. are not sets). On the other hand, we often find uses for this definition when 𝑅 is a proper class (see for example iprc 4659). (Contributed by NM, 31-Dec-1993.)
(𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
 
Theorembreq 3813 Equality theorem for binary relations. (Contributed by NM, 4-Jun-1995.)
(𝑅 = 𝑆 → (𝐴𝑅𝐵𝐴𝑆𝐵))
 
Theorembreq1 3814 Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)
(𝐴 = 𝐵 → (𝐴𝑅𝐶𝐵𝑅𝐶))
 
Theorembreq2 3815 Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)
(𝐴 = 𝐵 → (𝐶𝑅𝐴𝐶𝑅𝐵))
 
Theorembreq12 3816 Equality theorem for a binary relation. (Contributed by NM, 8-Feb-1996.)
((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝑅𝐶𝐵𝑅𝐷))
 
Theorembreqi 3817 Equality inference for binary relations. (Contributed by NM, 19-Feb-2005.)
𝑅 = 𝑆       (𝐴𝑅𝐵𝐴𝑆𝐵)
 
Theorembreq1i 3818 Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.)
𝐴 = 𝐵       (𝐴𝑅𝐶𝐵𝑅𝐶)
 
Theorembreq2i 3819 Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.)
𝐴 = 𝐵       (𝐶𝑅𝐴𝐶𝑅𝐵)
 
Theorembreq12i 3820 Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Eric Schmidt, 4-Apr-2007.)
𝐴 = 𝐵    &   𝐶 = 𝐷       (𝐴𝑅𝐶𝐵𝑅𝐷)
 
Theorembreq1d 3821 Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
(𝜑𝐴 = 𝐵)       (𝜑 → (𝐴𝑅𝐶𝐵𝑅𝐶))
 
Theorembreqd 3822 Equality deduction for a binary relation. (Contributed by NM, 29-Oct-2011.)
(𝜑𝐴 = 𝐵)       (𝜑 → (𝐶𝐴𝐷𝐶𝐵𝐷))
 
Theorembreq2d 3823 Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
(𝜑𝐴 = 𝐵)       (𝜑 → (𝐶𝑅𝐴𝐶𝑅𝐵))
 
Theorembreq12d 3824 Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐶 = 𝐷)       (𝜑 → (𝐴𝑅𝐶𝐵𝑅𝐷))
 
Theorembreq123d 3825 Equality deduction for a binary relation. (Contributed by NM, 29-Oct-2011.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝑅 = 𝑆)    &   (𝜑𝐶 = 𝐷)       (𝜑 → (𝐴𝑅𝐶𝐵𝑆𝐷))
 
Theorembreqan12d 3826 Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
(𝜑𝐴 = 𝐵)    &   (𝜓𝐶 = 𝐷)       ((𝜑𝜓) → (𝐴𝑅𝐶𝐵𝑅𝐷))
 
Theorembreqan12rd 3827 Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
(𝜑𝐴 = 𝐵)    &   (𝜓𝐶 = 𝐷)       ((𝜓𝜑) → (𝐴𝑅𝐶𝐵𝑅𝐷))
 
Theoremnbrne1 3828 Two classes are different if they don't have the same relationship to a third class. (Contributed by NM, 3-Jun-2012.)
((𝐴𝑅𝐵 ∧ ¬ 𝐴𝑅𝐶) → 𝐵𝐶)
 
Theoremnbrne2 3829 Two classes are different if they don't have the same relationship to a third class. (Contributed by NM, 3-Jun-2012.)
((𝐴𝑅𝐶 ∧ ¬ 𝐵𝑅𝐶) → 𝐴𝐵)
 
Theoremeqbrtri 3830 Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.)
𝐴 = 𝐵    &   𝐵𝑅𝐶       𝐴𝑅𝐶
 
Theoremeqbrtrd 3831 Substitution of equal classes into a binary relation. (Contributed by NM, 8-Oct-1999.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐵𝑅𝐶)       (𝜑𝐴𝑅𝐶)
 
Theoremeqbrtrri 3832 Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.)
𝐴 = 𝐵    &   𝐴𝑅𝐶       𝐵𝑅𝐶
 
Theoremeqbrtrrd 3833 Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐴𝑅𝐶)       (𝜑𝐵𝑅𝐶)
 
Theorembreqtri 3834 Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.)
𝐴𝑅𝐵    &   𝐵 = 𝐶       𝐴𝑅𝐶
 
Theorembreqtrd 3835 Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
(𝜑𝐴𝑅𝐵)    &   (𝜑𝐵 = 𝐶)       (𝜑𝐴𝑅𝐶)
 
Theorembreqtrri 3836 Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.)
𝐴𝑅𝐵    &   𝐶 = 𝐵       𝐴𝑅𝐶
 
Theorembreqtrrd 3837 Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
(𝜑𝐴𝑅𝐵)    &   (𝜑𝐶 = 𝐵)       (𝜑𝐴𝑅𝐶)
 
Theorem3brtr3i 3838 Substitution of equality into both sides of a binary relation. (Contributed by NM, 11-Aug-1999.)
𝐴𝑅𝐵    &   𝐴 = 𝐶    &   𝐵 = 𝐷       𝐶𝑅𝐷
 
Theorem3brtr4i 3839 Substitution of equality into both sides of a binary relation. (Contributed by NM, 11-Aug-1999.)
𝐴𝑅𝐵    &   𝐶 = 𝐴    &   𝐷 = 𝐵       𝐶𝑅𝐷
 
Theorem3brtr3d 3840 Substitution of equality into both sides of a binary relation. (Contributed by NM, 18-Oct-1999.)
(𝜑𝐴𝑅𝐵)    &   (𝜑𝐴 = 𝐶)    &   (𝜑𝐵 = 𝐷)       (𝜑𝐶𝑅𝐷)
 
Theorem3brtr4d 3841 Substitution of equality into both sides of a binary relation. (Contributed by NM, 21-Feb-2005.)
(𝜑𝐴𝑅𝐵)    &   (𝜑𝐶 = 𝐴)    &   (𝜑𝐷 = 𝐵)       (𝜑𝐶𝑅𝐷)
 
Theorem3brtr3g 3842 Substitution of equality into both sides of a binary relation. (Contributed by NM, 16-Jan-1997.)
(𝜑𝐴𝑅𝐵)    &   𝐴 = 𝐶    &   𝐵 = 𝐷       (𝜑𝐶𝑅𝐷)
 
Theorem3brtr4g 3843 Substitution of equality into both sides of a binary relation. (Contributed by NM, 16-Jan-1997.)
(𝜑𝐴𝑅𝐵)    &   𝐶 = 𝐴    &   𝐷 = 𝐵       (𝜑𝐶𝑅𝐷)
 
Theoremsyl5eqbr 3844 B chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)
𝐴 = 𝐵    &   (𝜑𝐵𝑅𝐶)       (𝜑𝐴𝑅𝐶)
 
Theoremsyl5eqbrr 3845 B chained equality inference for a binary relation. (Contributed by NM, 17-Sep-2004.)
𝐵 = 𝐴    &   (𝜑𝐵𝑅𝐶)       (𝜑𝐴𝑅𝐶)
 
Theoremsyl5breq 3846 B chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)
𝐴𝑅𝐵    &   (𝜑𝐵 = 𝐶)       (𝜑𝐴𝑅𝐶)
 
Theoremsyl5breqr 3847 B chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.)
𝐴𝑅𝐵    &   (𝜑𝐶 = 𝐵)       (𝜑𝐴𝑅𝐶)
 
Theoremsyl6eqbr 3848 A chained equality inference for a binary relation. (Contributed by NM, 12-Oct-1999.)
(𝜑𝐴 = 𝐵)    &   𝐵𝑅𝐶       (𝜑𝐴𝑅𝐶)
 
Theoremsyl6eqbrr 3849 A chained equality inference for a binary relation. (Contributed by NM, 4-Jan-2006.)
(𝜑𝐵 = 𝐴)    &   𝐵𝑅𝐶       (𝜑𝐴𝑅𝐶)
 
Theoremsyl6breq 3850 A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)
(𝜑𝐴𝑅𝐵)    &   𝐵 = 𝐶       (𝜑𝐴𝑅𝐶)
 
Theoremsyl6breqr 3851 A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.)
(𝜑𝐴𝑅𝐵)    &   𝐶 = 𝐵       (𝜑𝐴𝑅𝐶)
 
Theoremssbrd 3852 Deduction from a subclass relationship of binary relations. (Contributed by NM, 30-Apr-2004.)
(𝜑𝐴𝐵)       (𝜑 → (𝐶𝐴𝐷𝐶𝐵𝐷))
 
Theoremssbri 3853 Inference from a subclass relationship of binary relations. (Contributed by NM, 28-Mar-2007.) (Revised by Mario Carneiro, 8-Feb-2015.)
𝐴𝐵       (𝐶𝐴𝐷𝐶𝐵𝐷)
 
Theoremnfbrd 3854 Deduction version of bound-variable hypothesis builder nfbr 3855. (Contributed by NM, 13-Dec-2005.) (Revised by Mario Carneiro, 14-Oct-2016.)
(𝜑𝑥𝐴)    &   (𝜑𝑥𝑅)    &   (𝜑𝑥𝐵)       (𝜑 → Ⅎ𝑥 𝐴𝑅𝐵)
 
Theoremnfbr 3855 Bound-variable hypothesis builder for binary relation. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 14-Oct-2016.)
𝑥𝐴    &   𝑥𝑅    &   𝑥𝐵       𝑥 𝐴𝑅𝐵
 
Theorembrab1 3856* Relationship between a binary relation and a class abstraction. (Contributed by Andrew Salmon, 8-Jul-2011.)
(𝑥𝑅𝐴𝑥 ∈ {𝑧𝑧𝑅𝐴})
 
Theorembrun 3857 The union of two binary relations. (Contributed by NM, 21-Dec-2008.)
(𝐴(𝑅𝑆)𝐵 ↔ (𝐴𝑅𝐵𝐴𝑆𝐵))
 
Theorembrin 3858 The intersection of two relations. (Contributed by FL, 7-Oct-2008.)
(𝐴(𝑅𝑆)𝐵 ↔ (𝐴𝑅𝐵𝐴𝑆𝐵))
 
Theorembrdif 3859 The difference of two binary relations. (Contributed by Scott Fenton, 11-Apr-2011.)
(𝐴(𝑅𝑆)𝐵 ↔ (𝐴𝑅𝐵 ∧ ¬ 𝐴𝑆𝐵))
 
Theoremsbcbrg 3860 Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
(𝐴𝐷 → ([𝐴 / 𝑥]𝐵𝑅𝐶𝐴 / 𝑥𝐵𝐴 / 𝑥𝑅𝐴 / 𝑥𝐶))
 
Theoremsbcbr12g 3861* Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.)
(𝐴𝐷 → ([𝐴 / 𝑥]𝐵𝑅𝐶𝐴 / 𝑥𝐵𝑅𝐴 / 𝑥𝐶))
 
Theoremsbcbr1g 3862* Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.)
(𝐴𝐷 → ([𝐴 / 𝑥]𝐵𝑅𝐶𝐴 / 𝑥𝐵𝑅𝐶))
 
Theoremsbcbr2g 3863* Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.)
(𝐴𝐷 → ([𝐴 / 𝑥]𝐵𝑅𝐶𝐵𝑅𝐴 / 𝑥𝐶))
 
2.1.23  Ordered-pair class abstractions (class builders)
 
Syntaxcopab 3864 Extend class notation to include ordered-pair class abstraction (class builder).
class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
 
Syntaxcmpt 3865 Extend the definition of a class to include maps-to notation for defining a function via a rule.
class (𝑥𝐴𝐵)
 
Definitiondf-opab 3866* Define the class abstraction of a collection of ordered pairs. Definition 3.3 of [Monk1] p. 34. Usually 𝑥 and 𝑦 are distinct, although the definition doesn't strictly require it. The brace notation is called "class abstraction" by Quine; it is also (more commonly) called a "class builder" in the literature. (Contributed by NM, 4-Jul-1994.)
{⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
 
Definitiondf-mpt 3867* Define maps-to notation for defining a function via a rule. Read as "the function defined by the map from 𝑥 (in 𝐴) to 𝐵(𝑥)." The class expression 𝐵 is the value of the function at 𝑥 and normally contains the variable 𝑥. Similar to the definition of mapping in [ChoquetDD] p. 2. (Contributed by NM, 17-Feb-2008.)
(𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
 
Theoremopabss 3868* The collection of ordered pairs in a class is a subclass of it. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
{⟨𝑥, 𝑦⟩ ∣ 𝑥𝑅𝑦} ⊆ 𝑅
 
Theoremopabbid 3869 Equivalent wff's yield equal ordered-pair class abstractions (deduction rule). (Contributed by NM, 21-Feb-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
𝑥𝜑    &   𝑦𝜑    &   (𝜑 → (𝜓𝜒))       (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑥, 𝑦⟩ ∣ 𝜒})
 
Theoremopabbidv 3870* Equivalent wff's yield equal ordered-pair class abstractions (deduction rule). (Contributed by NM, 15-May-1995.)
(𝜑 → (𝜓𝜒))       (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑥, 𝑦⟩ ∣ 𝜒})
 
Theoremopabbii 3871 Equivalent wff's yield equal class abstractions. (Contributed by NM, 15-May-1995.)
(𝜑𝜓)       {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓}
 
Theoremnfopab 3872* Bound-variable hypothesis builder for class abstraction. (Contributed by NM, 1-Sep-1999.) (Unnecessary distinct variable restrictions were removed by Andrew Salmon, 11-Jul-2011.)
𝑧𝜑       𝑧{⟨𝑥, 𝑦⟩ ∣ 𝜑}
 
Theoremnfopab1 3873 The first abstraction variable in an ordered-pair class abstraction (class builder) is effectively not free. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 14-Oct-2016.)
𝑥{⟨𝑥, 𝑦⟩ ∣ 𝜑}
 
Theoremnfopab2 3874 The second abstraction variable in an ordered-pair class abstraction (class builder) is effectively not free. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 14-Oct-2016.)
𝑦{⟨𝑥, 𝑦⟩ ∣ 𝜑}
 
Theoremcbvopab 3875* Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 14-Sep-2003.)
𝑧𝜑    &   𝑤𝜑    &   𝑥𝜓    &   𝑦𝜓    &   ((𝑥 = 𝑧𝑦 = 𝑤) → (𝜑𝜓))       {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑧, 𝑤⟩ ∣ 𝜓}
 
Theoremcbvopabv 3876* Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 15-Oct-1996.)
((𝑥 = 𝑧𝑦 = 𝑤) → (𝜑𝜓))       {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑧, 𝑤⟩ ∣ 𝜓}
 
Theoremcbvopab1 3877* Change first bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 6-Oct-2004.) (Revised by Mario Carneiro, 14-Oct-2016.)
𝑧𝜑    &   𝑥𝜓    &   (𝑥 = 𝑧 → (𝜑𝜓))       {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑧, 𝑦⟩ ∣ 𝜓}
 
Theoremcbvopab2 3878* Change second bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 22-Aug-2013.)
𝑧𝜑    &   𝑦𝜓    &   (𝑦 = 𝑧 → (𝜑𝜓))       {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑧⟩ ∣ 𝜓}
 
Theoremcbvopab1s 3879* Change first bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 31-Jul-2003.)
{⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑧, 𝑦⟩ ∣ [𝑧 / 𝑥]𝜑}
 
Theoremcbvopab1v 3880* Rule used to change the first bound variable in an ordered pair abstraction, using implicit substitution. (Contributed by NM, 31-Jul-2003.) (Proof shortened by Eric Schmidt, 4-Apr-2007.)
(𝑥 = 𝑧 → (𝜑𝜓))       {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑧, 𝑦⟩ ∣ 𝜓}
 
Theoremcbvopab2v 3881* Rule used to change the second bound variable in an ordered pair abstraction, using implicit substitution. (Contributed by NM, 2-Sep-1999.)
(𝑦 = 𝑧 → (𝜑𝜓))       {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑧⟩ ∣ 𝜓}
 
Theoremcsbopabg 3882* Move substitution into a class abstraction. (Contributed by NM, 6-Aug-2007.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
(𝐴𝑉𝐴 / 𝑥{⟨𝑦, 𝑧⟩ ∣ 𝜑} = {⟨𝑦, 𝑧⟩ ∣ [𝐴 / 𝑥]𝜑})
 
Theoremunopab 3883 Union of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002.)
({⟨𝑥, 𝑦⟩ ∣ 𝜑} ∪ {⟨𝑥, 𝑦⟩ ∣ 𝜓}) = {⟨𝑥, 𝑦⟩ ∣ (𝜑𝜓)}
 
Theoremmpteq12f 3884 An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
((∀𝑥 𝐴 = 𝐶 ∧ ∀𝑥𝐴 𝐵 = 𝐷) → (𝑥𝐴𝐵) = (𝑥𝐶𝐷))
 
Theoremmpteq12dva 3885* An equality inference for the maps to notation. (Contributed by Mario Carneiro, 26-Jan-2017.)
(𝜑𝐴 = 𝐶)    &   ((𝜑𝑥𝐴) → 𝐵 = 𝐷)       (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐶𝐷))
 
Theoremmpteq12dv 3886* An equality inference for the maps to notation. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 16-Dec-2013.)
(𝜑𝐴 = 𝐶)    &   (𝜑𝐵 = 𝐷)       (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐶𝐷))
 
Theoremmpteq12 3887* An equality theorem for the maps to notation. (Contributed by NM, 16-Dec-2013.)
((𝐴 = 𝐶 ∧ ∀𝑥𝐴 𝐵 = 𝐷) → (𝑥𝐴𝐵) = (𝑥𝐶𝐷))
 
Theoremmpteq1 3888* An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
(𝐴 = 𝐵 → (𝑥𝐴𝐶) = (𝑥𝐵𝐶))
 
Theoremmpteq1d 3889* An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 11-Jun-2016.)
(𝜑𝐴 = 𝐵)       (𝜑 → (𝑥𝐴𝐶) = (𝑥𝐵𝐶))
 
Theoremmpteq2ia 3890 An equality inference for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
(𝑥𝐴𝐵 = 𝐶)       (𝑥𝐴𝐵) = (𝑥𝐴𝐶)
 
Theoremmpteq2i 3891 An equality inference for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
𝐵 = 𝐶       (𝑥𝐴𝐵) = (𝑥𝐴𝐶)
 
Theoremmpteq12i 3892 An equality inference for the maps to notation. (Contributed by Scott Fenton, 27-Oct-2010.) (Revised by Mario Carneiro, 16-Dec-2013.)
𝐴 = 𝐶    &   𝐵 = 𝐷       (𝑥𝐴𝐵) = (𝑥𝐶𝐷)
 
Theoremmpteq2da 3893 Slightly more general equality inference for the maps to notation. (Contributed by FL, 14-Sep-2013.) (Revised by Mario Carneiro, 16-Dec-2013.)
𝑥𝜑    &   ((𝜑𝑥𝐴) → 𝐵 = 𝐶)       (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
 
Theoremmpteq2dva 3894* Slightly more general equality inference for the maps to notation. (Contributed by Scott Fenton, 25-Apr-2012.)
((𝜑𝑥𝐴) → 𝐵 = 𝐶)       (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
 
Theoremmpteq2dv 3895* An equality inference for the maps to notation. (Contributed by Mario Carneiro, 23-Aug-2014.)
(𝜑𝐵 = 𝐶)       (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
 
Theoremnfmpt 3896* Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.)
𝑥𝐴    &   𝑥𝐵       𝑥(𝑦𝐴𝐵)
 
Theoremnfmpt1 3897 Bound-variable hypothesis builder for the maps-to notation. (Contributed by FL, 17-Feb-2008.)
𝑥(𝑥𝐴𝐵)
 
Theoremcbvmpt 3898* Rule to change the bound variable in a maps-to function, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. (Contributed by NM, 11-Sep-2011.)
𝑦𝐵    &   𝑥𝐶    &   (𝑥 = 𝑦𝐵 = 𝐶)       (𝑥𝐴𝐵) = (𝑦𝐴𝐶)
 
Theoremcbvmptv 3899* Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by Mario Carneiro, 19-Feb-2013.)
(𝑥 = 𝑦𝐵 = 𝐶)       (𝑥𝐴𝐵) = (𝑦𝐴𝐶)
 
Theoremmptv 3900* Function with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013.)
(𝑥 ∈ V ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ 𝑦 = 𝐵}
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11266
  Copyright terms: Public domain < Previous  Next >