HomeHome New Foundations Explorer
Theorem List (p. 49 of 64)
< Previous  Next >
Bad symbols? Use Firefox
(or GIF version for IE).

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
 
Theoremxpeq1d 4801 Equality deduction for cross product. (Contributed by Jeff Madsen, 17-Jun-2010.)
(φA = B)       (φ → (A × C) = (B × C))
 
Theoremxpeq2d 4802 Equality deduction for cross product. (Contributed by Jeff Madsen, 17-Jun-2010.)
(φA = B)       (φ → (C × A) = (C × B))
 
Theoremxpeq12d 4803 Equality deduction for cross product. (Contributed by NM, 8-Dec-2013.)
(φA = B)    &   (φC = D)       (φ → (A × C) = (B × D))
 
Theoremnfxp 4804 Bound-variable hypothesis builder for cross product. (Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro, 15-Oct-2016.)
F/_xA    &   F/_xB       F/_x(A × B)
 
Theoremopelxp 4805 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 4806 Binary relation on a cross product. (Contributed by NM, 22-Apr-2004.)
(A(C × D)B ↔ (A C B D))
 
Theoremcsbxpg 4807 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 4808* 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 4809* Representation of a constant function using ordered pairs. (Contributed by NM, 12-Oct-1999.)
(A × {B}) = {x, y (x A y = B)}
 
Theoremvtoclr 4810* Variable to class conversion of transitive relation. (Contributed by NM, 9-Jun-1998.)
((xRy yRz) → xRz)       ((ARB BRC) → ARC)
 
Theoremralxp 4811* Universal quantification restricted to a cross 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 4812* Existential quantification restricted to a cross 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 4813* Version of ralxp 4811 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 4814* Version of rexxp 4812 with bound-variable hypotheses. (Contributed by NM, 19-Dec-2008.)
yφ    &   zφ    &   xψ    &   (x = y, z → (φψ))       (x (A × B)φy A z B ψ)
 
Theoremiunxpf 4815* Indexed union on a cross product is equals a double indexed union. The hypothesis specifies an implicit substitution. (Contributed by NM, 19-Dec-2008.)
F/_yC    &   F/_zC    &   F/_xD    &   (x = y, zC = D)       x (A × B)C = y A z B D
 
Theorembrel 4816 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 4817* Membership in a cross product. (Contributed by NM, 5-Mar-1995.)
(A (B × C) ↔ xy(x, y = A x, y (B × C)))
 
Theoremxpundi 4818 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 4819 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))
 
Theoremxpiundi 4820* Distributive law for cross product over indexed union. (Revised by Mario Carneiro, 27-Apr-2014.) (Contributed by set.mm contributors, 27-Apr-2014.)
(C × x A B) = x A (C × B)
 
Theoremxpiundir 4821* Distributive law for cross product over indexed union. (Revised by Mario Carneiro, 27-Apr-2014.) (Contributed by set.mm contributors, 27-Apr-2014.)
(x A B × C) = x A (B × C)
 
Theoremiunxpconst 4822* 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)
 
Theoremxpun 4823 The cross product of two unions. (Contributed by NM, 12-Aug-2004.)
((AB) × (CD)) = (((A × C) ∪ (A × D)) ∪ ((B × C) ∪ (B × D)))
 
Theoremelvv 4824* Membership in universal class of ordered pairs. (Contributed by NM, 4-Jul-1994.)
(A (V × V) ↔ xy A = x, y)
 
Theoremelvvv 4825* Membership in universal class of ordered triples. (Contributed by NM, 17-Dec-2008.)
(A ((V × V) × V) ↔ xyz A = x, y, z)
 
Theorembrinxp2 4826 Intersection of binary relation with cross product. (Contributed by NM, 3-Mar-2007.)
(A(R ∩ (C × D))B ↔ (A C B D ARB))
 
Theorembrinxp 4827 Intersection of binary relation with cross product. (Contributed by NM, 9-Mar-1997.)
((A C B D) → (ARBA(R ∩ (C × D))B))
 
Theoremopabssxp 4828* 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 4829* 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 4830* 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 4831* 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 4832* 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 4833 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) =
 
Theoremreleq 4834 Equality theorem for the relation predicate. (Contributed by NM, 1-Aug-1994.)
(A = B → (Rel A ↔ Rel B))
 
Theoremreleqi 4835 Equality inference for the relation predicate. (Contributed by NM, 8-Dec-2006.)
A = B       (Rel A ↔ Rel B)
 
Theoremreleqd 4836 Equality deduction for the relation predicate. (Contributed by NM, 8-Mar-2014.)
(φA = B)       (φ → (Rel A ↔ Rel B))
 
Theoremnfrel 4837 Bound-variable hypothesis builder for a relation. (Contributed by NM, 31-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
F/_xA       xRel A
 
Theoremrelss 4838 Subclass theorem for relation predicate. Theorem 2 of [Suppes] p. 58. (Contributed by NM, 15-Aug-1994.)
(A B → (Rel B → Rel A))
 
Theoremssrel 4839* 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.)
(Rel A → (A Bxy(x, y Ax, y B)))
 
