P. 55 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 5401-5500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sbcfng 5401*	Distribute proper substitution through the function predicate with a domain. (Contributed by Alexander van der Vekens, 15-Jul-2018.)
⊢ (𝑋 ∈ 𝑉 → ([𝑋 / 𝑥]𝐹 Fn 𝐴 ↔ ⦋𝑋 / 𝑥⦌𝐹 Fn ⦋𝑋 / 𝑥⦌𝐴))
Theorem	sbcfg 5402*	Distribute proper substitution through the function predicate with domain and codomain. (Contributed by Alexander van der Vekens, 15-Jul-2018.)
⊢ (𝑋 ∈ 𝑉 → ([𝑋 / 𝑥]𝐹:𝐴⟶𝐵 ↔ ⦋𝑋 / 𝑥⦌𝐹:⦋𝑋 / 𝑥⦌𝐴⟶⦋𝑋 / 𝑥⦌𝐵))
Theorem	ffn 5403	A mapping is a function. (Contributed by NM, 2-Aug-1994.)
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
Theorem	ffnd 5404	A mapping is a function with domain, deduction form. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ (𝜑 → 𝐹 Fn 𝐴)
Theorem	dffn2 5405	Any function is a mapping into V. (Contributed by NM, 31-Oct-1995.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶V)
Theorem	ffun 5406	A mapping is a function. (Contributed by NM, 3-Aug-1994.)
⊢ (𝐹:𝐴⟶𝐵 → Fun 𝐹)
Theorem	ffund 5407	A mapping is a function, deduction version. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ (𝜑 → Fun 𝐹)
Theorem	frel 5408	A mapping is a relation. (Contributed by NM, 3-Aug-1994.)
⊢ (𝐹:𝐴⟶𝐵 → Rel 𝐹)
Theorem	fdm 5409	The domain of a mapping. (Contributed by NM, 2-Aug-1994.)
⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)
Theorem	fdmd 5410	Deduction form of fdm 5409. The domain of a mapping. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ (𝜑 → dom 𝐹 = 𝐴)
Theorem	fdmi 5411	The domain of a mapping. (Contributed by NM, 28-Jul-2008.)
⊢ 𝐹:𝐴⟶𝐵    ⇒   ⊢ dom 𝐹 = 𝐴
Theorem	frn 5412	The range of a mapping. (Contributed by NM, 3-Aug-1994.)
⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
Theorem	frnd 5413	Deduction form of frn 5412. The range of a mapping. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ (𝜑 → ran 𝐹 ⊆ 𝐵)
Theorem	dffn3 5414	A function maps to its range. (Contributed by NM, 1-Sep-1999.)
⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶ran 𝐹)
Theorem	fss 5415	Expanding the codomain of a mapping. (Contributed by NM, 10-May-1998.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
Theorem	fssd 5416	Expanding the codomain of a mapping, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → 𝐹:𝐴⟶𝐶)
Theorem	fssdmd 5417	Expressing that a class is a subclass of the domain of a function expressed in maps-to notation, deduction form. (Contributed by AV, 21-Aug-2022.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐷 ⊆ dom 𝐹)    ⇒   ⊢ (𝜑 → 𝐷 ⊆ 𝐴)
Theorem	fssdm 5418	Expressing that a class is a subclass of the domain of a function expressed in maps-to notation, semi-deduction form. (Contributed by AV, 21-Aug-2022.)
⊢ 𝐷 ⊆ dom 𝐹    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ (𝜑 → 𝐷 ⊆ 𝐴)
Theorem	fco 5419	Composition of two mappings. (Contributed by NM, 29-Aug-1999.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):𝐴⟶𝐶)
Theorem	fco2 5420	Functionality of a composition with weakened out of domain condition on the first argument. (Contributed by Stefan O'Rear, 11-Mar-2015.)
⊢ (((𝐹 ↾ 𝐵):𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):𝐴⟶𝐶)
Theorem	fssxp 5421	A mapping is a class of ordered pairs. (Contributed by NM, 3-Aug-1994.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 ⊆ (𝐴 × 𝐵))
Theorem	fex2 5422	A function with bounded domain and codomain is a set. This version is proven without the Axiom of Replacement. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ∈ V)
Theorem	funssxp 5423	Two ways of specifying a partial function from 𝐴 to 𝐵. (Contributed by NM, 13-Nov-2007.)
⊢ ((Fun 𝐹 ∧ 𝐹 ⊆ (𝐴 × 𝐵)) ↔ (𝐹:dom 𝐹⟶𝐵 ∧ dom 𝐹 ⊆ 𝐴))
Theorem	ffdm 5424	A mapping is a partial function. (Contributed by NM, 25-Nov-2007.)
⊢ (𝐹:𝐴⟶𝐵 → (𝐹:dom 𝐹⟶𝐵 ∧ dom 𝐹 ⊆ 𝐴))
Theorem	opelf 5425	The members of an ordered pair element of a mapping belong to the mapping's domain and codomain. (Contributed by NM, 10-Dec-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ ⟨𝐶, 𝐷⟩ ∈ 𝐹) → (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵))
Theorem	fun 5426	The union of two functions with disjoint domains. (Contributed by NM, 22-Sep-2004.)
⊢ (((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐷) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐹 ∪ 𝐺):(𝐴 ∪ 𝐵)⟶(𝐶 ∪ 𝐷))
Theorem	fun2 5427	The union of two functions with disjoint domains. (Contributed by Mario Carneiro, 12-Mar-2015.)
⊢ (((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐹 ∪ 𝐺):(𝐴 ∪ 𝐵)⟶𝐶)
Theorem	fnfco 5428	Composition of two functions. (Contributed by NM, 22-May-2006.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺:𝐵⟶𝐴) → (𝐹 ∘ 𝐺) Fn 𝐵)
Theorem	fssres 5429	Restriction of a function with a subclass of its domain. (Contributed by NM, 23-Sep-2004.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶𝐵)
Theorem	fssresd 5430	Restriction of a function with a subclass of its domain, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (𝐹 ↾ 𝐶):𝐶⟶𝐵)
Theorem	fssres2 5431	Restriction of a restricted function with a subclass of its domain. (Contributed by NM, 21-Jul-2005.)
⊢ (((𝐹 ↾ 𝐴):𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶𝐵)
Theorem	fresin 5432	An identity for the mapping relationship under restriction. (Contributed by Scott Fenton, 4-Sep-2011.) (Proof shortened by Mario Carneiro, 26-May-2016.)
⊢ (𝐹:𝐴⟶𝐵 → (𝐹 ↾ 𝑋):(𝐴 ∩ 𝑋)⟶𝐵)
Theorem	resasplitss 5433	If two functions agree on their common domain, their union contains a union of three functions with pairwise disjoint domains. If we assumed the law of the excluded middle, this would be equality rather than subset. (Contributed by Jim Kingdon, 28-Dec-2018.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → ((𝐹 ↾ (𝐴 ∩ 𝐵)) ∪ ((𝐹 ↾ (𝐴 ∖ 𝐵)) ∪ (𝐺 ↾ (𝐵 ∖ 𝐴)))) ⊆ (𝐹 ∪ 𝐺))
Theorem	fcoi1 5434	Composition of a mapping and restricted identity. (Contributed by NM, 13-Dec-2003.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ (𝐹:𝐴⟶𝐵 → (𝐹 ∘ ( I ↾ 𝐴)) = 𝐹)
Theorem	fcoi2 5435	Composition of restricted identity and a mapping. (Contributed by NM, 13-Dec-2003.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ (𝐹:𝐴⟶𝐵 → (( I ↾ 𝐵) ∘ 𝐹) = 𝐹)
Theorem	feu 5436*	There is exactly one value of a function in its codomain. (Contributed by NM, 10-Dec-2003.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → ∃!𝑦 ∈ 𝐵 ⟨𝐶, 𝑦⟩ ∈ 𝐹)
Theorem	fcnvres 5437	The converse of a restriction of a function. (Contributed by NM, 26-Mar-1998.)
⊢ (𝐹:𝐴⟶𝐵 → ◡(𝐹 ↾ 𝐴) = (◡𝐹 ↾ 𝐵))
Theorem	fimacnvdisj 5438	The preimage of a class disjoint with a mapping's codomain is empty. (Contributed by FL, 24-Jan-2007.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ (𝐵 ∩ 𝐶) = ∅) → (◡𝐹 “ 𝐶) = ∅)
Theorem	fintm 5439*	Function into an intersection. (Contributed by Jim Kingdon, 28-Dec-2018.)
⊢ ∃𝑥 𝑥 ∈ 𝐵    ⇒   ⊢ (𝐹:𝐴⟶∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐹:𝐴⟶𝑥)
Theorem	fin 5440	Mapping into an intersection. (Contributed by NM, 14-Sep-1999.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ (𝐹:𝐴⟶(𝐵 ∩ 𝐶) ↔ (𝐹:𝐴⟶𝐵 ∧ 𝐹:𝐴⟶𝐶))
Theorem	fabexg 5441*	Existence of a set of functions. (Contributed by Paul Chapman, 25-Feb-2008.)
⊢ 𝐹 = {𝑥 ∣ (𝑥:𝐴⟶𝐵 ∧ 𝜑)}    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝐹 ∈ V)
Theorem	fabex 5442*	Existence of a set of functions. (Contributed by NM, 3-Dec-2007.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐹 = {𝑥 ∣ (𝑥:𝐴⟶𝐵 ∧ 𝜑)}    ⇒   ⊢ 𝐹 ∈ V
Theorem	dmfex 5443	If a mapping is a set, its domain is a set. (Contributed by NM, 27-Aug-2006.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ ((𝐹 ∈ 𝐶 ∧ 𝐹:𝐴⟶𝐵) → 𝐴 ∈ V)
Theorem	f0 5444	The empty function. (Contributed by NM, 14-Aug-1999.)
⊢ ∅:∅⟶𝐴
Theorem	f00 5445	A class is a function with empty codomain iff it and its domain are empty. (Contributed by NM, 10-Dec-2003.)
⊢ (𝐹:𝐴⟶∅ ↔ (𝐹 = ∅ ∧ 𝐴 = ∅))
Theorem	f0bi 5446	A function with empty domain is empty. (Contributed by Alexander van der Vekens, 30-Jun-2018.)
⊢ (𝐹:∅⟶𝑋 ↔ 𝐹 = ∅)
Theorem	f0dom0 5447	A function is empty iff it has an empty domain. (Contributed by AV, 10-Feb-2019.)
⊢ (𝐹:𝑋⟶𝑌 → (𝑋 = ∅ ↔ 𝐹 = ∅))
Theorem	f0rn0 5448*	If there is no element in the range of a function, its domain must be empty. (Contributed by Alexander van der Vekens, 12-Jul-2018.)
⊢ ((𝐸:𝑋⟶𝑌 ∧ ¬ ∃𝑦 ∈ 𝑌 𝑦 ∈ ran 𝐸) → 𝑋 = ∅)
Theorem	fconst 5449	A cross product with a singleton is a constant function. (Contributed by NM, 14-Aug-1999.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 × {𝐵}):𝐴⟶{𝐵}
Theorem	fconstg 5450	A cross product with a singleton is a constant function. (Contributed by NM, 19-Oct-2004.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 × {𝐵}):𝐴⟶{𝐵})
Theorem	fnconstg 5451	A cross product with a singleton is a constant function. (Contributed by NM, 24-Jul-2014.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 × {𝐵}) Fn 𝐴)
Theorem	fconst6g 5452	Constant function with loose range. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ (𝐵 ∈ 𝐶 → (𝐴 × {𝐵}):𝐴⟶𝐶)
Theorem	fconst6 5453	A constant function as a mapping. (Contributed by Jeff Madsen, 30-Nov-2009.) (Revised by Mario Carneiro, 22-Apr-2015.)
⊢ 𝐵 ∈ 𝐶    ⇒   ⊢ (𝐴 × {𝐵}):𝐴⟶𝐶
Theorem	f1eq1 5454	Equality theorem for one-to-one functions. (Contributed by NM, 10-Feb-1997.)
⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))
Theorem	f1eq2 5455	Equality theorem for one-to-one functions. (Contributed by NM, 10-Feb-1997.)
⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐹:𝐵–1-1→𝐶))
Theorem	f1eq3 5456	Equality theorem for one-to-one functions. (Contributed by NM, 10-Feb-1997.)
⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1→𝐴 ↔ 𝐹:𝐶–1-1→𝐵))
Theorem	nff1 5457	Bound-variable hypothesis builder for a one-to-one function. (Contributed by NM, 16-May-2004.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐹:𝐴–1-1→𝐵
Theorem	dff12 5458*	Alternate definition of a one-to-one function. (Contributed by NM, 31-Dec-1996.)
⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦∃*𝑥 𝑥𝐹𝑦))
Theorem	f1f 5459	A one-to-one mapping is a mapping. (Contributed by NM, 31-Dec-1996.)
⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
Theorem	f1rn 5460	The range of a one-to-one mapping. (Contributed by BJ, 6-Jul-2022.)
⊢ (𝐹:𝐴–1-1→𝐵 → ran 𝐹 ⊆ 𝐵)
Theorem	f1fn 5461	A one-to-one mapping is a function on its domain. (Contributed by NM, 8-Mar-2014.)
⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
Theorem	f1fun 5462	A one-to-one mapping is a function. (Contributed by NM, 8-Mar-2014.)
⊢ (𝐹:𝐴–1-1→𝐵 → Fun 𝐹)
Theorem	f1rel 5463	A one-to-one onto mapping is a relation. (Contributed by NM, 8-Mar-2014.)
⊢ (𝐹:𝐴–1-1→𝐵 → Rel 𝐹)
Theorem	f1dm 5464	The domain of a one-to-one mapping. (Contributed by NM, 8-Mar-2014.)
⊢ (𝐹:𝐴–1-1→𝐵 → dom 𝐹 = 𝐴)
Theorem	f1ss 5465	A function that is one-to-one is also one-to-one on some superset of its range. (Contributed by Mario Carneiro, 12-Jan-2013.)
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴–1-1→𝐶)
Theorem	f1ssr 5466	Combine a one-to-one function with a restriction on the domain. (Contributed by Stefan O'Rear, 20-Feb-2015.)
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 ⊆ 𝐶) → 𝐹:𝐴–1-1→𝐶)
Theorem	f1ff1 5467	If a function is one-to-one from 𝐴 to 𝐵 and is also a function from 𝐴 to 𝐶, then it is a one-to-one function from 𝐴 to 𝐶. (Contributed by BJ, 4-Jul-2022.)
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴⟶𝐶) → 𝐹:𝐴–1-1→𝐶)
Theorem	f1ssres 5468	A function that is one-to-one is also one-to-one on any subclass of its domain. (Contributed by Mario Carneiro, 17-Jan-2015.)
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶–1-1→𝐵)
Theorem	f1resf1 5469	The restriction of an injective function is injective. (Contributed by AV, 28-Jun-2022.)
⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴) ∧ (𝐹 ↾ 𝐶):𝐶⟶𝐷) → (𝐹 ↾ 𝐶):𝐶–1-1→𝐷)
Theorem	f1cnvcnv 5470	Two ways to express that a set 𝐴 (not necessarily a function) is one-to-one. Each side is equivalent to Definition 6.4(3) of [TakeutiZaring] p. 24, who use the notation "Un2 (A)" for one-to-one. We do not introduce a separate notation since we rarely use it. (Contributed by NM, 13-Aug-2004.)
⊢ (◡◡𝐴:dom 𝐴–1-1→V ↔ (Fun ◡𝐴 ∧ Fun ◡◡𝐴))
Theorem	f1co 5471	Composition of one-to-one functions. Exercise 30 of [TakeutiZaring] p. 25. (Contributed by NM, 28-May-1998.)
⊢ ((𝐹:𝐵–1-1→𝐶 ∧ 𝐺:𝐴–1-1→𝐵) → (𝐹 ∘ 𝐺):𝐴–1-1→𝐶)
Theorem	foeq1 5472	Equality theorem for onto functions. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐹 = 𝐺 → (𝐹:𝐴–onto→𝐵 ↔ 𝐺:𝐴–onto→𝐵))
Theorem	foeq2 5473	Equality theorem for onto functions. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐴 = 𝐵 → (𝐹:𝐴–onto→𝐶 ↔ 𝐹:𝐵–onto→𝐶))
Theorem	foeq3 5474	Equality theorem for onto functions. (Contributed by NM, 1-Aug-1994.)
⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵))
Theorem	nffo 5475	Bound-variable hypothesis builder for an onto function. (Contributed by NM, 16-May-2004.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐹:𝐴–onto→𝐵
Theorem	fof 5476	An onto mapping is a mapping. (Contributed by NM, 3-Aug-1994.)
⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)
Theorem	fofun 5477	An onto mapping is a function. (Contributed by NM, 29-Mar-2008.)
⊢ (𝐹:𝐴–onto→𝐵 → Fun 𝐹)
Theorem	fofn 5478	An onto mapping is a function on its domain. (Contributed by NM, 16-Dec-2008.)
⊢ (𝐹:𝐴–onto→𝐵 → 𝐹 Fn 𝐴)
Theorem	forn 5479	The codomain of an onto function is its range. (Contributed by NM, 3-Aug-1994.)
⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵)
Theorem	dffo2 5480	Alternate definition of an onto function. (Contributed by NM, 22-Mar-2006.)
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵))
Theorem	foima 5481	The image of the domain of an onto function. (Contributed by NM, 29-Nov-2002.)
⊢ (𝐹:𝐴–onto→𝐵 → (𝐹 “ 𝐴) = 𝐵)
Theorem	dffn4 5482	A function maps onto its range. (Contributed by NM, 10-May-1998.)
⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴–onto→ran 𝐹)
Theorem	funforn 5483	A function maps its domain onto its range. (Contributed by NM, 23-Jul-2004.)
⊢ (Fun 𝐴 ↔ 𝐴:dom 𝐴–onto→ran 𝐴)
Theorem	fodmrnu 5484	An onto function has unique domain and range. (Contributed by NM, 5-Nov-2006.)
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐹:𝐶–onto→𝐷) → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	fimadmfo 5485	A function is a function onto the image of its domain. (Contributed by AV, 1-Dec-2022.)
⊢ (𝐹:𝐴⟶𝐵 → 𝐹:𝐴–onto→(𝐹 “ 𝐴))
Theorem	fores 5486	Restriction of a function. (Contributed by NM, 4-Mar-1997.)
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐹 ↾ 𝐴):𝐴–onto→(𝐹 “ 𝐴))
Theorem	foco 5487	Composition of onto functions. (Contributed by NM, 22-Mar-2006.)
⊢ ((𝐹:𝐵–onto→𝐶 ∧ 𝐺:𝐴–onto→𝐵) → (𝐹 ∘ 𝐺):𝐴–onto→𝐶)
Theorem	f1oeq1 5488	Equality theorem for one-to-one onto functions. (Contributed by NM, 10-Feb-1997.)
⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1-onto→𝐵 ↔ 𝐺:𝐴–1-1-onto→𝐵))
Theorem	f1oeq2 5489	Equality theorem for one-to-one onto functions. (Contributed by NM, 10-Feb-1997.)
⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐶))
Theorem	f1oeq3 5490	Equality theorem for one-to-one onto functions. (Contributed by NM, 10-Feb-1997.)
⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵))
Theorem	f1oeq23 5491	Equality theorem for one-to-one onto functions. (Contributed by FL, 14-Jul-2012.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐷))
Theorem	f1eq123d 5492	Equality deduction for one-to-one functions. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐺:𝐵–1-1→𝐷))
Theorem	foeq123d 5493	Equality deduction for onto functions. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐹:𝐴–onto→𝐶 ↔ 𝐺:𝐵–onto→𝐷))
Theorem	f1oeq123d 5494	Equality deduction for one-to-one onto functions. (Contributed by Mario Carneiro, 27-Jan-2017.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐷))
Theorem	f1oeq1d 5495	Equality deduction for one-to-one onto functions. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐹 = 𝐺)    ⇒   ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐵 ↔ 𝐺:𝐴–1-1-onto→𝐵))
Theorem	f1oeq2d 5496	Equality deduction for one-to-one onto functions. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐶))
Theorem	f1oeq3d 5497	Equality deduction for one-to-one onto functions. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵))
Theorem	nff1o 5498	Bound-variable hypothesis builder for a one-to-one onto function. (Contributed by NM, 16-May-2004.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐹:𝐴–1-1-onto→𝐵
Theorem	f1of1 5499	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 5500	A one-to-one onto mapping is a mapping. (Contributed by NM, 12-Dec-2003.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵)