HomeHome New Foundations Explorer
Theorem List (p. 56 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 - 5501-5600   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremopbr1st 5501 Binary relationship of an ordered pair over 1st. (Contributed by SF, 6-Feb-2015.)
A V    &   B V       (A, B1st CA = C)
 
Theoremopbr2nd 5502 Binary relationship of an ordered pair over 2nd. (Contributed by SF, 6-Feb-2015.)
A V    &   B V       (A, B2nd CB = C)
 
Theoremdfid4 5503 Alternate definition of the identity relationship. (Contributed by SF, 11-Feb-2015.)
I = ( S S )
 
Theoremidex 5504 The identity relationship is a set. (Contributed by SF, 11-Feb-2015.)
I V
 
Theorem1stfo 5505 1st is a mapping from the universe onto the universe. (Contributed by SF, 12-Feb-2015.) (Revised by Scott Fenton, 17-Apr-2021.)
1st :V–onto→V
 
Theorem2ndfo 5506 2nd is a mapping from the universe onto the universe. (Contributed by SF, 12-Feb-2015.) (Revised by Scott Fenton, 17-Apr-2021.)
2nd :V–onto→V
 
Theoremdfdm4 5507 Alternate definition of domain. (Contributed by SF, 23-Feb-2015.)
dom A = (1stA)
 
Theoremdfrn5 5508 Alternate definition of range. (Contributed by SF, 23-Feb-2015.)
ran A = (2ndA)
 
Theorembrswap 5509* Binary relationship of Swap . (Contributed by SF, 23-Feb-2015.)
(A Swap Bxy(A = x, y B = y, x))
 
Theoremcnvswap 5510 The converse of Swap is Swap . (Contributed by SF, 23-Feb-2015.)
Swap = Swap
 
Theoremswapf1o 5511 Swap is a bijection over the universe. (Contributed by SF, 23-Feb-2015.) (Revised by Scott Fenton, 17-Apr-2021.)
Swap :V–1-1-onto→V
 
Theoremswapres 5512 Bijection law for restrictions of Swap . (Contributed by SF, 23-Feb-2015.) (Modified by Scott Fenton, 17-Apr-2021.)
( Swap A):A1-1-ontoA
 
Theoremxpnedisj 5513 Cross products with non-equal singletons are disjoint. (Contributed by SF, 23-Feb-2015.)
C V    &   CD       ((A × {C}) ∩ (B × {D})) =
 
Theoremopfv1st 5514 The value of the 1st function on an ordered pair. (Contributed by SF, 23-Feb-2015.)
A V    &   B V       (1stA, B) = A
 
Theoremopfv2nd 5515 The value of the 2nd function on an ordered pair. (Contributed by SF, 23-Feb-2015.)
A V    &   B V       (2ndA, B) = B
 
Theorem1st2nd2 5516 Reconstruction of a member of a cross product in terms of its ordered pair components. (Contributed by SF, 20-Oct-2013.)
(A (B × C) → A = (1stA), (2ndA))
 
Theoremfununiq 5517 Implicational form of part of the definition of a function. (Contributed by SF, 24-Feb-2015.)
((Fun F AFB AFC) → B = C)
 
Theoremcnvsi 5518 Calculate the converse of a singleton image. (Contributed by SF, 26-Feb-2015.)
SI R = SI R
 
Theoremdmsi 5519 Calculate the domain of a singleton image. Theorem X.4.29.I of [Rosser] p. 301. (Contributed by SF, 26-Feb-2015.)
dom SI R = 1dom R
 
Theoremfunsi 5520 The singleton image of a function is a function. (Contributed by SF, 26-Feb-2015.)
(Fun F → Fun SI F)
 
Theoremrnsi 5521 Calculate the range of a singleton image. Theorem X.4.29.II of [Rosser] p. 302. (Contributed by SF, 26-Feb-2015.)
ran SI R = 1ran R
 
Theoremop1std 5522 Extract the first member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.)
A V    &   B V       (C = A, B → (1stC) = A)
 
Theoremop2ndd 5523 Extract the second member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.)
A V    &   B V       (C = A, B → (2ndC) = B)
 
Theoremdmep 5524 The domain of the epsilon relationship. (Contributed by Scott Fenton, 20-Apr-2021.)
dom E = V
 
2.3.8  Operations
 
Syntaxco 5525 Extend class notation to include the value of an operation F for two arguments A and B. Note that the syntax is simply three class symbols in a row surrounded by parentheses. Since operation values are the only possible class expressions consisting of three class expressions in a row surrounded by parentheses, the syntax is unambiguous.
class (AFB)
 
Definitiondf-ov 5526 Define the value of an operation. Definition of operation value in [Enderton] p. 79. Note that the syntax is simply three class expressions in a row bracketed by parentheses. There are no restrictions of any kind on what those class expressions may be, although only certain kinds of class expressions - a binary operation F and its arguments A and B- will be useful for proving meaningful theorems. This definition is well-defined, although not very meaningful, when classes A and/or B are proper classes (i.e. are not sets). On the other hand, we often find uses for this definition when F is a proper class. F is normally equal to a class of nested ordered pairs of the form defined by df-oprab 5528. (Contributed by SF, 5-Jan-2015.)
(AFB) = (FA, B)
 
Syntaxcoprab 5527 Extend class notation to include class abstraction (class builder) of nested ordered pairs.
class {x, y, z φ}
 
Definitiondf-oprab 5528* Define the class abstraction (class builder) of a collection of nested ordered pairs (for use in defining operations). This is a special case of Definition 4.16 of [TakeutiZaring] p. 14. Normally x, y, and z are distinct, although the definition doesn't strictly require it. See df-ov 5526 for the value of an operation. The brace notation is called "class abstraction" by Quine; it is also called a "class builder" in the literature. The value of the most common operation class builder is given by ov2 in set.mm. (Contributed by SF, 5-Jan-2015.)
{x, y, z φ} = {w xyz(w = x, y, z φ)}
 
Theoremoveq 5529 Equality theorem for operation value. (Contributed by set.mm contributors, 28-Feb-1995.)
(F = G → (AFB) = (AGB))
 
Theoremoveq1 5530 Equality theorem for operation value. (Contributed by set.mm contributors, 28-Feb-1995.)
(A = B → (AFC) = (BFC))
 
Theoremoveq2 5531 Equality theorem for operation value. (Contributed by set.mm contributors, 28-Feb-1995.)
(A = B → (CFA) = (CFB))
 
Theoremoveq12 5532 Equality theorem for operation value. (Contributed by set.mm contributors, 16-Jul-1995.)
((A = B C = D) → (AFC) = (BFD))
 
Theoremoveq1i 5533 Equality inference for operation value. (Contributed by set.mm contributors, 28-Feb-1995.)
A = B       (AFC) = (BFC)
 
Theoremoveq2i 5534 Equality inference for operation value. (Contributed by set.mm contributors, 28-Feb-1995.)
A = B       (CFA) = (CFB)
 
Theoremoveq12i 5535 Equality inference for operation value. (The proof was shortened by Andrew Salmon, 22-Oct-2011.) (Contributed by set.mm contributors, 28-Feb-1995.) (Revised by set.mm contributors, 22-Oct-2011.)
A = B    &   C = D       (AFC) = (BFD)
 
Theoremoveqi 5536 Equality inference for operation value. (Contributed by set.mm contributors, 24-Nov-2007.)
A = B       (CAD) = (CBD)
 
Theoremoveq1d 5537 Equality deduction for operation value. (Contributed by set.mm contributors, 13-Mar-1995.)
(φA = B)       (φ → (AFC) = (BFC))
 
Theoremoveq2d 5538 Equality deduction for operation value. (Contributed by set.mm contributors, 13-Mar-1995.)
(φA = B)       (φ → (CFA) = (CFB))
 
