P. 68 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 6701-6800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dffo2 6701	Alternate definition of an onto function. (Contributed by NM, 22-Mar-2006.)
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵))
Theorem	foima 6702	The image of the domain of an onto function. (Contributed by NM, 29-Nov-2002.)
⊢ (𝐹:𝐴–onto→𝐵 → (𝐹 “ 𝐴) = 𝐵)
Theorem	dffn4 6703	A function maps onto its range. (Contributed by NM, 10-May-1998.)
⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴–onto→ran 𝐹)
Theorem	funforn 6704	A function maps its domain onto its range. (Contributed by NM, 23-Jul-2004.)
⊢ (Fun 𝐴 ↔ 𝐴:dom 𝐴–onto→ran 𝐴)
Theorem	fodmrnu 6705	An onto function has unique domain and range. (Contributed by NM, 5-Nov-2006.)
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐹:𝐶–onto→𝐷) → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	fimadmfo 6706	A function is a function onto the image of its domain. (Contributed by AV, 1-Dec-2022.)
⊢ (𝐹:𝐴⟶𝐵 → 𝐹:𝐴–onto→(𝐹 “ 𝐴))
Theorem	fores 6707	Restriction of an onto function. (Contributed by NM, 4-Mar-1997.)
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐹 ↾ 𝐴):𝐴–onto→(𝐹 “ 𝐴))
Theorem	fimadmfoALT 6708	Alternate proof of fimadmfo 6706, based on fores 6707. A function is a function onto the image of its domain. (Contributed by AV, 1-Dec-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐹:𝐴⟶𝐵 → 𝐹:𝐴–onto→(𝐹 “ 𝐴))
Theorem	focnvimacdmdm 6709	The preimage of the codomain of a surjection is its domain. (Contributed by AV, 29-Sep-2024.)
⊢ (𝐺:𝐴–onto→𝐵 → (◡𝐺 “ 𝐵) = 𝐴)
Theorem	focofo 6710	Composition of onto functions. Generalisation of foco 6711. (Contributed by AV, 29-Sep-2024.)
⊢ ((𝐹:𝐴–onto→𝐵 ∧ Fun 𝐺 ∧ 𝐴 ⊆ ran 𝐺) → (𝐹 ∘ 𝐺):(◡𝐺 “ 𝐴)–onto→𝐵)
Theorem	foco 6711	Composition of onto functions. (Contributed by NM, 22-Mar-2006.) (Proof shortened by AV, 29-Sep-2024.)
⊢ ((𝐹:𝐵–onto→𝐶 ∧ 𝐺:𝐴–onto→𝐵) → (𝐹 ∘ 𝐺):𝐴–onto→𝐶)
Theorem	foconst 6712	A nonzero constant function is onto. (Contributed by NM, 12-Jan-2007.)
⊢ ((𝐹:𝐴⟶{𝐵} ∧ 𝐹 ≠ ∅) → 𝐹:𝐴–onto→{𝐵})
Theorem	f1oeq1 6713	Equality theorem for one-to-one onto functions. (Contributed by NM, 10-Feb-1997.)
⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1-onto→𝐵 ↔ 𝐺:𝐴–1-1-onto→𝐵))
Theorem	f1oeq2 6714	Equality theorem for one-to-one onto functions. (Contributed by NM, 10-Feb-1997.)
⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐶))
Theorem	f1oeq3 6715	Equality theorem for one-to-one onto functions. (Contributed by NM, 10-Feb-1997.)
⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵))
Theorem	f1oeq23 6716	Equality theorem for one-to-one onto functions. (Contributed by FL, 14-Jul-2012.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐷))
Theorem	f1eq123d 6717	Equality deduction for one-to-one functions. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐺:𝐵–1-1→𝐷))
Theorem	foeq123d 6718	Equality deduction for onto functions. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐹:𝐴–onto→𝐶 ↔ 𝐺:𝐵–onto→𝐷))
Theorem	f1oeq123d 6719	Equality deduction for one-to-one onto functions. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐷))
Theorem	f1oeq1d 6720	Equality deduction for one-to-one onto functions. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐹 = 𝐺)    ⇒   ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐵 ↔ 𝐺:𝐴–1-1-onto→𝐵))
Theorem	f1oeq2d 6721	Equality deduction for one-to-one onto functions. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐶))
Theorem	f1oeq3d 6722	Equality deduction for one-to-one onto functions. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵))
Theorem	nff1o 6723	Bound-variable hypothesis builder for a one-to-one onto function. (Contributed by NM, 16-May-2004.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐹:𝐴–1-1-onto→𝐵
Theorem	f1of1 6724	A one-to-one onto mapping is a one-to-one mapping. (Contributed by NM, 12-Dec-2003.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–1-1→𝐵)
Theorem	f1of 6725	A one-to-one onto mapping is a mapping. (Contributed by NM, 12-Dec-2003.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵)
Theorem	f1ofn 6726	A one-to-one onto mapping is function on its domain. (Contributed by NM, 12-Dec-2003.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹 Fn 𝐴)
Theorem	f1ofun 6727	A one-to-one onto mapping is a function. (Contributed by NM, 12-Dec-2003.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 → Fun 𝐹)
Theorem	f1orel 6728	A one-to-one onto mapping is a relation. (Contributed by NM, 13-Dec-2003.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 → Rel 𝐹)
Theorem	f1odm 6729	The domain of a one-to-one onto mapping. (Contributed by NM, 8-Mar-2014.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 → dom 𝐹 = 𝐴)
Theorem	dff1o2 6730	Alternate definition of one-to-one onto function. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
Theorem	dff1o3 6731	Alternate definition of one-to-one onto function. (Contributed by NM, 25-Mar-1998.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹))
Theorem	f1ofo 6732	A one-to-one onto function is an onto function. (Contributed by NM, 28-Apr-2004.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–onto→𝐵)
Theorem	dff1o4 6733	Alternate definition of one-to-one onto function. (Contributed by NM, 25-Mar-1998.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
Theorem	dff1o5 6734	Alternate definition of one-to-one onto function. (Contributed by NM, 10-Dec-2003.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 = 𝐵))
Theorem	f1orn 6735	A one-to-one function maps onto its range. (Contributed by NM, 13-Aug-2004.)
⊢ (𝐹:𝐴–1-1-onto→ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹))
Theorem	f1f1orn 6736	A one-to-one function maps one-to-one onto its range. (Contributed by NM, 4-Sep-2004.)
⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴–1-1-onto→ran 𝐹)
Theorem	f1ocnv 6737	The converse of a one-to-one onto function is also one-to-one onto. (Contributed by NM, 11-Feb-1997.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)
Theorem	f1ocnvb 6738	A relation is a one-to-one onto function iff its converse is a one-to-one onto function with domain and range interchanged. (Contributed by NM, 8-Dec-2003.)
⊢ (Rel 𝐹 → (𝐹:𝐴–1-1-onto→𝐵 ↔ ◡𝐹:𝐵–1-1-onto→𝐴))
Theorem	f1ores 6739	The restriction of a one-to-one function maps one-to-one onto the image. (Contributed by NM, 25-Mar-1998.)
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶–1-1-onto→(𝐹 “ 𝐶))
Theorem	f1orescnv 6740	The converse of a one-to-one-onto restricted function. (Contributed by Paul Chapman, 21-Apr-2008.)
⊢ ((Fun ◡𝐹 ∧ (𝐹 ↾ 𝑅):𝑅–1-1-onto→𝑃) → (◡𝐹 ↾ 𝑃):𝑃–1-1-onto→𝑅)
Theorem	f1imacnv 6741	Preimage of an image. (Contributed by NM, 30-Sep-2004.)
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴) → (◡𝐹 “ (𝐹 “ 𝐶)) = 𝐶)
Theorem	foimacnv 6742	A reverse version of f1imacnv 6741. (Contributed by Jeff Hankins, 16-Jul-2009.)
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → (𝐹 “ (◡𝐹 “ 𝐶)) = 𝐶)
Theorem	foun 6743	The union of two onto functions with disjoint domains is an onto function. (Contributed by Mario Carneiro, 22-Jun-2016.)
⊢ (((𝐹:𝐴–onto→𝐵 ∧ 𝐺:𝐶–onto→𝐷) ∧ (𝐴 ∩ 𝐶) = ∅) → (𝐹 ∪ 𝐺):(𝐴 ∪ 𝐶)–onto→(𝐵 ∪ 𝐷))
Theorem	f1oun 6744	The union of two one-to-one onto functions with disjoint domains and ranges. (Contributed by NM, 26-Mar-1998.)
⊢ (((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷) ∧ ((𝐴 ∩ 𝐶) = ∅ ∧ (𝐵 ∩ 𝐷) = ∅)) → (𝐹 ∪ 𝐺):(𝐴 ∪ 𝐶)–1-1-onto→(𝐵 ∪ 𝐷))
Theorem	f1un 6745	The union of two one-to-one functions with disjoint domains and codomains. (Contributed by BTernaryTau, 3-Dec-2024.)
⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐶–1-1→𝐷) ∧ ((𝐴 ∩ 𝐶) = ∅ ∧ (𝐵 ∩ 𝐷) = ∅)) → (𝐹 ∪ 𝐺):(𝐴 ∪ 𝐶)–1-1→(𝐵 ∪ 𝐷))
Theorem	resdif 6746	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 ◡𝐹 ∧ (𝐹 ↾ 𝐴):𝐴–onto→𝐶 ∧ (𝐹 ↾ 𝐵):𝐵–onto→𝐷) → (𝐹 ↾ (𝐴 ∖ 𝐵)):(𝐴 ∖ 𝐵)–1-1-onto→(𝐶 ∖ 𝐷))
Theorem	resin 6747	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 ◡𝐹 ∧ (𝐹 ↾ 𝐴):𝐴–onto→𝐶 ∧ (𝐹 ↾ 𝐵):𝐵–onto→𝐷) → (𝐹 ↾ (𝐴 ∩ 𝐵)):(𝐴 ∩ 𝐵)–1-1-onto→(𝐶 ∩ 𝐷))
Theorem	f1oco 6748	Composition of one-to-one onto functions. (Contributed by NM, 19-Mar-1998.)
⊢ ((𝐹:𝐵–1-1-onto→𝐶 ∧ 𝐺:𝐴–1-1-onto→𝐵) → (𝐹 ∘ 𝐺):𝐴–1-1-onto→𝐶)
Theorem	f1cnv 6749	The converse of an injective function is bijective. (Contributed by FL, 11-Nov-2011.)
⊢ (𝐹:𝐴–1-1→𝐵 → ◡𝐹:ran 𝐹–1-1-onto→𝐴)
Theorem	funcocnv2 6750	Composition with the converse. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (Fun 𝐹 → (𝐹 ∘ ◡𝐹) = ( I ↾ ran 𝐹))
Theorem	fococnv2 6751	The composition of an onto function and its converse. (Contributed by Stefan O'Rear, 12-Feb-2015.)
⊢ (𝐹:𝐴–onto→𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ 𝐵))
Theorem	f1ococnv2 6752	The composition of a one-to-one onto function and its converse equals the identity relation restricted to the function's range. (Contributed by NM, 13-Dec-2003.) (Proof shortened by Stefan O'Rear, 12-Feb-2015.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ 𝐵))
Theorem	f1cocnv2 6753	Composition of an injective function with its converse. (Contributed by FL, 11-Nov-2011.)
⊢ (𝐹:𝐴–1-1→𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ ran 𝐹))
Theorem	f1ococnv1 6754	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 NM, 13-Dec-2003.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 → (◡𝐹 ∘ 𝐹) = ( I ↾ 𝐴))
Theorem	f1cocnv1 6755	Composition of an injective function with its converse. (Contributed by FL, 11-Nov-2011.)
⊢ (𝐹:𝐴–1-1→𝐵 → (◡𝐹 ∘ 𝐹) = ( I ↾ 𝐴))
Theorem	funcoeqres 6756	Express a constraint on a composition as a constraint on the composand. (Contributed by Stefan O'Rear, 7-Mar-2015.)
⊢ ((Fun 𝐺 ∧ (𝐹 ∘ 𝐺) = 𝐻) → (𝐹 ↾ ran 𝐺) = (𝐻 ∘ ◡𝐺))
Theorem	f1ssf1 6757	A subset of an injective function is injective. (Contributed by AV, 20-Nov-2020.)
⊢ ((Fun 𝐹 ∧ Fun ◡𝐹 ∧ 𝐺 ⊆ 𝐹) → Fun ◡𝐺)
Theorem	f10 6758	The empty set maps one-to-one into any class. (Contributed by NM, 7-Apr-1998.)
⊢ ∅:∅–1-1→𝐴
Theorem	f10d 6759	The empty set maps one-to-one into any class, deduction version. (Contributed by AV, 25-Nov-2020.)
⊢ (𝜑 → 𝐹 = ∅)    ⇒   ⊢ (𝜑 → 𝐹:dom 𝐹–1-1→𝐴)
Theorem	f1o00 6760	One-to-one onto mapping of the empty set. (Contributed by NM, 15-Apr-1998.)
⊢ (𝐹:∅–1-1-onto→𝐴 ↔ (𝐹 = ∅ ∧ 𝐴 = ∅))
Theorem	fo00 6761	Onto mapping of the empty set. (Contributed by NM, 22-Mar-2006.)
⊢ (𝐹:∅–onto→𝐴 ↔ (𝐹 = ∅ ∧ 𝐴 = ∅))
Theorem	f1o0 6762	One-to-one onto mapping of the empty set. (Contributed by NM, 10-Sep-2004.)
⊢ ∅:∅–1-1-onto→∅
Theorem	f1oi 6763	A restriction of the identity relation is a one-to-one onto function. (Contributed by NM, 30-Apr-1998.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴
Theorem	f1ovi 6764	The identity relation is a one-to-one onto function on the universe. (Contributed by NM, 16-May-2004.)
⊢ I :V–1-1-onto→V
Theorem	f1osn 6765	A singleton of an ordered pair is one-to-one onto function. (Contributed by NM, 18-May-1998.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ {⟨𝐴, 𝐵⟩}:{𝐴}–1-1-onto→{𝐵}
Theorem	f1osng 6766	A singleton of an ordered pair is one-to-one onto function. (Contributed by Mario Carneiro, 12-Jan-2013.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {⟨𝐴, 𝐵⟩}:{𝐴}–1-1-onto→{𝐵})
Theorem	f1sng 6767	A singleton of an ordered pair is a one-to-one function. (Contributed by AV, 17-Apr-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {⟨𝐴, 𝐵⟩}:{𝐴}–1-1→𝑊)
Theorem	fsnd 6768	A singleton of an ordered pair is a function. (Contributed by AV, 17-Apr-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → {⟨𝐴, 𝐵⟩}:{𝐴}⟶𝑊)
Theorem	f1oprswap 6769	A two-element swap is a bijection on a pair. (Contributed by Mario Carneiro, 23-Jan-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {⟨𝐴, 𝐵⟩, ⟨𝐵, 𝐴⟩}:{𝐴, 𝐵}–1-1-onto→{𝐴, 𝐵})
Theorem	f1oprg 6770	An unordered pair of ordered pairs with different elements is a one-to-one onto function, analogous to f1oprswap 6769. (Contributed by Alexander van der Vekens, 14-Aug-2017.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) → {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩}:{𝐴, 𝐶}–1-1-onto→{𝐵, 𝐷}))
Theorem	tz6.12-2 6771*	Function value when 𝐹 is not a function. Theorem 6.12(2) of [TakeutiZaring] p. 27. (Contributed by NM, 30-Apr-2004.) (Proof shortened by Mario Carneiro, 31-Aug-2015.)
⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅)
Theorem	fveu 6772*	The value of a function at a unique point. (Contributed by Scott Fenton, 6-Oct-2017.)
⊢ (∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∪ {𝑥 ∣ 𝐴𝐹𝑥})
Theorem	brprcneu 6773*	If 𝐴 is a proper class and 𝐹 is any class, then there is no unique set which is related to 𝐴 through the binary relation 𝐹. See brprcneuALT 6774 for a proof that uses ax-pow 5289 instead of ax-pr 5353. (Contributed by Scott Fenton, 7-Oct-2017.)
⊢ (¬ 𝐴 ∈ V → ¬ ∃!𝑥 𝐴𝐹𝑥)
Theorem	brprcneuALT 6774*	Alternate proof of brprcneu 6773 using ax-pow 5289 instead of ax-pr 5353. (Contributed by Scott Fenton, 7-Oct-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ 𝐴 ∈ V → ¬ ∃!𝑥 𝐴𝐹𝑥)
Theorem	fvprc 6775	A function's value at a proper class is the empty set. See fvprcALT 6776 for a proof that uses ax-pow 5289 instead of ax-pr 5353. (Contributed by NM, 20-May-1998.) Avoid ax-pow 5289. (Revised by BTernaryTau, 3-Aug-2024.) (Proof shortened by BTernaryTau, 3-Dec-2024.)
⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅)
Theorem	fvprcALT 6776	Alternate proof of fvprc 6775 using ax-pow 5289 instead of ax-pr 5353. (Contributed by NM, 20-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅)
Theorem	rnfvprc 6777	The range of a function value at a proper class is empty. (Contributed by AV, 20-Aug-2022.)
⊢ 𝑌 = (𝐹‘𝑋)    ⇒   ⊢ (¬ 𝑋 ∈ V → ran 𝑌 = ∅)
Theorem	fv2 6778*	Alternate definition of function value. Definition 10.11 of [Quine] p. 68. (Contributed by NM, 30-Apr-2004.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) (Revised by Mario Carneiro, 31-Aug-2015.)
⊢ (𝐹‘𝐴) = ∪ {𝑥 ∣ ∀𝑦(𝐴𝐹𝑦 ↔ 𝑦 = 𝑥)}
Theorem	dffv3 6779*	A definition of function value in terms of iota. (Contributed by Scott Fenton, 19-Feb-2013.)
⊢ (𝐹‘𝐴) = (℩𝑥𝑥 ∈ (𝐹 “ {𝐴}))
Theorem	dffv4 6780*	The previous definition of function value, from before the ℩ operator was introduced. Although based on the idea embodied by Definition 10.2 of [Quine] p. 65 (see args 6003), this definition apparently does not appear in the literature. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐹‘𝐴) = ∪ {𝑥 ∣ (𝐹 “ {𝐴}) = {𝑥}}
Theorem	elfv 6781*	Membership in a function value. (Contributed by NM, 30-Apr-2004.)
⊢ (𝐴 ∈ (𝐹‘𝐵) ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ ∀𝑦(𝐵𝐹𝑦 ↔ 𝑦 = 𝑥)))
Theorem	fveq1 6782	Equality theorem for function value. (Contributed by NM, 29-Dec-1996.)
⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))
Theorem	fveq2 6783	Equality theorem for function value. (Contributed by NM, 29-Dec-1996.)
⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))
Theorem	fveq1i 6784	Equality inference for function value. (Contributed by NM, 2-Sep-2003.)
⊢ 𝐹 = 𝐺    ⇒   ⊢ (𝐹‘𝐴) = (𝐺‘𝐴)
Theorem	fveq1d 6785	Equality deduction for function value. (Contributed by NM, 2-Sep-2003.)
⊢ (𝜑 → 𝐹 = 𝐺)    ⇒   ⊢ (𝜑 → (𝐹‘𝐴) = (𝐺‘𝐴))
Theorem	fveq2i 6786	Equality inference for function value. (Contributed by NM, 28-Jul-1999.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐹‘𝐴) = (𝐹‘𝐵)
Theorem	fveq2d 6787	Equality deduction for function value. (Contributed by NM, 29-May-1999.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹‘𝐴) = (𝐹‘𝐵))
Theorem	2fveq3 6788	Equality theorem for nested function values. (Contributed by AV, 14-Aug-2022.)
⊢ (𝐴 = 𝐵 → (𝐹‘(𝐺‘𝐴)) = (𝐹‘(𝐺‘𝐵)))
Theorem	fveq12i 6789	Equality deduction for function value. (Contributed by FL, 27-Jun-2014.)
⊢ 𝐹 = 𝐺    &   ⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐹‘𝐴) = (𝐺‘𝐵)
Theorem	fveq12d 6790	Equality deduction for function value. (Contributed by FL, 22-Dec-2008.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹‘𝐴) = (𝐺‘𝐵))
Theorem	fveqeq2d 6791	Equality deduction for function value. (Contributed by BJ, 30-Aug-2022.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ((𝐹‘𝐴) = 𝐶 ↔ (𝐹‘𝐵) = 𝐶))
Theorem	fveqeq2 6792	Equality deduction for function value. (Contributed by BJ, 31-Aug-2022.)
⊢ (𝐴 = 𝐵 → ((𝐹‘𝐴) = 𝐶 ↔ (𝐹‘𝐵) = 𝐶))
Theorem	nffv 6793	Bound-variable hypothesis builder for function value. (Contributed by NM, 14-Nov-1995.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥(𝐹‘𝐴)
Theorem	nffvmpt1 6794*	Bound-variable hypothesis builder for mapping, special case. (Contributed by Mario Carneiro, 25-Dec-2016.)
⊢ Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝐶)
Theorem	nffvd 6795	Deduction version of bound-variable hypothesis builder nffv 6793. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝐹)    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥(𝐹‘𝐴))
Theorem	fvex 6796	The value of a class exists. Corollary 6.13 of [TakeutiZaring] p. 27. (Contributed by NM, 30-Dec-1996.)
⊢ (𝐹‘𝐴) ∈ V
Theorem	fvexi 6797	The value of a class exists. Inference form of fvex 6796. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ 𝐴 = (𝐹‘𝐵)    ⇒   ⊢ 𝐴 ∈ V
Theorem	fvexd 6798	The value of a class exists (as consequent of anything). (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → (𝐹‘𝐴) ∈ V)
Theorem	fvif 6799	Move a conditional outside of a function. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝐹‘if(𝜑, 𝐴, 𝐵)) = if(𝜑, (𝐹‘𝐴), (𝐹‘𝐵))
Theorem	iffv 6800	Move a conditional outside of a function. (Contributed by Thierry Arnoux, 28-Sep-2018.)
⊢ (if(𝜑, 𝐹, 𝐺)‘𝐴) = if(𝜑, (𝐹‘𝐴), (𝐺‘𝐴))