HomeHome New Foundations Explorer
Theorem List (p. 49 of 64)
< Previous  Next >
Bad symbols? Try the
GIF version.

Mirrors  >  Metamath Home Page  >  NFE Home Page  >  Theorem List Contents       This page: Page List

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.)
(A(C D)Bx(ADx xCB))
 
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}
    < 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-6338
  Copyright terms: Public domain < Previous  Next >