Theoremeqrel 4840* Extensionality principle for relations. Theorem 3.2(ii) of [Monk1] p. 33. (Contributed by NM, 2-Aug-1994.)
((Rel A Rel B) → (A = Bxy(x, y Ax, y B)))
 
Theoremrelssi 4841* Inference from subclass principle for relations. (Contributed by NM, 31-Mar-1998.)
Rel A    &   (x, y Ax, y B)       A B
 
Theoremrelssdv 4842* Deduction from subclass principle for relations. (Contributed by set.mm contributors, 11-Sep-2004.)
(φ → Rel A)    &   (φ → (x, y Ax, y B))       (φA B)
 
Theoremeqrelriv 4843* Inference from extensionality principle for relations. (Contributed by FL, 15-Oct-2012.)
(x, y Ax, y B)       ((Rel A Rel B) → A = B)
 
Theoremeqrelriiv 4844* Inference from extensionality principle for relations. (Contributed by NM, 17-Mar-1995.)
Rel A    &   Rel B    &   (x, y Ax, y B)       A = B
 
Theoremeqbrriv 4845* Inference from extensionality principle for relations. (Contributed by NM, 12-Dec-2006.)
Rel A    &   Rel B    &   (xAyxBy)       A = B
 
Theoremeqrelrdv 4846* Deduce equality of relations from equivalence of membership. (Contributed by Rodolfo Medina, 10-Oct-2010.)
Rel A    &   Rel B    &   (φ → (x, y Ax, y B))       (φA = B)
 
Theoremeqrelrdv2 4847* A version of eqrelrdv 4846. (Contributed by Rodolfo Medina, 10-Oct-2010.)
(φ → (x, y Ax, y B))       (((Rel A Rel B) φ) → A = B)
 
Theoremssrelrel 4848* A subclass relationship determined by ordered triples. Use relrelss 5130 to express the antecedent in terms of the relation predicate. (The proof was shortened by Andrew Salmon, 27-Aug-2011.) (Contributed by NM, 17-Dec-2008.) (Revised by set.mm contributors, 27-Aug-2011.)
(A ((V × V) × V) → (A Bxyz(x, y, z Ax, y, z B)))
 
Theoremeqrelrel 4849* Extensionality principle for ordered triples (used by 2-place operations df-oprab 5567), analogous to eqrel 4840. Use relrelss 5130 to express the antecedent in terms of the relation predicate. (Contributed by NM, 17-Dec-2008.)
((AB) ((V × V) × V) → (A = Bxyz(x, y, z Ax, y, z B)))
 
Theoremelrel 4850* A member of a relation is an ordered pair. (Contributed by NM, 17-Sep-2006.)
((Rel R A R) → xy A = x, y)
 
Theoremrelsn 4851 A singleton is a relation iff it is an ordered pair. (Contributed by NM, 24-Sep-2013.)
A V       (Rel {A} ↔ A (V × V))
 
Theoremrelsnop 4852 A singleton of an ordered pair is a relation. (Contributed by NM, 17-May-1998.)
A V    &   B V       Rel {A, B}
 
Theoremxpss12 4853 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))
 
Theoremxpss 4854 A cross product is included in the ordered pair universe. Exercise 3 of [TakeutiZaring] p. 25. (Contributed by NM, 2-Aug-1994.)
(A × B) (V × V)
 
Theoremrelxp 4855 A cross product is a relation. Theorem 3.13(i) of [Monk1] p. 37. (Contributed by NM, 2-Aug-1994.)
Rel (A × B)
 
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)
 
Theoremrelun 4861 The union of two relations is a relation. Compare Exercise 5 of [TakeutiZaring] p. 25. (Contributed by NM, 12-Aug-1994.)
(Rel (AB) ↔ (Rel A Rel B))
 
Theoremrelin1 4862 The intersection with a relation is a relation. (Contributed by NM, 16-Aug-1994.)
(Rel A → Rel (AB))
 
Theoremrelin2 4863 The intersection with a relation is a relation. (Contributed by NM, 17-Jan-2006.)
(Rel B → Rel (AB))
 
Theoremreldif 4864 A difference cutting down a relation is a relation. (Contributed by NM, 31-Mar-1998.)
(Rel A → Rel (A B))
 
Theoremreliun 4865 An indexed union is a relation iff each member of its indexed family is a relation. (Contributed by set.mm contributors, 19-Dec-2008.)
(Rel x A Bx A Rel B)
 
Theoremreliin 4866 An indexed intersection is a relation if if at least one of the member of the indexed family is a relation. (Contributed by set.mm contributors, 8-Mar-2014.)
(x A Rel B → Rel x A B)
 
Theoremreluni 4867* 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 Ax A Rel x)
 
