Theorem List for New Foundations Explorer - 5301-5400 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | f1orescnv 5301 |
The converse of a one-to-one-onto restricted function. (Contributed by
Paul Chapman, 21-Apr-2008.)
|
⊢ ((Fun ◡F ∧ (F ↾ R):R–1-1-onto→P) →
(◡F ↾ P):P–1-1-onto→R) |
|
Theorem | f1imacnv 5302 |
Preimage of an image. (Contributed by set.mm contributors,
30-Sep-2004.)
|
⊢ ((F:A–1-1→B
∧ C ⊆ A) →
(◡F “ (F
“ C)) = C) |
|
Theorem | foimacnv 5303 |
A reverse version of f1imacnv 5302. (Contributed by Jeffrey Hankins,
16-Jul-2009.)
|
⊢ ((F:A–onto→B
∧ C ⊆ B) →
(F “ (◡F
“ C)) = C) |
|
Theorem | f1oun 5304 |
The union of two one-to-one onto functions with disjoint domains and
ranges. (Contributed by set.mm contributors, 26-Mar-1998.)
|
⊢ (((F:A–1-1-onto→B ∧ G:C–1-1-onto→D) ∧ ((A ∩
C) = ∅
∧ (B
∩ D) = ∅)) → (F
∪ G):(A ∪ C)–1-1-onto→(B ∪
D)) |
|
Theorem | fun11iun 5305* |
The union of a chain (with respect to inclusion) of one-to-one functions
is a one-to-one function. (Contributed by Mario Carneiro, 20-May-2013.)
(Revised by Mario Carneiro, 24-Jun-2015.)
|
⊢ (x =
y → B = C)
& ⊢ B ∈ V ⇒ ⊢ (∀x ∈ A (B:D–1-1→S ∧ ∀y ∈ A (B ⊆ C ∨ C ⊆ B)) →
∪x ∈ A B:∪x ∈ A D–1-1→S) |
|
Theorem | resdif 5306 |
The restriction of a one-to-one onto function to a difference maps onto
the difference of the images. (Contributed by Paul Chapman,
11-Apr-2009.)
|
⊢ ((Fun ◡F ∧ (F ↾ A):A–onto→C ∧ (F ↾ B):B–onto→D) →
(F ↾
(A ∖
B)):(A
∖ B)–1-1-onto→(C ∖ D)) |
|
Theorem | resin 5307 |
The restriction of a one-to-one onto function to an intersection maps onto
the intersection of the images. (Contributed by Paul Chapman,
11-Apr-2009.)
|
⊢ ((Fun ◡F ∧ (F ↾ A):A–onto→C ∧ (F ↾ B):B–onto→D) →
(F ↾
(A ∩ B)):(A ∩
B)–1-1-onto→(C ∩
D)) |
|
Theorem | f1oco 5308 |
Composition of one-to-one onto functions. (Contributed by set.mm
contributors, 19-Mar-1998.)
|
⊢ ((F:B–1-1-onto→C ∧ G:A–1-1-onto→B) →
(F ∘
G):A–1-1-onto→C) |
|
Theorem | f1ococnv2 5309 |
The composition of a one-to-one onto function and its converse equals the
identity relation restricted to the function's range. (Contributed by
set.mm contributors, 13-Dec-2003.)
|
⊢ (F:A–1-1-onto→B →
(F ∘
◡F) = ( I ↾
B)) |
|
Theorem | f1ococnv1 5310 |
The composition of a one-to-one onto function's converse and itself equals
the identity relation restricted to the function's domain. (Contributed
by set.mm contributors, 13-Dec-2003.)
|
⊢ (F:A–1-1-onto→B →
(◡F ∘ F) = ( I ↾
A)) |
|
Theorem | f1cnv 5311 |
The converse of an injective function is bijective. (Contributed by FL,
11-Nov-2011.)
|
⊢ (F:A–1-1→B →
◡F:ran F–1-1-onto→A) |
|
Theorem | f1cocnv1 5312 |
Composition of an injective function with its converse. (Contributed by
FL, 11-Nov-2011.)
|
⊢ (F:A–1-1→B →
(◡F ∘ F) = ( I ↾
A)) |
|
Theorem | f1cocnv2 5313 |
Composition of an injective function with its converse. (Contributed by
FL, 11-Nov-2011.)
|
⊢ (F:A–1-1→B →
(F ∘
◡F) = ( I ↾ ran
F)) |
|
Theorem | ffoss 5314* |
Relationship between a mapping and an onto mapping. Figure 38 of
[Enderton] p. 145. (Contributed by
set.mm contributors,
10-May-1998.)
|
⊢ F ∈ V ⇒ ⊢ (F:A–→B
↔ ∃x(F:A–onto→x ∧ x ⊆ B)) |
|
Theorem | f11o 5315* |
Relationship between one-to-one and one-to-one onto function.
(Contributed by set.mm contributors, 4-Apr-1998.)
|
⊢ F ∈ V ⇒ ⊢ (F:A–1-1→B ↔
∃x(F:A–1-1-onto→x ∧ x ⊆ B)) |
|
Theorem | f10 5316 |
The empty set maps one-to-one into any class. (Contributed by set.mm
contributors, 7-Apr-1998.)
|
⊢ ∅:∅–1-1→A |
|
Theorem | f1o00 5317 |
One-to-one onto mapping of the empty set. (Contributed by set.mm
contributors, 15-Apr-1998.)
|
⊢ (F:∅–1-1-onto→A ↔
(F = ∅
∧ A =
∅)) |
|
Theorem | fo00 5318 |
Onto mapping of the empty set. (Contributed by set.mm contributors,
22-Mar-2006.)
|
⊢ (F:∅–onto→A ↔
(F = ∅
∧ A =
∅)) |
|
Theorem | f1o0 5319 |
One-to-one onto mapping of the empty set. (Contributed by set.mm
contributors, 10-Feb-2004.) (Revised by set.mm contributors,
16-Feb-2004.)
|
⊢ ∅:∅–1-1-onto→∅ |
|
Theorem | f1oi 5320 |
A restriction of the identity relation is a one-to-one onto function.
(The proof was shortened by Andrew Salmon, 22-Oct-2011.) (Contributed by
set.mm contributors, 30-Apr-1998.) (Revised by set.mm contributors,
22-Oct-2011.)
|
⊢ ( I ↾
A):A–1-1-onto→A |
|
Theorem | f1ovi 5321 |
The identity relation is a one-to-one onto function on the universe.
(Contributed by set.mm contributors, 16-May-2004.)
|
⊢ I :V–1-1-onto→V |
|
Theorem | f1osn 5322 |
A singleton of an ordered pair is one-to-one onto function. (The proof
was shortened by Andrew Salmon, 22-Oct-2011.) (Contributed by set.mm
contributors, 18-May-1998.) (Revised by set.mm contributors,
22-Oct-2011.)
|
⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ {〈A, B〉}:{A}–1-1-onto→{B} |
|
Theorem | f1osng 5323 |
A singleton of an ordered pair is one-to-one onto function.
(Contributed by Mario Carneiro, 12-Jan-2013.)
|
⊢ ((A ∈ V ∧ B ∈ W) →
{〈A,
B〉}:{A}–1-1-onto→{B}) |
|
Theorem | fv2 5324* |
Alternate definition of function value. Definition 10.11 of [Quine]
p. 68. (The proof was shortened by Andrew Salmon, 17-Sep-2011.)
(Contributed by set.mm contributors, 30-Apr-2004.) (Revised by set.mm
contributors, 18-Sep-2011.)
|
⊢ (F
‘A) = ∪{x ∣ ∀y(AFy ↔
y = x)} |
|
Theorem | fvprc 5325 |
A function's value at a proper class is the empty set. (Contributed by
set.mm contributors, 20-May-1998.)
|
⊢ (¬ A
∈ V → (F ‘A) =
∅) |
|
Theorem | elfv 5326* |
Membership in a function value. (Contributed by set.mm contributors,
30-Apr-2004.)
|
⊢ (A ∈ (F
‘B) ↔ ∃x(A ∈ x ∧ ∀y(BFy ↔ y =
x))) |
|
Theorem | fveq1 5327 |
Equality theorem for function value. (Contributed by set.mm
contributors, 29-Dec-1996.)
|
⊢ (F =
G → (F ‘A) =
(G ‘A)) |
|
Theorem | fveq2 5328 |
Equality theorem for function value. (Contributed by set.mm
contributors, 29-Dec-1996.)
|
⊢ (A =
B → (F ‘A) =
(F ‘B)) |
|
Theorem | fveq1i 5329 |
Equality inference for function value. (Contributed by set.mm
contributors, 2-Sep-2003.)
|
⊢ F =
G ⇒ ⊢ (F
‘A) = (G ‘A) |
|
Theorem | fveq1d 5330 |
Equality deduction for function value. (Contributed by set.mm
contributors, 2-Sep-2003.)
|
⊢ (φ
→ F = G) ⇒ ⊢ (φ
→ (F ‘A) = (G
‘A)) |
|
Theorem | fveq2i 5331 |
Equality inference for function value. (Contributed by set.mm
contributors, 28-Jul-1999.)
|
⊢ A =
B ⇒ ⊢ (F
‘A) = (F ‘B) |
|
Theorem | fveq2d 5332 |
Equality deduction for function value. (Contributed by set.mm
contributors, 29-May-1999.)
|
⊢ (φ
→ A = B) ⇒ ⊢ (φ
→ (F ‘A) = (F
‘B)) |
|
Theorem | fveq12d 5333 |
Equality deduction for function value. (Contributed by FL,
22-Dec-2008.)
|
⊢ (φ
→ F = G)
& ⊢ (φ
→ A = B) ⇒ ⊢ (φ
→ (F ‘A) = (G
‘B)) |
|
Theorem | nffv 5334 |
Bound-variable hypothesis builder for function value. (Contributed by
NM, 14-Nov-1995.) (Revised by Mario Carneiro, 15-Oct-2016.)
|
⊢ ℲxF & ⊢ ℲxA ⇒ ⊢ Ⅎx(F
‘A) |
|
Theorem | nffvd 5335 |
Deduction version of bound-variable hypothesis builder nffv 5334.
(Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro,
15-Oct-2016.)
|
⊢ (φ
→ ℲxF)
& ⊢ (φ
→ ℲxA) ⇒ ⊢ (φ
→ Ⅎx(F ‘A)) |
|
Theorem | csbfv12g 5336 |
Move class substitution in and out of a function value. (Contributed by
NM, 11-Nov-2005.)
|
⊢ (A ∈ C →
[A / x](F
‘B) = ([A / x]F
‘[A / x]B)) |
|
Theorem | csbfv2g 5337* |
Move class substitution in and out of a function value. (Contributed by
NM, 10-Nov-2005.)
|
⊢ (A ∈ C →
[A / x](F
‘B) = (F ‘[A / x]B)) |
|
Theorem | csbfvg 5338* |
Substitution for a function value. (Contributed by NM, 1-Jan-2006.)
|
⊢ (A ∈ C →
[A / x](F
‘x) = (F ‘A)) |
|
Theorem | fvex 5339 |
The value of a class exists. Corollary 6.13 of [TakeutiZaring] p. 27.
(Contributed by set.mm contributors, 30-Dec-1996.)
|
⊢ (F
‘A) ∈ V |
|
Theorem | fvif 5340 |
Move a conditional outside of a function. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
⊢ (F ‘
if(φ, A, B)) =
if(φ, (F ‘A),
(F ‘B)) |
|
Theorem | fv3 5341* |
Alternate definition of the value of a function. Definition 6.11 of
[TakeutiZaring] p. 26.
(Contributed by NM, 30-Apr-2004.) (Revised by
Mario Carneiro, 31-Aug-2015.)
|
⊢ (F
‘A) = {x ∣ (∃y(x ∈ y ∧ AFy) ∧ ∃!y AFy)} |
|
Theorem | fvres 5342 |
The value of a restricted function. (Contributed by set.mm
contributors, 2-Aug-1994.) (Revised by set.mm contributors,
16-Feb-2004.)
|
⊢ (A ∈ B →
((F ↾
B) ‘A) = (F
‘A)) |
|
Theorem | funssfv 5343 |
The value of a member of the domain of a subclass of a function.
(Contributed by set.mm contributors, 15-Aug-1994.) (Revised by set.mm
contributors, 29-May-2007.)
|
⊢ ((Fun F
∧ G ⊆ F ∧ A ∈ dom G)
→ (F ‘A) = (G
‘A)) |
|
Theorem | tz6.12-1 5344* |
Function value. Theorem 6.12(1) of [TakeutiZaring] p. 27. (Contributed
by NM, 30-Apr-2004.)
|
⊢ ((AFB ∧ ∃!y AFy) →
(F ‘A) = B) |
|
Theorem | tz6.12 5345* |
Function value. Theorem 6.12(1) of [TakeutiZaring] p. 27. (Contributed
by NM, 10-Jul-1994.)
|
⊢ ((〈A, B〉 ∈ F ∧ ∃!y〈A, y〉 ∈ F) →
(F ‘A) = B) |
|
Theorem | tz6.12-2 5346* |
Function value when F is not
a function. Theorem 6.12(2) of
[TakeutiZaring] p. 27.
(Contributed by set.mm contributors,
30-Apr-2004.)
|
⊢ (¬ ∃!y AFy → (F
‘A) = ∅) |
|
Theorem | tz6.12c 5347* |
Corollary of Theorem 6.12(1) of [TakeutiZaring] p. 27. (Contributed by
NM, 30-Apr-2004.)
|
⊢ (∃!y AFy →
((F ‘A) = B ↔
AFB)) |
|
Theorem | tz6.12i 5348 |
Corollary of Theorem 6.12(2) of [TakeutiZaring] p. 27. (Contributed by
set.mm contributors, 30-Apr-2004.) (Revised by set.mm contributors,
6-Apr-2007.)
|
⊢ (B ≠
∅ → ((F ‘A) =
B → AFB)) |
|
Theorem | ndmfv 5349 |
The value of a class outside its domain is the empty set. (Contributed
by set.mm contributors, 24-Aug-1995.)
|
⊢ (¬ A
∈ dom F
→ (F ‘A) = ∅) |
|
Theorem | ndmfvrcl 5350 |
Reverse closure law for function with the empty set not in its domain.
(Contributed by set.mm contributors, 26-Apr-1996.)
|
⊢ dom F =
S
& ⊢ ¬ ∅
∈ S ⇒ ⊢ ((F
‘A) ∈ S →
A ∈
S) |
|
Theorem | elfvdm 5351 |
If a function value has a member, the argument belongs to the domain.
(Contributed by set.mm contributors, 12-Feb-2007.)
|
⊢ (A ∈ (F
‘B) → B ∈ dom F) |
|
Theorem | nfvres 5352 |
The value of a non-member of a restriction is the empty set. (Contributed
by set.mm contributors, 13-Nov-1995.)
|
⊢ (¬ A
∈ B
→ ((F ↾ B)
‘A) = ∅) |
|
Theorem | nfunsn 5353 |
If the restriction of a class to a singleton is not a function, its
value is the empty set. (Contributed by NM, 8-Aug-2010.) (Proof
shortened by Andrew Salmon, 22-Oct-2011.)
|
⊢ (¬ Fun (F ↾ {A}) → (F
‘A) = ∅) |
|
Theorem | fv01 5354 |
Function value of the empty set. (Contributed by Stefan O'Rear,
26-Nov-2014.)
|
⊢ (∅
‘A) = ∅ |
|
Theorem | fveqres 5355 |
Equal values imply equal values in a restriction. (Contributed by set.mm
contributors, 13-Nov-1995.)
|
⊢ ((F
‘A) = (G ‘A)
→ ((F ↾ B)
‘A) = ((G ↾ B) ‘A)) |
|
Theorem | funbrfv 5356 |
The second argument of a binary relation on a function is the function's
value. (Contributed by NM, 30-Apr-2004.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
⊢ (Fun F
→ (AFB →
(F ‘A) = B)) |
|
Theorem | funopfv 5357 |
The second element in an ordered pair member of a function is the
function's value. (Contributed by set.mm contributors, 19-Jul-1996.)
|
⊢ (Fun F
→ (〈A, B〉 ∈ F → (F
‘A) = B)) |
|
Theorem | fnbrfvb 5358 |
Equivalence of function value and binary relation. (Contributed by NM,
19-Apr-2004.) (Revised by Mario Carneiro, 28-Apr-2015.)
|
⊢ ((F Fn
A ∧
B ∈
A) → ((F ‘B) =
C ↔ BFC)) |
|
Theorem | fnopfvb 5359 |
Equivalence of function value and ordered pair membership. (Contributed
by set.mm contributors, 9-Jan-2015.)
|
⊢ ((F Fn
A ∧
B ∈
A) → ((F ‘B) =
C ↔ 〈B, C〉 ∈ F)) |
|
Theorem | funbrfvb 5360 |
Equivalence of function value and binary relation. (Contributed by set.mm
contributors, 9-Jan-2015.)
|
⊢ ((Fun F
∧ A ∈ dom F)
→ ((F ‘A) = B ↔
AFB)) |
|
Theorem | funopfvb 5361 |
Equivalence of function value and ordered pair membership. Theorem
4.3(ii) of [Monk1] p. 42. (Contributed by
set.mm contributors,
9-Jan-2015.)
|
⊢ ((Fun F
∧ A ∈ dom F)
→ ((F ‘A) = B ↔
〈A,
B〉 ∈ F)) |
|
Theorem | funbrfv2b 5362 |
Function value in terms of a binary relation. (Contributed by Mario
Carneiro, 19-Mar-2014.)
|
⊢ (Fun F
→ (AFB ↔
(A ∈ dom
F ∧
(F ‘A) = B))) |
|
Theorem | dffn5 5363* |
Representation of a function in terms of its values. (Contributed by
set.mm contributors, 29-Jan-2004.)
|
⊢ (F Fn
A ↔ F = {〈x, y〉 ∣ (x ∈ A ∧ y = (F
‘x))}) |
|
Theorem | fnrnfv 5364* |
The range of a function expressed as a collection of the function's
values. (Contributed by set.mm contributors, 20-Oct-2005.)
|
⊢ (F Fn
A → ran F = {y ∣ ∃x ∈ A y = (F ‘x)}) |
|
Theorem | fvelrnb 5365* |
A member of a function's range is a value of the function. (Contributed
by set.mm contributors, 31-Oct-1995.)
|
⊢ (F Fn
A → (B ∈ ran F ↔ ∃x ∈ A (F ‘x) =
B)) |
|
Theorem | dfimafn 5366* |
Alternate definition of the image of a function. (Contributed by Raph
Levien, 20-Nov-2006.)
|
⊢ ((Fun F
∧ A ⊆ dom F)
→ (F “ A) = {y ∣ ∃x ∈ A (F
‘x) = y}) |
|
Theorem | dfimafn2 5367* |
Alternate definition of the image of a function as an indexed union of
singletons of function values. (Contributed by Raph Levien,
20-Nov-2006.)
|
⊢ ((Fun F
∧ A ⊆ dom F)
→ (F “ A) = ∪x ∈ A {(F
‘x)}) |
|
Theorem | funimass4 5368* |
Membership relation for the values of a function whose image is a
subclass. (Contributed by Raph Levien, 20-Nov-2006.)
|
⊢ ((Fun F
∧ A ⊆ dom F)
→ ((F “ A) ⊆ B ↔ ∀x ∈ A (F ‘x)
∈ B)) |
|
Theorem | fvelima 5369* |
Function value in an image. Part of Theorem 4.4(iii) of [Monk1] p. 42.
(The proof was shortened by Andrew Salmon, 22-Oct-2011.) (Contributed
by set.mm contributors, 29-Apr-2004.) (Revised by set.mm contributors,
22-Oct-2011.)
|
⊢ ((Fun F
∧ A ∈ (F “
B)) → ∃x ∈ B (F ‘x) =
A) |
|
Theorem | fvelimab 5370* |
Function value in an image. (The proof was shortened by Andrew Salmon,
22-Oct-2011.) (An unnecessary distinct variable restriction was removed
by David Abernethy, 17-Dec-2011.) (Contributed by set.mm contributors,
20-Jan-2007.) (Revised by set.mm contributors, 25-Dec-2011.)
|
⊢ ((F Fn
A ∧
B ⊆
A) → (C ∈ (F “ B)
↔ ∃x ∈ B (F
‘x) = C)) |
|
Theorem | fniniseg 5371 |
Membership in the preimage of a singleton, under a function. (Contributed
by Mario Carneiro, 12-May-2014.)
|
⊢ (F Fn
A → (C ∈ (◡F
“ {B}) ↔ (C ∈ A ∧ (F ‘C) =
B))) |
|
Theorem | fniinfv 5372* |
The indexed intersection of a function's values is the intersection of
its range. (Contributed by set.mm contributors, 20-Oct-2005.)
|
⊢ (F Fn
A → ∩x ∈ A (F ‘x) =
∩ran F) |
|
Theorem | fnsnfv 5373 |
Singleton of function value. (Contributed by set.mm contributors,
22-May-1998.)
|
⊢ ((F Fn
A ∧
B ∈
A) → {(F ‘B)} =
(F “ {B})) |
|
Theorem | fnimapr 5374 |
The image of a pair under a function. (Contributed by Jeff Madsen,
6-Jan-2011.)
|
⊢ ((F Fn
A ∧
B ∈
A ∧
C ∈
A) → (F “ {B,
C}) = {(F ‘B),
(F ‘C)}) |
|
Theorem | funfv 5375 |
A simplified expression for the value of a function when we know it's a
function. (Contributed by NM, 22-May-1998.)
|
⊢ (Fun F
→ (F ‘A) = ∪(F “ {A})) |
|
Theorem | funfv2 5376* |
The value of a function. Definition of function value in [Enderton]
p. 43. (Contributed by set.mm contributors, 22-May-1998.) (Revised by
set.mm contributors, 11-May-2005.)
|
⊢ (Fun F
→ (F ‘A) = ∪{y ∣ AFy}) |
|
Theorem | funfv2f 5377 |
The value of a function. Version of funfv2 5376 using a bound-variable
hypotheses instead of distinct variable conditions. (Contributed by NM,
19-Feb-2006.)
|
⊢ ℲyA & ⊢ ℲyF ⇒ ⊢ (Fun F
→ (F ‘A) = ∪{y ∣ AFy}) |
|
Theorem | fvun 5378 |
Value of the union of two functions when the domains are separate.
(Contributed by FL, 7-Nov-2011.)
|
⊢ (((Fun F
∧ Fun G)
∧ (dom F
∩ dom G) = ∅) → ((F
∪ G) ‘A) = ((F
‘A) ∪ (G ‘A))) |
|
Theorem | fvun1 5379 |
The value of a union when the argument is in the first domain.
(Contributed by Scott Fenton, 29-Jun-2013.)
|
⊢ ((F Fn
A ∧
G Fn B
∧ ((A
∩ B) = ∅ ∧ X ∈ A)) → ((F
∪ G) ‘X) = (F
‘X)) |
|
Theorem | fvun2 5380 |
The value of a union when the argument is in the second domain.
(Contributed by Scott Fenton, 29-Jun-2013.)
|
⊢ ((F Fn
A ∧
G Fn B
∧ ((A
∩ B) = ∅ ∧ X ∈ B)) → ((F
∪ G) ‘X) = (G
‘X)) |
|
Theorem | dmfco 5381 |
Domains of a function composition. (Contributed by set.mm contributors,
27-Jan-1997.)
|
⊢ ((Fun G
∧ A ∈ dom G)
→ (A ∈ dom (F ∘ G) ↔
(G ‘A) ∈ dom F)) |
|
Theorem | fvco2 5382 |
Value of a function composition. Similar to second part of Theorem 3H
of [Enderton] p. 47. (The proof was
shortened by Andrew Salmon,
22-Oct-2011.) (Contributed by set.mm contributors, 9-Oct-2004.)
(Revised by set.mm contributors, 22-Oct-2011.)
|
⊢ ((G Fn
A ∧
C ∈
A) → ((F ∘ G) ‘C) =
(F ‘(G ‘C))) |
|
Theorem | fvco 5383 |
Value of a function composition. Similar to Exercise 5 of [TakeutiZaring]
p. 28. (Contributed by set.mm contributors, 22-Apr-2006.)
|
⊢ ((Fun G
∧ A ∈ dom G)
→ ((F ∘ G)
‘A) = (F ‘(G
‘A))) |
|
Theorem | fvco3 5384 |
Value of a function composition. (Contributed by set.mm contributors,
3-Jan-2004.) (Revised by set.mm contributors, 21-Aug-2006.)
|
⊢ ((G:A–→B
∧ C ∈ A) →
((F ∘
G) ‘C) = (F
‘(G ‘C))) |
|
Theorem | fvopab4t 5385* |
Closed theorem form of fvopab4 5389. (Contributed by set.mm contributors,
21-Feb-2013.)
|
⊢ ((∀x∀y(x = A → B =
C) ∧
∀x
F = {〈x, y〉 ∣ (x ∈ D ∧ y = B)} ∧ (A ∈ D ∧ C ∈ V)) → (F
‘A) = C) |
|
Theorem | fvopab3g 5386* |
Value of a function given by ordered-pair class abstraction.
(Contributed by set.mm contributors, 6-Mar-1996.)
|
⊢ B ∈ V
& ⊢ (x =
A → (φ ↔ ψ))
& ⊢ (y =
B → (ψ ↔ χ))
& ⊢ (x ∈ C →
∃!yφ)
& ⊢ F = {〈x, y〉 ∣ (x ∈ C ∧ φ)} ⇒ ⊢ (A ∈ C →
((F ‘A) = B ↔
χ)) |
|
Theorem | fvopab3ig 5387* |
Value of a function given by ordered-pair class abstraction.
(Contributed by set.mm contributors, 23-Oct-1999.)
|
⊢ (x =
A → (φ ↔ ψ))
& ⊢ (y =
B → (ψ ↔ χ))
& ⊢ (x ∈ C →
∃*yφ)
& ⊢ F = {〈x, y〉 ∣ (x ∈ C ∧ φ)} ⇒ ⊢ ((A ∈ C ∧ B ∈ D) →
(χ → (F ‘A) =
B)) |
|
Theorem | fvopab4g 5388* |
Value of a function given by ordered-pair class abstraction.
(Contributed by set.mm contributors, 23-Oct-1999.)
|
⊢ (x =
A → B = C)
& ⊢ F = {〈x, y〉 ∣ (x ∈ D ∧ y = B)} ⇒ ⊢ ((A ∈ D ∧ C ∈ R) →
(F ‘A) = C) |
|
Theorem | fvopab4 5389* |
Value of a function given by ordered-pair class abstraction.
(Contributed by set.mm contributors, 23-Oct-1999.)
|
⊢ (x =
A → B = C)
& ⊢ F = {〈x, y〉 ∣ (x ∈ D ∧ y = B)}
& ⊢ C ∈ V ⇒ ⊢ (A ∈ D →
(F ‘A) = C) |
|
Theorem | fvopab4ndm 5390* |
Value of a function given by an ordered-pair class abstraction, outside
of its domain. (Contributed by set.mm contributors, 28-Mar-2008.)
|
⊢ F = {〈x, y〉 ∣ (x ∈ A ∧ φ)} ⇒ ⊢ (¬ B
∈ A
→ (F ‘B) = ∅) |
|
Theorem | fvopabg 5391* |
The value of a function given by ordered-pair class abstraction.
(Contributed by set.mm contributors, 2-Sep-2003.)
|
⊢ (x =
A → B = C) ⇒ ⊢ ((A ∈ V ∧ C ∈ W) →
({〈x,
y〉 ∣ y =
B} ‘A) = C) |
|
Theorem | eqfnfv 5392* |
Equality of functions is determined by their values. Special case of
Exercise 4 of [TakeutiZaring] p.
28 (with domain equality omitted).
(The proof was shortened by Andrew Salmon, 22-Oct-2011.) (Contributed
by set.mm contributors, 3-Aug-1994.) (Revised by set.mm contributors,
22-Oct-2011.)
|
⊢ ((F Fn
A ∧
G Fn A) → (F =
G ↔ ∀x ∈ A (F ‘x) =
(G ‘x))) |
|
Theorem | eqfnfv2 5393* |
Equality of functions is determined by their values. Exercise 4 of
[TakeutiZaring] p. 28.
(Contributed by set.mm contributors,
3-Aug-1994.) (Revised by set.mm contributors, 5-Feb-2004.)
|
⊢ ((F Fn
A ∧
G Fn B) → (F =
G ↔ (A = B ∧ ∀x ∈ A (F
‘x) = (G ‘x)))) |
|
Theorem | eqfnfv3 5394* |
Derive equality of functions from equality of their values.
(Contributed by Jeff Madsen, 2-Sep-2009.)
|
⊢ ((F Fn
A ∧
G Fn B) → (F =
G ↔ (B ⊆ A ∧ ∀x ∈ A (x ∈ B ∧ (F ‘x) =
(G ‘x))))) |
|
Theorem | eqfnfvd 5395* |
Deduction for equality of functions. (Contributed by Mario Carneiro,
24-Jul-2014.)
|
⊢ (φ
→ F Fn A)
& ⊢ (φ
→ G Fn A)
& ⊢ ((φ
∧ x ∈ A) →
(F ‘x) = (G
‘x)) ⇒ ⊢ (φ
→ F = G) |
|
Theorem | eqfnfv2f 5396* |
Equality of functions is determined by their values. Special case of
Exercise 4 of [TakeutiZaring] p.
28 (with domain equality omitted).
This version of eqfnfv 5392 uses bound-variable hypotheses instead of
distinct variable conditions. (Contributed by NM, 29-Jan-2004.)
|
⊢ ℲxF & ⊢ ℲxG ⇒ ⊢ ((F Fn
A ∧
G Fn A) → (F =
G ↔ ∀x ∈ A (F ‘x) =
(G ‘x))) |
|
Theorem | eqfunfv 5397* |
Equality of functions is determined by their values. (Contributed by
Scott Fenton, 19-Jun-2011.)
|
⊢ ((Fun F
∧ Fun G)
→ (F = G ↔ (dom F
= dom G ∧
∀x
∈ dom F(F
‘x) = (G ‘x)))) |
|
Theorem | fvreseq 5398* |
Equality of restricted functions is determined by their values.
(Contributed by set.mm contributors, 3-Aug-1994.) (Revised by set.mm
contributors, 6-Feb-2004.)
|
⊢ (((F Fn
A ∧
G Fn A) ∧ B ⊆ A) → ((F
↾ B) =
(G ↾
B) ↔ ∀x ∈ B (F ‘x) =
(G ‘x))) |
|
Theorem | chfnrn 5399* |
The range of a choice function (a function that chooses an element from
each member of its domain) is included in the union of its domain.
(Contributed by set.mm contributors, 31-Aug-1999.)
|
⊢ ((F Fn
A ∧ ∀x ∈ A (F ‘x)
∈ x)
→ ran F ⊆ ∪A) |
|
Theorem | funfvop 5400 |
Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1]
p. 41. (Contributed by set.mm contributors, 14-Oct-1996.)
|
⊢ ((Fun F
∧ A ∈ dom F)
→ 〈A, (F
‘A)〉 ∈ F) |