Theorem List for New Foundations Explorer - 4801-4900   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremelxp 4801* Membership in a cross product. (Contributed by NM, 4-Jul-1994.)
(A (B × C) ↔ xy(A = x, y (x B y C)))

Theoremelxp2 4802* Membership in a cross product. (Contributed by NM, 23-Feb-2004.)
(A (B × C) ↔ x B y C A = x, y)

Theoremxpeq12 4803 Equality theorem for cross product. (Contributed by FL, 31-Aug-2009.)
((A = B C = D) → (A × C) = (B × D))

Theoremxpeq1i 4804 Equality inference for cross product. (Contributed by NM, 21-Dec-2008.)
A = B       (A × C) = (B × C)

Theoremxpeq2i 4805 Equality inference for cross product. (Contributed by NM, 21-Dec-2008.)
A = B       (C × A) = (C × B)

Theoremxpeq12i 4806 Equality inference for cross product. (Contributed by FL, 31-Aug-2009.)
A = B    &   C = D       (A × C) = (B × D)

Theoremxpeq1d 4807 Equality deduction for cross product. (Contributed by Jeff Madsen, 17-Jun-2010.)
(φA = B)       (φ → (A × C) = (B × C))

Theoremxpeq2d 4808 Equality deduction for cross product. (Contributed by Jeff Madsen, 17-Jun-2010.)
(φA = B)       (φ → (C × A) = (C × B))

Theoremxpeq12d 4809 Equality deduction for cross product. (Contributed by NM, 8-Dec-2013.)
(φA = B)    &   (φC = D)       (φ → (A × C) = (B × D))

Theoremnfxp 4810 Bound-variable hypothesis builder for cross product. (Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro, 15-Oct-2016.)
xA    &   xB       x(A × B)

Theoremopelxp 4811 Ordered pair membership in a cross product. (The proof was shortened by Andrew Salmon, 12-Aug-2011.) (Contributed by NM, 15-Nov-1994.) (Revised by set.mm contributors, 12-Aug-2011.)
(A, B (C × D) ↔ (A C B D))

Theorembrxp 4812 Binary relation on a cross product. (Contributed by NM, 22-Apr-2004.)
(A(C × D)B ↔ (A C B D))

Theoremcsbxpg 4813 Distribute proper substitution through the cross product of two classes. (Contributed by Alan Sare, 10-Nov-2012.)
(A D[A / x](B × C) = ([A / x]B × [A / x]C))

Theoremrabxp 4814* Membership in a class builder restricted to a cross product. (Contributed by NM, 20-Feb-2014.)
(x = y, z → (φψ))       {x (A × B) φ} = {y, z (y A z B ψ)}

Theoremfconstopab 4815* Representation of a constant function using ordered pairs. (Contributed by NM, 12-Oct-1999.)
(A × {B}) = {x, y (x A y = B)}

Theoremvtoclr 4816* Variable to class conversion of transitive relation. (Contributed by NM, 9-Jun-1998.)
((xRy yRz) → xRz)       ((ARB BRC) → ARC)

Theoremxpiundi 4817* Distributive law for cross product over indexed union. (Contributed by set.mm contributors, 26-Apr-2014.) (Revised by Mario Carneiro, 27-Apr-2014.)
(C × x A B) = x A (C × B)

Theoremxpiundir 4818* Distributive law for cross product over indexed union. (Contributed by set.mm contributors, 26-Apr-2014.) (Revised by Mario Carneiro, 27-Apr-2014.)
(x A B × C) = x A (B × C)

Theoremiunxpconst 4819* Membership in a union of cross products when the second factor is constant. (Contributed by Mario Carneiro, 29-Dec-2014.)
x A ({x} × B) = (A × B)

Theoremopeliunxp 4820 Membership in a union of Cartesian products. (Contributed by Mario Carneiro, 29-Dec-2014.) (Revised by Mario Carneiro, 1-Jan-2017.)
(x, C x A ({x} × B) ↔ (x A C B))