Theoremoveqd 5539 Equality deduction for operation value. (Contributed by set.mm contributors, 9-Sep-2006.)
(φA = B)       (φ → (CAD) = (CBD))
 
Theoremoveq12d 5540 Equality deduction for operation value. (The proof was shortened by Andrew Salmon, 22-Oct-2011.) (Contributed by set.mm contributors, 13-Mar-1995.) (Revised by set.mm contributors, 22-Oct-2011.)
(φA = B)    &   (φC = D)       (φ → (AFC) = (BFD))
 
Theoremoveqan12d 5541 Equality deduction for operation value. (Contributed by set.mm contributors, 10-Aug-1995.)
(φA = B)    &   (ψC = D)       ((φ ψ) → (AFC) = (BFD))
 
Theoremoveqan12rd 5542 Equality deduction for operation value. (Contributed by set.mm contributors, 10-Aug-1995.)
(φA = B)    &   (ψC = D)       ((ψ φ) → (AFC) = (BFD))
 
Theoremoveq123d 5543 Equality deduction for operation value. (Contributed by FL, 22-Dec-2008.)
(φF = G)    &   (φA = B)    &   (φC = D)       (φ → (AFC) = (BGD))
 
Theoremnfovd 5544 Deduction version of bound-variable hypothesis builder nfov 5545. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
(φxA)    &   (φxF)    &   (φxB)       (φx(AFB))
 
Theoremnfov 5545 Bound-variable hypothesis builder for operation value. (Contributed by NM, 4-May-2004.)
xA    &   xF    &   xB       x(AFB)
 
Theoremnfoprab1 5546 The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 25-Apr-1995.) (Revised by David Abernethy, 19-Jun-2012.)
x{x, y, z φ}
 
Theoremnfoprab2 5547 The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 25-Apr-1995.) (Revised by David Abernethy, 30-Jul-2012.)
y{x, y, z φ}
 
Theoremnfoprab3 5548 The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 22-Aug-2013.)
z{x, y, z φ}
 
Theoremnfoprab 5549* Bound-variable hypothesis builder for an operation class abstraction. (Contributed by NM, 22-Aug-2013.)
wφ       w{x, y, z φ}
 
Theoremoprabid 5550 The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 20-Mar-2013.)
(x, y, z {x, y, z φ} ↔ φ)
 
Theoremovex 5551 The result of an operation is a set. (Contributed by set.mm contributors, 13-Mar-1995.)
(AFB) V
 
Theoremcsbovg 5552 Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.) (Proof shortened by Mario Carneiro, 5-Dec-2016.)
(A D[A / x](BFC) = ([A / x]B[A / x]F[A / x]C))
 
Theoremcsbov12g 5553* Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)
(A D[A / x](BFC) = ([A / x]BF[A / x]C))
 
Theoremcsbov1g 5554* Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)
(A D[A / x](BFC) = ([A / x]BFC))
 
Theoremcsbov2g 5555* Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)
(A D[A / x](BFC) = (BF[A / x]C))
 
Theoremrspceov 5556* A frequently used special case of rspc2ev 2963 for operation values. (Contributed by set.mm contributors, 21-Mar-2007.)
((C A D B S = (CFD)) → x A y B S = (xFy))
 
Theoremfnopovb 5557 Equivalence of operation value and ordered triple membership, analogous to fnopfvb 5359. (Contributed by set.mm contributors, 17-Dec-2008.)
((F Fn (A × B) C A D B) → ((CFD) = RC, D, R F))
 
Theoremdfoprab2 5558* Class abstraction for operations in terms of class abstraction of ordered pairs. (Contributed by set.mm contributors, 12-Mar-1995.)
{x, y, z φ} = {w, z xy(w = x, y φ)}
 
Theoremhboprab1 5559* The abstraction variables in an operation class abstraction are not free. (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Contributed by set.mm contributors, 25-Apr-1995.) (Revised by set.mm contributors, 24-Jul-2012.)
(w {x, y, z φ} → x w {x, y, z φ})
 
Theoremhboprab2 5560* The abstraction variables in an operation class abstraction are not free. (Unnecessary distinct variable restrictions were removed by David Abernethy, 30-Jul-2012.) (Contributed by set.mm contributors, 25-Apr-1995.) (Revised by set.mm contributors, 31-Jul-2012.)
(w {x, y, z φ} → y w {x, y, z φ})
 
Theoremhboprab3 5561* The abstraction variables in an operation class abstraction are not free. (Contributed by set.mm contributors, 22-Aug-2013.)
(w {x, y, z φ} → z w {x, y, z φ})
 
Theoremhboprab 5562* Bound-variable hypothesis builder for an operation class abstraction. (Contributed by set.mm contributors, 22-Aug-2013.)
(φwφ)       (u {x, y, z φ} → w u {x, y, z φ})
 
Theoremoprabbid 5563* Equivalent wff's yield equal operation class abstractions (deduction rule). (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro, 24-Jun-2014.)
xφ    &   yφ    &   zφ    &   (φ → (ψχ))       (φ → {x, y, z ψ} = {x, y, z χ})
 
Theoremoprabbidv 5564* Equivalent wff's yield equal operation class abstractions (deduction rule). (Contributed by NM, 21-Feb-2004.)
(φ → (ψχ))       (φ → {x, y, z ψ} = {x, y, z χ})
 
Theoremoprabbii 5565* Equivalent wff's yield equal operation class abstractions. (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Contributed by set.mm contributors, 28-May-1995.) (Revised by set.mm contributors, 24-Jul-2012.)
(φψ)       {x, y, z φ} = {x, y, z ψ}
 
Theoremoprab4 5566* Two ways to state the domain of an operation. (Contributed by FL, 24-Jan-2010.)
{x, y, z (x, y (A × B) φ)} = {x, y, z ((x A y B) φ)}
 
Theoremcbvoprab1 5567* Rule used to change first bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 20-Dec-2008.) (Revised by Mario Carneiro, 5-Dec-2016.)
wφ    &   xψ    &   (x = w → (φψ))       {x, y, z φ} = {w, y, z ψ}
 
Theoremcbvoprab2 5568* Change the second bound variable in an operation abstraction. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 11-Dec-2016.)
wφ    &   yψ    &   (y = w → (φψ))       {x, y, z φ} = {x, w, z ψ}
 
Theoremcbvoprab12 5569* Rule used to change first two bound variables in an operation abstraction, using implicit substitution. (Contributed by NM, 21-Feb-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
wφ    &   vφ    &   xψ    &   yψ    &   ((x = w y = v) → (φψ))       {x, y, z φ} = {w, v, z ψ}
 
Theoremcbvoprab12v 5570* Rule used to change first two bound variables in an operation abstraction, using implicit substitution. (Contributed by set.mm contributors, 8-Oct-2004.)
((x = w y = v) → (φψ))       {x, y, z φ} = {w, v, z ψ}
 
Theoremcbvoprab3 5571* Rule used to change the third bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 22-Aug-2013.)
wφ    &   zψ    &   (z = w → (φψ))       {x, y, z φ} = {x, y, w ψ}
 
Theoremcbvoprab3v 5572* Rule used to change the third bound variable in an operation abstraction, using implicit substitution. (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Contributed by set.mm contributors, 8-Oct-2004.) (Revised by set.mm contributors, 24-Jul-2012.)
(z = w → (φψ))       {x, y, z φ} = {x, y, w ψ}
 
Theoremelimdelov 5573 Eliminate a hypothesis which is a predicate expressing membership in the result of an operator (deduction version). (Contributed by Paul Chapman, 25-Mar-2008.)
(φC (AFB))    &   Z (XFY)        if(φ, C, Z) ( if(φ, A, X)F if(φ, B, Y))
 