Theoremrelint 4868* The intersection of a class is a relation if at least one member is a relation. (Contributed by NM, 8-Mar-2014.)
(x A Rel x → Rel A)
 
Theoremrel0 4869 The empty set is a relation. (Contributed by NM, 26-Apr-1998.)
Rel
 
Theoremrelopabi 4870 A class of ordered pairs is a relation. (Contributed by Mario Carneiro, 21-Dec-2013.)
A = {x, y φ}       Rel A
 
Theoremrelopab 4871 A class of ordered pairs is a relation. (Unnecessary distinct variable restrictions were removed by Alan Sare, 9-Jul-2013.) (The proof was shortened by Mario Carneiro, 21-Dec-2013.) (Contributed by NM, 8-Mar-1995.) (Revised by set.mm contributors, 9-Jul-2013.)
Rel {x, y φ}
 
Theoremreli 4872 The identity relation is a relation. Part of Exercise 4.12(p) of [Mendelson] p. 235. (Contributed by NM, 26-Apr-1998.) (Revised by set.mm contributors, 21-Dec-2013.)
Rel I
 
Theoremrele 4873 The membership relation is a relation. (Contributed by NM, 26-Apr-1998.) (Revised by set.mm contributors, 21-Dec-2013.)
Rel E
 
Theoremopabid2 4874* A relation expressed as an ordered pair abstraction. (Contributed by set.mm contributors, 11-Dec-2006.)
(Rel A → {x, y x, y A} = A)
 
Theoreminopab 4875* Intersection of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002.)
({x, y φ} ∩ {x, y ψ}) = {x, y (φ ψ)}
 
Theoreminxp 4876 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 4877 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 4878 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))
 
Theoremopabbi2dv 4879* Deduce equality of a relation and an ordered-pair class builder. Compare abbi2dv 2468. (Contributed by NM, 24-Feb-2014.)
Rel A    &   (φ → (x, y Aψ))       (φA = {x, y ψ})
 
Theoremideqg 4880 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 4881 For sets, the identity relation is the same as equality. (Contributed by SF, 8-Jan-2015.)
(A V → (A I BA = B))
 
Theoremideq 4882 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 4883 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 4884 Subclass theorem for composition. (Contributed by FL, 30-Dec-2010.)
(A B → (A C) (B C))
 
Theoremcoss2 4885 Subclass theorem for composition. (Contributed by set.mm contributors, 5-Apr-2013.)
(A B → (C A) (C B))
 
Theoremcoeq1 4886 Equality theorem for composition of two classes. (Contributed by set.mm contributors, 3-Jan-1997.)
(A = B → (A C) = (B C))
 
Theoremcoeq2 4887 Equality theorem for composition of two classes. (Contributed by set.mm contributors, 3-Jan-1997.)
(A = B → (C A) = (C B))
 
Theoremcoeq1i 4888 Equality inference for composition of two classes. (Contributed by set.mm contributors, 16-Nov-2000.)
A = B       (A C) = (B C)
 
Theoremcoeq2i 4889 Equality inference for composition of two classes. (Contributed by set.mm contributors, 16-Nov-2000.)
A = B       (C A) = (C B)
 
Theoremcoeq1d 4890 Equality deduction for composition of two classes. (Contributed by set.mm contributors, 16-Nov-2000.)
(φA = B)       (φ → (A C) = (B C))
 
Theoremcoeq2d 4891 Equality deduction for composition of two classes. (Contributed by set.mm contributors, 16-Nov-2000.)
(φA = B)       (φ → (C A) = (C B))
 
Theoremcoeq12i 4892 Equality inference for composition of two classes. (Contributed by FL, 7-Jun-2012.)
A = B    &   C = D       (A C) = (B D)
 
Theoremcoeq12d 4893 Equality deduction for composition of two classes. (Contributed by FL, 7-Jun-2012.)
(φA = B)    &   (φC = D)       (φ → (A C) = (B D))
 
Theoremnfco 4894 Bound-variable hypothesis builder for function value. (Contributed by NM, 1-Sep-1999.)
F/_xA    &   F/_xB       F/_x(A B)
 
Theorembrco 4895* Binary relation on a composition. (Contributed by set.mm contributors, 21-Sep-2004.)
(A(C D)Bx(ADx xCB))
 
Theoremopelco 4896* 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 4897 Subset theorem for converse. (Contributed by set.mm contributors, 22-Mar-1998.)
(A BA B)
 
Theoremcnveq 4898 Equality theorem for converse. (Contributed by set.mm contributors, 13-Aug-1995.)
(A = BA = B)
 
Theoremcnveqi 4899 Equality inference for converse. (Contributed by set.mm contributors, 23-Dec-2008.)
A = B       A = B
 
Theoremcnveqd 4900 Equality deduction for converse. (Contributed by set.mm contributors, 6-Dec-2013.)
(φA = B)       (φA = B)
    < 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-6308
  Copyright terms: Public domain < Previous  Next >