Theoremeliunxp 4821* Membership in a union of Cartesian products. Analogue of elxp 4801 for nonconstant B(x). (Contributed by Mario Carneiro, 29-Dec-2014.)
(C x A ({x} × B) ↔ xy(C = x, y (x A y B)))

Theoremopeliunxp2 4822* Membership in a union of Cartesian products. (Contributed by Mario Carneiro, 14-Feb-2015.)
(x = CB = E)       (C, D x A ({x} × B) ↔ (C A D E))

Theoremraliunxp 4823* Write a double restricted quantification as one universal quantifier. In this version of ralxp 4825, B(y) is not assumed to be constant. (Contributed by Mario Carneiro, 29-Dec-2014.)
(x = y, z → (φψ))       (x y A ({y} × B)φy A z B ψ)

Theoremrexiunxp 4824* Write a double restricted quantification as one universal quantifier. In this version of rexxp 4826, B(y) is not assumed to be constant. (Contributed by Mario Carneiro, 14-Feb-2015.)
(x = y, z → (φψ))       (x y A ({y} × B)φy A z B ψ)

Theoremralxp 4825* 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.)
(x = y, z → (φψ))       (x (A × B)φy A z B ψ)

Theoremrexxp 4826* 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.)
(x = y, z → (φψ))       (x (A × B)φy A z B ψ)

Theoremralxpf 4827* Version of ralxp 4825 with bound-variable hypotheses. (Contributed by NM, 18-Aug-2006.) (Revised by set.mm contributors, 20-Dec-2008.)
yφ    &   zφ    &   xψ    &   (x = y, z → (φψ))       (x (A × B)φy A z B ψ)

Theoremrexxpf 4828* Version of rexxp 4826 with bound-variable hypotheses. (Contributed by NM, 19-Dec-2008.)
yφ    &   zφ    &   xψ    &   (x = y, z → (φψ))       (x (A × B)φy A z B ψ)

Theoremiunxpf 4829* Indexed union on a cross product is equals a double indexed union. The hypothesis specifies an implicit substitution. (Contributed by NM, 19-Dec-2008.)
yC    &   zC    &   xD    &   (x = y, zC = D)       x (A × B)C = y A z B D

Theorembrel 4830 Two things in a binary relation belong to the relation's domain. (Contributed by NM, 17-May-1996.)
R (C × D)       (ARB → (A C B D))

Theoremelxp3 4831* Membership in a cross product. (Contributed by NM, 5-Mar-1995.)
(A (B × C) ↔ xy(x, y = A x, y (B × C)))

Theoremxpundi 4832 Distributive law for cross product over union. Theorem 103 of [Suppes] p. 52. (Contributed by NM, 12-Aug-2004.)
(A × (BC)) = ((A × B) ∪ (A × C))

Theoremxpundir 4833 Distributive law for cross product over union. Similar to Theorem 103 of [Suppes] p. 52. (Contributed by NM, 30-Sep-2002.)
((AB) × C) = ((A × C) ∪ (B × C))

Theoremxpun 4834 The cross product of two unions. (Contributed by NM, 12-Aug-2004.)
((AB) × (CD)) = (((A × C) ∪ (A × D)) ∪ ((B × C) ∪ (B × D)))

Theorembrinxp2 4835 Intersection of binary relation with cross product. (Contributed by NM, 3-Mar-2007.)
(A(R ∩ (C × D))B ↔ (A C B D ARB))

Theorembrinxp 4836 Intersection of binary relation with cross product. (Contributed by NM, 9-Mar-1997.)
((A C B D) → (ARBA(R ∩ (C × D))B))

Theoremopabssxp 4837* An abstraction relation is a subset of a related cross product. (Contributed by NM, 16-Jul-1995.)
{x, y ((x A y B) φ)} (A × B)

Theoremoptocl 4838* Implicit substitution of class for ordered pair. (Contributed by NM, 5-Mar-1995.)
D = (B × C)    &   (x, y = A → (φψ))    &   ((x B y C) → φ)       (A Dψ)

Theorem2optocl 4839* Implicit substitution of classes for ordered pairs. (Contributed by NM, 12-Mar-1995.)
R = (C × D)    &   (x, y = A → (φψ))    &   (z, w = B → (ψχ))    &   (((x C y D) (z C w D)) → φ)       ((A R B R) → χ)

Theorem3optocl 4840* Implicit substitution of classes for ordered pairs. (Contributed by NM, 12-Mar-1995.)
R = (D × F)    &   (x, y = A → (φψ))    &   (z, w = B → (ψχ))    &   (v, u = C → (χθ))    &   (((x D y F) (z D w F) (v D u F)) → φ)       ((A R B R C R) → θ)

Theoremopbrop 4841* Ordered pair membership in a relation. Special case. (Contributed by NM, 5-Aug-1995.)
(((z = A w = B) (v = C u = D)) → (φψ))    &   R = {x, y ((x (S × S) y (S × S)) zwvu((x = z, w y = v, u) φ))}       (((A S B S) (C S D S)) → (A, BRC, Dψ))

Theoremxp0r 4842 The cross product with the empty set is empty. Part of Theorem 3.13(ii) of [Monk1] p. 37. (Contributed by NM, 4-Jul-1994.)
( × A) =

Theoremxpvv 4843 The cross product of the universe with itself is the universe. (Contributed by Scott Fenton, 14-Apr-2021.)
(V × V) = V

Theoremssrel 4844* A subclass relationship depends only on a relation's ordered pairs. Theorem 3.2(i) of [Monk1] p. 33. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by NM, 2-Aug-1994.) (Revised by set.mm contributors, 27-Aug-2011.)
(A Bxy(x, y Ax, y B))

Theoremeqrel 4845* Extensionality principle for relations. Theorem 3.2(ii) of [Monk1] p. 33. (Contributed by NM, 2-Aug-1994.) (Revised by Scott Fenton, 14-Apr-2021.)
(A = Bxy(x, y Ax, y B))

Theoremssopr 4846* Subclass principle for operators. (Contributed by Scott Fenton, 19-Apr-2021.)
(A Bxyz(x, y, z Ax, y, z B))

Theoremeqopr 4847* Extensionality principle for operators. (Contributed by Scott Fenton, 19-Apr-2021.)
(A = Bxyz(x, y, z Ax, y, z B))

Theoremrelssi 4848* Inference from subclass principle for relations. (Contributed by NM, 31-Mar-1998.) (Revised by Scott Fenton, 15-Apr-2021.)
(x, y Ax, y B)       A B

Theoremrelssdv 4849* Deduction from subclass principle for relations. (Contributed by set.mm contributors, 11-Sep-2004.) (Revised by Scott Fenton, 16-Apr-2021.)
(φ → (x, y Ax, y B))       (φA B)

Theoremeqrelriv 4850* Inference from extensionality principle for relations. (Contributed by FL, 15-Oct-2012.) (Revised by Scott Fenton, 16-Apr-2021.)
(x, y Ax, y B)       A = B

Theoremeqbrriv 4851* Inference from extensionality principle for relations. (Contributed by NM, 12-Dec-2006.) (Revised by Scott Fenton, 16-Apr-2021.)
(xAyxBy)       A = B

Theoremeqrelrdv 4852* Deduce equality of relations from equivalence of membership. (Contributed by Rodolfo Medina, 10-Oct-2010.) (Revised by Scott Fenton, 16-Apr-2021.)
(φ → (x, y Ax, y B))       (φA = B)

Theoremeqoprriv 4853* Equality inference for operators. (Contributed by Scott Fenton, 19-Apr-2021.)
(x, y, z Ax, y, z B)       A = B

Theoremeqoprrdv 4854* Equality deduction for operators. (Contributed by Scott Fenton, 19-Apr-2021.)
(φ → (x, y, z Ax, y, z B))       (φA = B)

Theoremxpss12 4855 Subset theorem for cross product. Generalization of Theorem 101 of [Suppes] p. 52. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by NM, 26-Aug-1995.) (Revised by set.mm contributors, 27-Aug-2011.)
((A B C D) → (A × C) (B × D))