Theoremdmoprab 5574* The domain of an operation class abstraction. (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Contributed by set.mm contributors, 17-Mar-1995.) (Revised by set.mm contributors, 24-Jul-2012.)
dom {x, y, z φ} = {x, y zφ}
 
Theoremdmoprabss 5575* The domain of an operation class abstraction. (Contributed by set.mm contributors, 24-Aug-1995.)
dom {x, y, z ((x A y B) φ)} (A × B)
 
Theoremrnoprab 5576* The range of an operation class abstraction. (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Apr-2013.) (Contributed by set.mm contributors, 30-Aug-2004.) (Revised by set.mm contributors, 19-Apr-2013.)
ran {x, y, z φ} = {z xyφ}
 
Theoremrnoprab2 5577* The range of a restricted operation class abstraction. (Contributed by Scott Fenton, 21-Mar-2012.)
ran {x, y, z ((x A y B) φ)} = {z x A y B φ}
 
Theoremeloprabga 5578* The law of concretion for operation class abstraction. Compare elopab 4696. (Contributed by set.mm contributors, 17-Dec-2013.) (Revised by David Abernethy, 18-Jun-2012.) Removed unnecessary distinct variable requirements. (Revised by Mario Carneiro, 19-Dec-2013.)
((x = A y = B z = C) → (φψ))       ((A V B W C X) → (A, B, C {x, y, z φ} ↔ ψ))
 
Theoremeloprabg 5579* The law of concretion for operation class abstraction. Compare elopab 4696. (Contributed by set.mm contributors, 14-Sep-1999.) (Revised by David Abernethy, 19-Jun-2012.) Removed unnecessary distinct variable requirements. (Revised by set.mm contributors, 19-Dec-2013.)
(x = A → (φψ))    &   (y = B → (ψχ))    &   (z = C → (χθ))       ((A V B W C X) → (A, B, C {x, y, z φ} ↔ θ))
 
Theoremssoprab2i 5580* Inference of operation class abstraction subclass from implication. (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Contributed by set.mm contributors, 11-Nov-1995.) (Revised by set.mm contributors, 24-Jul-2012.)
(φψ)       {x, y, z φ} {x, y, z ψ}
 
Theoremresoprab 5581* Restriction of an operation class abstraction. (Contributed by set.mm contributors, 10-Feb-2007.)
({x, y, z φ} (A × B)) = {x, y, z ((x A y B) φ)}
 
Theoremresoprab2 5582* Restriction of an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.)
((C A D B) → ({x, y, z ((x A y B) φ)} (C × D)) = {x, y, z ((x C y D) φ)})
 
Theoremfunoprabg 5583* "At most one" is a sufficient condition for an operation class abstraction to be a function. (Contributed by set.mm contributors, 28-Aug-2007.)
(xy∃*zφ → Fun {x, y, z φ})
 
Theoremfunoprab 5584* "At most one" is a sufficient condition for an operation class abstraction to be a function. (Contributed by set.mm contributors, 17-Mar-1995.)
∃*zφ       Fun {x, y, z φ}
 
Theoremfnoprabg 5585* Functionality and domain of an operation class abstraction. (Contributed by set.mm contributors, 28-Aug-2007.)
(xy(φ∃!zψ) → {x, y, z (φ ψ)} Fn {x, y φ})
 
Theoremfnoprab 5586* Functionality and domain of an operation class abstraction. (Contributed by set.mm contributors, 15-May-1995.)
(φ∃!zψ)       {x, y, z (φ ψ)} Fn {x, y φ}
 
Theoremffnov 5587* An operation maps to a class to which all values belong. (Contributed by set.mm contributors, 7-Feb-2004.)
(F:(A × B)–→C ↔ (F Fn (A × B) x A y B (xFy) C))
 
Theoremfovcl 5588 Closure law for an operation. (Contributed by set.mm contributors, 19-Apr-2007.)
F:(R × S)–→C       ((A R B S) → (AFB) C)
 