Theoremxpss1 4856 Subset relation for cross product. (Contributed by Jeff Hankins, 30-Aug-2009.)
(A B → (A × C) (B × C))

Theoremxpss2 4857 Subset relation for cross product. (Contributed by Jeff Hankins, 30-Aug-2009.)
(A B → (C × A) (C × B))

Theorembr1st 4858* Binary relationship equivalence for the 1st function. (Contributed by set.mm contributors, 8-Jan-2015.)
B V       (A1st Bx A = B, x)

Theorembr2nd 4859* Binary relationship equivalence for the 2nd function. (Contributed by set.mm contributors, 8-Jan-2015.)
B V       (A2nd Bx A = x, B)

Theorembrswap2 4860 Binary relationship equivalence for the Swap function. (Contributed by set.mm contributors, 8-Jan-2015.)
B V    &   C V       (A Swap B, CA = C, B)

Theoremopabid2 4861* A relation expressed as an ordered pair abstraction. (Contributed by set.mm contributors, 11-Dec-2006.)
{x, y x, y A} = A

Theoreminopab 4862* Intersection of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002.)
({x, y φ} ∩ {x, y ψ}) = {x, y (φ ψ)}

Theoreminxp 4863 The intersection of two cross products. Exercise 9 of [TakeutiZaring] p. 25. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by NM, 3-Aug-1994.) (Revised by set.mm contributors, 27-Aug-2011.)
((A × B) ∩ (C × D)) = ((AC) × (BD))

Theoremxpindi 4864 Distributive law for cross product over intersection. Theorem 102 of [Suppes] p. 52. (Contributed by NM, 26-Sep-2004.)
(A × (BC)) = ((A × B) ∩ (A × C))

Theoremxpindir 4865 Distributive law for cross product over intersection. Similar to Theorem 102 of [Suppes] p. 52. (Contributed by NM, 26-Sep-2004.)
((AB) × C) = ((A × C) ∩ (B × C))

Theoremopabbi2i 4866* Equality of a class variable and an ordered pair abstractions (inference rule). Compare abbi2i 2464. (Contributed by Scott Fenton, 18-Apr-2021.)
(x, y Aφ)       A = {x, y φ}

Theoremopabbi2dv 4867* Deduce equality of a relation and an ordered-pair class builder. Compare abbi2dv 2468. (Contributed by NM, 24-Feb-2014.)
(φ → (x, y Aψ))       (φA = {x, y ψ})

Theoremideqg 4868 For sets, the identity relation is the same as equality. (Contributed by NM, 30-Apr-2004.) (Revised by set.mm contributors, 27-Aug-2011.)
(B V → (A I BA = B))

Theoremideqg2 4869 For sets, the identity relation is the same as equality. (Contributed by SF, 8-Jan-2015.)
(A V → (A I BA = B))

Theoremideq 4870 For sets, the identity relation is the same as equality. (Contributed by NM, 13-Aug-1995.) (Revised by set.mm contributors, 1-Jun-2008.)
B V       (A I BA = B)

Theoremididg 4871 A set is identical to itself. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by NM, 28-May-2008.) (Revised by set.mm contributors, 27-Aug-2011.)
(A VA I A)

Theoremcoss1 4872 Subclass theorem for composition. (Contributed by FL, 30-Dec-2010.)
(A B → (A C) (B C))

Theoremcoss2 4873 Subclass theorem for composition. (Contributed by set.mm contributors, 5-Apr-2013.)
(A B → (C A) (C B))

Theoremcoeq1 4874 Equality theorem for composition of two classes. (Contributed by set.mm contributors, 3-Jan-1997.)
(A = B → (A C) = (B C))

Theoremcoeq2 4875 Equality theorem for composition of two classes. (Contributed by set.mm contributors, 3-Jan-1997.)
(A = B → (C A) = (C B))

Theoremcoeq1i 4876 Equality inference for composition of two classes. (Contributed by set.mm contributors, 16-Nov-2000.)
A = B       (A C) = (B C)

Theoremcoeq2i 4877 Equality inference for composition of two classes. (Contributed by set.mm contributors, 16-Nov-2000.)
A = B       (C A) = (C B)

Theoremcoeq1d 4878 Equality deduction for composition of two classes. (Contributed by set.mm contributors, 16-Nov-2000.)
(φA = B)       (φ → (A C) = (B C))

Theoremcoeq2d 4879 Equality deduction for composition of two classes. (Contributed by set.mm contributors, 16-Nov-2000.)
(φA = B)       (φ → (C A) = (C B))

Theoremcoeq12i 4880 Equality inference for composition of two classes. (Contributed by FL, 7-Jun-2012.)
A = B    &   C = D       (A C) = (B D)

Theoremcoeq12d 4881 Equality deduction for composition of two classes. (Contributed by FL, 7-Jun-2012.)
(φA = B)    &   (φC = D)       (φ → (A C) = (B D))

Theoremnfco 4882 Bound-variable hypothesis builder for function value. (Contributed by NM, 1-Sep-1999.)
xA    &   xB       x(A B)

Theorembrco 4883* Binary relation on a composition. (Contributed by set.mm contributors, 21-Sep-2004.)

Theoremopelco 4884* Ordered pair membership in a composition. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm contributors, 27-Dec-1996.) (Revised by set.mm contributors, 27-Aug-2011.)
(A, B (C D) ↔ x(ADx xCB))

Theoremcnvss 4885 Subset theorem for converse. (Contributed by set.mm contributors, 22-Mar-1998.)
(A BA B)

Theoremcnveq 4886 Equality theorem for converse. (Contributed by set.mm contributors, 13-Aug-1995.)
(A = BA = B)

Theoremcnveqi 4887 Equality inference for converse. (Contributed by set.mm contributors, 23-Dec-2008.)
A = B       A = B

Theoremcnveqd 4888 Equality deduction for converse. (Contributed by set.mm contributors, 6-Dec-2013.)
(φA = B)       (φA = B)

Theoremelcnv 4889* Membership in a converse. Equation 5 of [Suppes] p. 62. (Contributed by set.mm contributors, 24-Mar-1998.)
(A Rxy(A = x, y yRx))

Theoremelcnv2 4890* Membership in a converse. Equation 5 of [Suppes] p. 62. (Contributed by set.mm contributors, 11-Aug-2004.)
(A Rxy(A = x, y y, x R))

Theoremnfcnv 4891 Bound-variable hypothesis builder for converse. (Contributed by NM, 31-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
xA       xA

Theorembrcnv 4892 The converse of a binary relation swaps arguments. Theorem 11 of [Suppes] p. 61. (Contributed by set.mm contributors, 13-Aug-1995.)
(ARBBRA)

Theoremopelcnv 4893 Ordered-pair membership in converse. (Contributed by set.mm contributors, 13-Aug-1995.)
(A, B RB, A R)

Theoremcnvco 4894 Distributive law of converse over class composition. Theorem 26 of [Suppes] p. 64. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by set.mm contributors, 19-Mar-1998.) (Revised by set.mm contributors, 27-Aug-2011.)
(A B) = (B A)

Theoremcnvuni 4895* The converse of a class union is the (indexed) union of the converses of its members. (Contributed by set.mm contributors, 11-Aug-2004.)
A = x A x

Theoremelrn 4896* Membership in a range. (Contributed by set.mm contributors, 2-Apr-2004.)
(A ran Bx xBA)

Theoremelrn2 4897* Membership in a range. (Contributed by set.mm contributors, 10-Jul-1994.)
(A ran Bxx, A B)

Theoremeldm 4898* Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by set.mm contributors, 2-Apr-2004.)
(A dom By ABy)

Theoremeldm2 4899* Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by set.mm contributors, 1-Aug-1994.)
(A dom ByA, y B)

Theoremdfdm2 4900* Alternate definition of domain. (Contributed by set.mm contributors, 5-Feb-2015.)
dom A = {x y xAy}

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-6338
 Copyright terms: Public domain < Previous  Next >