Theoremeqfnov 5589* Equality of two operations is determined by their values. (Contributed by set.mm contributors, 1-Sep-2005.)
((F Fn (A × B) G Fn (C × D)) → (F = G ↔ ((A × B) = (C × D) x A y B (xFy) = (xGy))))
 
Theoremeqfnov2 5590* Two operators with the same domain are equal iff their values at each point in the domain are equal. (Contributed by Jeff Madsen, 7-Jun-2010.)
((F Fn (A × B) G Fn (A × B)) → (F = Gx A y B (xFy) = (xGy)))
 
Theoremfnov 5591* Representation of an operation class abstraction in terms of its values. (Contributed by set.mm contributors, 7-Feb-2004.)
(F Fn (A × B) ↔ F = {x, y, z ((x A y B) z = (xFy))})
 
Theoremfov 5592* Representation of an operation class abstraction in terms of its values. (Contributed by set.mm contributors, 7-Feb-2004.)
(F:(A × B)–→C ↔ (F = {x, y, z ((x A y B) z = (xFy))} x A y B (xFy) C))
 
Theoremovidig 5593* The value of an operation class abstraction. Compare ovidi 5594. The condition (x R y S) is been removed. (Contributed by Mario Carneiro, 29-Dec-2014.)
∃*zφ    &   F = {x, y, z φ}       (φ → (xFy) = z)
 
Theoremovidi 5594* The value of an operation class abstraction (weak version). (Contributed by Mario Carneiro, 29-Dec-2014.)
((x R y S) → ∃*zφ)    &   F = {x, y, z ((x R y S) φ)}       ((x R y S) → (φ → (xFy) = z))
 
Theoremov 5595* The value of an operation class abstraction. (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Contributed by set.mm contributors, 16-May-1995.) (Revised by set.mm contributors, 24-Jul-2012.)
C V    &   (x = A → (φψ))    &   (y = B → (ψχ))    &   (z = C → (χθ))    &   ((x R y S) → ∃!zφ)    &   F = {x, y, z ((x R y S) φ)}       ((A R B S) → ((AFB) = Cθ))
 
Theoremovigg 5596* The value of an operation class abstraction. Compare ovig 5597. The condition (x R y S) is been removed. (Contributed by FL, 24-Mar-2007.)
((x = A y = B z = C) → (φψ))    &   ∃*zφ    &   F = {x, y, z φ}       ((A V B W C X) → (ψ → (AFB) = C))
 
Theoremovig 5597* The value of an operation class abstraction (weak version). (Contributed by set.mm contributors, 14-Sep-1999.) (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Revised by Mario Carneiro, 19-Dec-2013.)
((x = A y = B z = C) → (φψ))    &   ((x R y S) → ∃*zφ)    &   F = {x, y, z ((x R y S) φ)}       ((A R B S C D) → (ψ → (AFB) = C))
 
Theoremov2ag 5598* The value of an operation class abstraction. Special case. (Contributed by Mario Carneiro, 19-Dec-2013.)
((x = A y = B) → R = S)    &   F = {x, y, z ((x C y D) z = R)}       ((A C B D S H) → (AFB) = S)
 
Theoremov3 5599* The value of an operation class abstraction. Special case. (Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro, 29-Dec-2014.)
S V    &   (((w = A v = B) (u = C f = D)) → R = S)    &   F = {x, y, z ((x (H × H) y (H × H)) wvuf((x = w, v y = u, f) z = R))}       (((A H B H) (C H D H)) → (A, BFC, D) = S)
 
Theoremov6g 5600* The value of an operation class abstraction. Special case. (Contributed by set.mm contributors, 13-Nov-2006.)
(x, y = A, BR = S)    &   F = {x, y, z (x, y C z = R)}       (((A G B H A, B C) S J) → (AFB) = S)
    < 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-6336
  Copyright terms: Public domain < Previous  Next >