P. 79 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 7801-7900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	tfindsg 7801*	Transfinite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last three are the basis, the induction step for successors, and the induction step for limit ordinals. The basis of this version is an arbitrary ordinal 𝐵 instead of zero. Remark in [TakeutiZaring] p. 57. (Contributed by NM, 5-Mar-2004.)
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ (𝐵 ∈ On → 𝜓)    &   ⊢ (((𝑦 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 ⊆ 𝑦) → (𝜒 → 𝜃))    &   ⊢ (((Lim 𝑥 ∧ 𝐵 ∈ On) ∧ 𝐵 ⊆ 𝑥) → (∀𝑦 ∈ 𝑥 (𝐵 ⊆ 𝑦 → 𝜒) → 𝜑))    ⇒   ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 ⊆ 𝐴) → 𝜏)
Theorem	tfindsg2 7802*	Transfinite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last three are the basis, the induction step for successors, and the induction step for limit ordinals. The basis of this version is an arbitrary ordinal suc 𝐵 instead of zero. (Contributed by NM, 5-Jan-2005.) Remove unnecessary distinct variable conditions. (Revised by David Abernethy, 19-Jun-2012.)
⊢ (𝑥 = suc 𝐵 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ (𝐵 ∈ On → 𝜓)    &   ⊢ ((𝑦 ∈ On ∧ 𝐵 ∈ 𝑦) → (𝜒 → 𝜃))    &   ⊢ ((Lim 𝑥 ∧ 𝐵 ∈ 𝑥) → (∀𝑦 ∈ 𝑥 (𝐵 ∈ 𝑦 → 𝜒) → 𝜑))    ⇒   ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → 𝜏)
Theorem	tfindes 7803*	Transfinite Induction with explicit substitution. The first hypothesis is the basis, the second is the induction step for successors, and the third is the induction step for limit ordinals. Theorem Schema 4 of [Suppes] p. 197. (Contributed by NM, 5-Mar-2004.)
⊢ [∅ / 𝑥]𝜑    &   ⊢ (𝑥 ∈ On → (𝜑 → [suc 𝑥 / 𝑥]𝜑))    &   ⊢ (Lim 𝑦 → (∀𝑥 ∈ 𝑦 𝜑 → [𝑦 / 𝑥]𝜑))    ⇒   ⊢ (𝑥 ∈ On → 𝜑)
Theorem	tfinds2 7804*	Transfinite Induction (inference schema), using implicit substitutions. The first three hypotheses establish the substitutions we need. The last three are the basis and the induction hypotheses (for successor and limit ordinals respectively). Theorem Schema 4 of [Suppes] p. 197. The wff 𝜏 is an auxiliary antecedent to help shorten proofs using this theorem. (Contributed by NM, 4-Sep-2004.)
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃))    &   ⊢ (𝜏 → 𝜓)    &   ⊢ (𝑦 ∈ On → (𝜏 → (𝜒 → 𝜃)))    &   ⊢ (Lim 𝑥 → (𝜏 → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑)))    ⇒   ⊢ (𝑥 ∈ On → (𝜏 → 𝜑))
Theorem	tfinds3 7805*	Principle of Transfinite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last three are the basis, the induction step for successors, and the induction step for limit ordinals. (Contributed by NM, 6-Jan-2005.) (Revised by David Abernethy, 21-Jun-2011.)
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ (𝜂 → 𝜓)    &   ⊢ (𝑦 ∈ On → (𝜂 → (𝜒 → 𝜃)))    &   ⊢ (Lim 𝑥 → (𝜂 → (∀𝑦 ∈ 𝑥 𝜒 → 𝜑)))    ⇒   ⊢ (𝐴 ∈ On → (𝜂 → 𝜏))
2.4.4  The natural numbers (i.e., finite ordinals)
Syntax	com 7806	Extend class notation to include the class of natural numbers.
class ω
Definition	df-om 7807*	Define the class of natural numbers, which are all ordinal numbers that are less than every limit ordinal, i.e., all finite ordinals. Our definition is a variant of the Definition of N of [BellMachover] p. 471. See dfom2 7808 for an alternate definition. Later, when we assume the Axiom of Infinity, we show ω is a set in omex 9558, and ω can then be defined per dfom3 9562 (the smallest inductive set) and dfom4 9564. Note: the natural numbers ω are a subset of the ordinal numbers df-on 6315. Later, when we define complex numbers, we will be able to also define a subset of the complex numbers (df-nn 12147) with analogous properties and operations, but they will be different sets. (Contributed by NM, 15-May-1994.)
⊢ ω = {𝑥 ∈ On ∣ ∀𝑦(Lim 𝑦 → 𝑥 ∈ 𝑦)}
Theorem	dfom2 7808	An alternate definition of the set of natural numbers ω. Definition 7.28 of [TakeutiZaring] p. 42, who use the symbol KI for the restricted class abstraction of non-limit ordinal numbers (see nlimon 7791). (Contributed by NM, 1-Nov-2004.)
⊢ ω = {𝑥 ∈ On ∣ suc 𝑥 ⊆ {𝑦 ∈ On ∣ ¬ Lim 𝑦}}
Theorem	elom 7809*	Membership in omega. The left conjunct can be eliminated if we assume the Axiom of Infinity; see elom3 9563. (Contributed by NM, 15-May-1994.)
⊢ (𝐴 ∈ ω ↔ (𝐴 ∈ On ∧ ∀𝑥(Lim 𝑥 → 𝐴 ∈ 𝑥)))
Theorem	omsson 7810	Omega is a subset of On. (Contributed by NM, 13-Jun-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ω ⊆ On
Theorem	limomss 7811	The class of natural numbers is a subclass of any (infinite) limit ordinal. Exercise 1 of [TakeutiZaring] p. 44. Remarkably, our proof does not require the Axiom of Infinity. (Contributed by NM, 30-Oct-2003.)
⊢ (Lim 𝐴 → ω ⊆ 𝐴)
Theorem	nnon 7812	A natural number is an ordinal number. (Contributed by NM, 27-Jun-1994.)
⊢ (𝐴 ∈ ω → 𝐴 ∈ On)
Theorem	nnoni 7813	A natural number is an ordinal number. (Contributed by NM, 27-Jun-1994.)
⊢ 𝐴 ∈ ω    ⇒   ⊢ 𝐴 ∈ On
Theorem	nnord 7814	A natural number is ordinal. (Contributed by NM, 17-Oct-1995.)
⊢ (𝐴 ∈ ω → Ord 𝐴)
Theorem	trom 7815	The class of finite ordinals ω is a transitive class. (Contributed by NM, 18-Oct-1995.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ Tr ω
Theorem	ordom 7816	The class of finite ordinals ω is ordinal. Theorem 7.32 of [TakeutiZaring] p. 43. Theorem 1.22 of [Schloeder] p. 3. (Contributed by NM, 18-Oct-1995.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ Ord ω
Theorem	elnn 7817	A member of a natural number is a natural number. (Contributed by NM, 21-Jun-1998.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ ω) → 𝐴 ∈ ω)
Theorem	omon 7818	The class of natural numbers ω is either an ordinal number (if we accept the Axiom of Infinity) or the proper class of all ordinal numbers (if we deny the Axiom of Infinity). Remark in [TakeutiZaring] p. 43. (Contributed by NM, 10-May-1998.)
⊢ (ω ∈ On ∨ ω = On)
Theorem	omelon2 7819	Omega is an ordinal number. (Contributed by Mario Carneiro, 30-Jan-2013.)
⊢ (ω ∈ V → ω ∈ On)
Theorem	nnlim 7820	A natural number is not a limit ordinal. (Contributed by NM, 18-Oct-1995.)
⊢ (𝐴 ∈ ω → ¬ Lim 𝐴)
Theorem	omssnlim 7821	The class of natural numbers is a subclass of the class of non-limit ordinal numbers. Exercise 4 of [TakeutiZaring] p. 42. (Contributed by NM, 2-Nov-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ω ⊆ {𝑥 ∈ On ∣ ¬ Lim 𝑥}
Theorem	limom 7822	Omega is a limit ordinal. Theorem 2.8 of [BellMachover] p. 473. Theorem 1.23 of [Schloeder] p. 4. Our proof, however, does not require the Axiom of Infinity. (Contributed by NM, 26-Mar-1995.) (Proof shortened by Mario Carneiro, 2-Sep-2015.)
⊢ Lim ω
Theorem	peano2b 7823	A class belongs to omega iff its successor does. (Contributed by NM, 3-Dec-1995.)
⊢ (𝐴 ∈ ω ↔ suc 𝐴 ∈ ω)
Theorem	nnsuc 7824*	A nonzero natural number is a successor. (Contributed by NM, 18-Feb-2004.)
⊢ ((𝐴 ∈ ω ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ ω 𝐴 = suc 𝑥)
Theorem	omsucne 7825	A natural number is not the successor of itself. (Contributed by AV, 17-Oct-2023.)
⊢ (𝐴 ∈ ω → 𝐴 ≠ suc 𝐴)
Theorem	ssnlim 7826*	An ordinal subclass of non-limit ordinals is a class of natural numbers. Exercise 7 of [TakeutiZaring] p. 42. (Contributed by NM, 2-Nov-2004.)
⊢ ((Ord 𝐴 ∧ 𝐴 ⊆ {𝑥 ∈ On ∣ ¬ Lim 𝑥}) → 𝐴 ⊆ ω)
Theorem	omsinds 7827*	Strong (or "total") induction principle over the finite ordinals. (Contributed by Scott Fenton, 17-Jul-2015.) (Proof shortened by BJ, 16-Oct-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 ∈ ω → (∀𝑦 ∈ 𝑥 𝜓 → 𝜑))    ⇒   ⊢ (𝐴 ∈ ω → 𝜒)
Theorem	omun 7828	The union of two finite ordinals is a finite ordinal. (Contributed by Scott Fenton, 15-Mar-2025.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∪ 𝐵) ∈ ω)
2.4.5  Peano's postulates
Theorem	peano1 7829	Zero is a natural number. One of Peano's five postulates for arithmetic. Proposition 7.30(1) of [TakeutiZaring] p. 42. Note: Unlike most textbooks, our proofs of peano1 7829 through peano5 7833 do not use the Axiom of Infinity. Unlike Takeuti and Zaring, they also do not use the Axiom of Regularity. (Contributed by NM, 15-May-1994.) Avoid ax-un 7675. (Revised by BTernaryTau, 29-Nov-2024.)
⊢ ∅ ∈ ω
Theorem	peano2 7830	The successor of any natural number is a natural number. One of Peano's five postulates for arithmetic. Proposition 7.30(2) of [TakeutiZaring] p. 42. (Contributed by NM, 3-Sep-2003.)
⊢ (𝐴 ∈ ω → suc 𝐴 ∈ ω)
Theorem	peano3 7831	The successor of any natural number is not zero. One of Peano's five postulates for arithmetic. Proposition 7.30(3) of [TakeutiZaring] p. 42. (Contributed by NM, 3-Sep-2003.)
⊢ (𝐴 ∈ ω → suc 𝐴 ≠ ∅)
Theorem	peano4 7832	Two natural numbers are equal iff their successors are equal, i.e. the successor function is one-to-one. One of Peano's five postulates for arithmetic. Proposition 7.30(4) of [TakeutiZaring] p. 43. (Contributed by NM, 3-Sep-2003.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (suc 𝐴 = suc 𝐵 ↔ 𝐴 = 𝐵))
Theorem	peano5 7833*	The induction postulate: any class containing zero and closed under the successor operation contains all natural numbers. One of Peano's five postulates for arithmetic. Proposition 7.30(5) of [TakeutiZaring] p. 43, except our proof does not require the Axiom of Infinity. The more traditional statement of mathematical induction as a theorem schema, with a basis and an induction step, is derived from this theorem as Theorem findes 7840. (Contributed by NM, 18-Feb-2004.) Avoid ax-10 2142, ax-12 2178. (Revised by GG, 3-Oct-2024.)
⊢ ((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) → ω ⊆ 𝐴)
Theorem	nn0suc 7834*	A natural number is either 0 or a successor. (Contributed by NM, 27-May-1998.)
⊢ (𝐴 ∈ ω → (𝐴 = ∅ ∨ ∃𝑥 ∈ ω 𝐴 = suc 𝑥))
2.4.6  Finite induction (for finite ordinals)
Theorem	find 7835*	The Principle of Finite Induction (mathematical induction). Corollary 7.31 of [TakeutiZaring] p. 43. The simpler hypothesis shown here was suggested in an email from "Colin" on 1-Oct-2001. The hypothesis states that 𝐴 is a set of natural numbers, zero belongs to 𝐴, and given any member of 𝐴 the member's successor also belongs to 𝐴. The conclusion is that every natural number is in 𝐴. (Contributed by NM, 22-Feb-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Proof shortened by Wolf Lammen, 28-May-2024.)
⊢ (𝐴 ⊆ ω ∧ ∅ ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴)    ⇒   ⊢ 𝐴 = ω
Theorem	finds 7836*	Principle of Finite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last two are the basis and the induction step. Theorem Schema 22 of [Suppes] p. 136. This is Metamath 100 proof #74. (Contributed by NM, 14-Apr-1995.)
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ 𝜓    &   ⊢ (𝑦 ∈ ω → (𝜒 → 𝜃))    ⇒   ⊢ (𝐴 ∈ ω → 𝜏)
Theorem	findsg 7837*	Principle of Finite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last two are the basis and the induction step. The basis of this version is an arbitrary natural number 𝐵 instead of zero. (Contributed by NM, 16-Sep-1995.)
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ (𝐵 ∈ ω → 𝜓)    &   ⊢ (((𝑦 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐵 ⊆ 𝑦) → (𝜒 → 𝜃))    ⇒   ⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐵 ⊆ 𝐴) → 𝜏)
Theorem	finds2 7838*	Principle of Finite Induction (inference schema), using implicit substitutions. The first three hypotheses establish the substitutions we need. The last two are the basis and the induction step. Theorem Schema 22 of [Suppes] p. 136. (Contributed by NM, 29-Nov-2002.)
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃))    &   ⊢ (𝜏 → 𝜓)    &   ⊢ (𝑦 ∈ ω → (𝜏 → (𝜒 → 𝜃)))    ⇒   ⊢ (𝑥 ∈ ω → (𝜏 → 𝜑))
Theorem	finds1 7839*	Principle of Finite Induction (inference schema), using implicit substitutions. The first three hypotheses establish the substitutions we need. The last two are the basis and the induction step. Theorem Schema 22 of [Suppes] p. 136. (Contributed by NM, 22-Mar-2006.)
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃))    &   ⊢ 𝜓    &   ⊢ (𝑦 ∈ ω → (𝜒 → 𝜃))    ⇒   ⊢ (𝑥 ∈ ω → 𝜑)
Theorem	findes 7840	Finite induction with explicit substitution. The first hypothesis is the basis and the second is the induction step. Theorem Schema 22 of [Suppes] p. 136. See tfindes 7803 for the transfinite version. This is an alternative for Metamath 100 proof #74. (Contributed by Raph Levien, 9-Jul-2003.)
⊢ [∅ / 𝑥]𝜑    &   ⊢ (𝑥 ∈ ω → (𝜑 → [suc 𝑥 / 𝑥]𝜑))    ⇒   ⊢ (𝑥 ∈ ω → 𝜑)
2.4.7  Relations and functions (cont.)
Theorem	dmexg 7841	The domain of a set is a set. Corollary 6.8(2) of [TakeutiZaring] p. 26. (Contributed by NM, 7-Apr-1995.)
⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)
Theorem	rnexg 7842	The range of a set is a set. Corollary 6.8(3) of [TakeutiZaring] p. 26. Similar to Lemma 3D of [Enderton] p. 41. (Contributed by NM, 31-Mar-1995.)
⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
Theorem	dmexd 7843	The domain of a set is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → dom 𝐴 ∈ V)
Theorem	fndmexd 7844	If a function is a set, its domain is a set. (Contributed by Rohan Ridenour, 13-May-2024.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 Fn 𝐷)    ⇒   ⊢ (𝜑 → 𝐷 ∈ V)
Theorem	dmfex 7845	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	fndmexb 7846	The domain of a function is a set iff the function is a set. (Contributed by AV, 8-Aug-2024.)
⊢ (𝐹 Fn 𝐴 → (𝐴 ∈ V ↔ 𝐹 ∈ V))
Theorem	fdmexb 7847	The domain of a function is a set iff the function is a set. (Contributed by AV, 8-Aug-2024.)
⊢ (𝐹:𝐴⟶𝐵 → (𝐴 ∈ V ↔ 𝐹 ∈ V))
Theorem	dmfexALT 7848	Alternate proof of dmfex 7845: shorter but using ax-rep 5221. (Contributed by NM, 27-Aug-2006.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) (Proof shortened by AV, 23-Aug-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐹 ∈ 𝐶 ∧ 𝐹:𝐴⟶𝐵) → 𝐴 ∈ V)
Theorem	dmex 7849	The domain of a set is a set. Corollary 6.8(2) of [TakeutiZaring] p. 26. (Contributed by NM, 7-Jul-2008.)
⊢ 𝐴 ∈ V    ⇒   ⊢ dom 𝐴 ∈ V
Theorem	rnex 7850	The range of a set is a set. Corollary 6.8(3) of [TakeutiZaring] p. 26. Similar to Lemma 3D of [Enderton] p. 41. (Contributed by NM, 7-Jul-2008.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ran 𝐴 ∈ V
Theorem	iprc 7851	The identity function is a proper class. This means, for example, that we cannot use it as a member of the class of continuous functions unless it is restricted to a set, as in idcn 23160. (Contributed by NM, 1-Jan-2007.)
⊢ ¬ I ∈ V
Theorem	resiexg 7852	The existence of a restricted identity function, proved without using the Axiom of Replacement (unlike resfunexg 7155). (Contributed by NM, 13-Jan-2007.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) ∈ V)
Theorem	imaexg 7853	The image of a set is a set. Theorem 3.17 of [Monk1] p. 39. (Contributed by NM, 24-Jul-1995.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 “ 𝐵) ∈ V)
Theorem	imaex 7854	The image of a set is a set. Theorem 3.17 of [Monk1] p. 39. (Contributed by JJ, 24-Sep-2021.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 “ 𝐵) ∈ V
Theorem	rnexd 7855	The range of a set is a set. Deduction version of rnexd 7855. (Contributed by Thierry Arnoux, 14-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ran 𝐴 ∈ V)
Theorem	imaexd 7856	The image of a set is a set. Deduction version of imaexg 7853. (Contributed by Thierry Arnoux, 14-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐴 “ 𝐵) ∈ V)
Theorem	exse2 7857	Any set relation is set-like. (Contributed by Mario Carneiro, 22-Jun-2015.)
⊢ (𝑅 ∈ 𝑉 → 𝑅 Se 𝐴)
Theorem	xpexr 7858	If a Cartesian product is a set, one of its components must be a set. (Contributed by NM, 27-Aug-2006.)
⊢ ((𝐴 × 𝐵) ∈ 𝐶 → (𝐴 ∈ V ∨ 𝐵 ∈ V))
Theorem	xpexr2 7859	If a nonempty Cartesian product is a set, so are both of its components. (Contributed by NM, 27-Aug-2006.)
⊢ (((𝐴 × 𝐵) ∈ 𝐶 ∧ (𝐴 × 𝐵) ≠ ∅) → (𝐴 ∈ V ∧ 𝐵 ∈ V))
Theorem	xpexcnv 7860	A condition where the converse of xpex 7693 holds as well. Corollary 6.9(2) in [TakeutiZaring] p. 26. (Contributed by Andrew Salmon, 13-Nov-2011.)
⊢ ((𝐵 ≠ ∅ ∧ (𝐴 × 𝐵) ∈ V) → 𝐴 ∈ V)
Theorem	soex 7861	If the relation in a strict order is a set, then the base field is also a set. (Contributed by Mario Carneiro, 27-Apr-2015.)
⊢ ((𝑅 Or 𝐴 ∧ 𝑅 ∈ 𝑉) → 𝐴 ∈ V)
Theorem	elxp4 7862	Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp5 7863, elxp6 7965, and elxp7 7966. (Contributed by NM, 17-Feb-2004.)
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩ ∧ (∪ dom {𝐴} ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))
Theorem	elxp5 7863	Membership in a Cartesian product requiring no quantifiers or dummy variables. Provides a slightly shorter version of elxp4 7862 when the double intersection does not create class existence problems (caused by int0 4915). (Contributed by NM, 1-Aug-2004.)
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨∩ ∩ 𝐴, ∪ ran {𝐴}⟩ ∧ (∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))
Theorem	cnvexg 7864	The converse of a set is a set. Corollary 6.8(1) of [TakeutiZaring] p. 26. (Contributed by NM, 17-Mar-1998.)
⊢ (𝐴 ∈ 𝑉 → ◡𝐴 ∈ V)
Theorem	cnvex 7865	The converse of a set is a set. Corollary 6.8(1) of [TakeutiZaring] p. 26. (Contributed by NM, 19-Dec-2003.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ◡𝐴 ∈ V
Theorem	relcnvexb 7866	A relation is a set iff its converse is a set. (Contributed by FL, 3-Mar-2007.)
⊢ (Rel 𝑅 → (𝑅 ∈ V ↔ ◡𝑅 ∈ V))
Theorem	f1oexrnex 7867	If the range of a 1-1 onto function is a set, the function itself is a set. (Contributed by AV, 2-Jun-2019.)
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐹 ∈ V)
Theorem	f1oexbi 7868*	There is a one-to-one onto function from a set to a second set iff there is a one-to-one onto function from the second set to the first set. (Contributed by Alexander van der Vekens, 30-Sep-2018.)
⊢ (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 ↔ ∃𝑔 𝑔:𝐵–1-1-onto→𝐴)
Theorem	coexg 7869	The composition of two sets is a set. (Contributed by NM, 19-Mar-1998.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∘ 𝐵) ∈ V)
Theorem	coex 7870	The composition of two sets is a set. (Contributed by NM, 15-Dec-2003.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∘ 𝐵) ∈ V
Theorem	coexd 7871	The composition of two sets is a set. (Contributed by SN, 7-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐴 ∘ 𝐵) ∈ V)
Theorem	funcnvuni 7872*	The union of a chain (with respect to inclusion) of single-rooted sets is single-rooted. (See funcnv 6555 for "single-rooted" definition.) (Contributed by NM, 11-Aug-2004.)
⊢ (∀𝑓 ∈ 𝐴 (Fun ◡𝑓 ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → Fun ◡∪ 𝐴)
Theorem	fun11uni 7873*	The union of a chain (with respect to inclusion) of one-to-one functions is a one-to-one function. (Contributed by NM, 11-Aug-2004.)
⊢ (∀𝑓 ∈ 𝐴 ((Fun 𝑓 ∧ Fun ◡𝑓) ∧ ∀𝑔 ∈ 𝐴 (𝑓 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑓)) → (Fun ∪ 𝐴 ∧ Fun ◡∪ 𝐴))
Theorem	resf1extb 7874	Extension of an injection which is a restriction of a function. (Contributed by AV, 3-Oct-2025.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑋 ∈ (𝐴 ∖ 𝐶) ∧ 𝐶 ⊆ 𝐴) → (((𝐹 ↾ 𝐶):𝐶–1-1→𝐵 ∧ (𝐹‘𝑋) ∉ (𝐹 “ 𝐶)) ↔ (𝐹 ↾ (𝐶 ∪ {𝑋})):(𝐶 ∪ {𝑋})–1-1→𝐵))
Theorem	resf1ext2b 7875	Extension of an injection which is a restriction of a function. (Contributed by AV, 3-Oct-2025.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑋 ∈ (𝐴 ∖ 𝐶) ∧ 𝐶 ⊆ 𝐴) → ((Fun ◡(𝐹 ↾ 𝐶) ∧ (𝐹‘𝑋) ∉ (𝐹 “ 𝐶)) ↔ Fun ◡(𝐹 ↾ (𝐶 ∪ {𝑋}))))
Theorem	fex2 7876	A function with bounded domain and codomain is a set. This version of fex 7166 is proven without the Axiom of Replacement ax-rep 5221, but depends on ax-un 7675, which is not required for the proof of fex 7166. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ∈ V)
Theorem	fabexd 7877*	Existence of a set of functions. In contrast to fabex 7880 or fabexg 7878, the condition in the class abstraction does not contain the function explicitly, but the function can be derived from it. Therefore, this theorem is also applicable for more special functions like one-to-one, onto or one-to-one onto functions. (Contributed by AV, 20-May-2025.)
⊢ ((𝜑 ∧ 𝜓) → 𝑓:𝑋⟶𝑌)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑊)    ⇒   ⊢ (𝜑 → {𝑓 ∣ 𝜓} ∈ V)
Theorem	fabexg 7878*	Existence of a set of functions. (Contributed by Paul Chapman, 25-Feb-2008.) (Proof shortened by AV, 9-Jun-2025.)
⊢ 𝐹 = {𝑥 ∣ (𝑥:𝐴⟶𝐵 ∧ 𝜑)}    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝐹 ∈ V)
Theorem	fabexgOLD 7879*	Obsolete version of fabexg 7878 as of 9-Jun-2025. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐹 = {𝑥 ∣ (𝑥:𝐴⟶𝐵 ∧ 𝜑)}    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝐹 ∈ V)
Theorem	fabex 7880*	Existence of a set of functions. (Contributed by NM, 3-Dec-2007.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐹 = {𝑥 ∣ (𝑥:𝐴⟶𝐵 ∧ 𝜑)}    ⇒   ⊢ 𝐹 ∈ V
Theorem	mapex 7881*	The class of all functions mapping one set to another is a set. Remark after Definition 10.24 of [Kunen] p. 31. (Contributed by Raph Levien, 4-Dec-2003.) (Proof shortened by AV, 16-Jun-2025.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → {𝑓 ∣ 𝑓:𝐴⟶𝐵} ∈ V)
Theorem	f1oabexg 7882*	The class of all 1-1-onto functions mapping one set to another is a set. (Contributed by Paul Chapman, 25-Feb-2008.) (Proof shortened by AV, 9-Jun-2025.)
⊢ 𝐹 = {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐵 ∧ 𝜑)}    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝐹 ∈ V)
Theorem	f1oabexgOLD 7883*	Obsolete version of f1oabexg 7882 as of 9-Jun-2025. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐹 = {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐵 ∧ 𝜑)}    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝐹 ∈ V)
Theorem	fiunlem 7884*	Lemma for fiun 7885 and f1iun 7886. Formerly part of f1iun 7886. (Contributed by AV, 6-Oct-2023.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ (((𝐵:𝐷⟶𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) → ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))
Theorem	fiun 7885*	The union of a chain (with respect to inclusion) of functions is a function. Analogous to f1iun 7886. (Contributed by AV, 6-Oct-2023.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷⟶𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷⟶𝑆)
Theorem	f1iun 7886*	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.) (Proof shortened by AV, 5-Nov-2023.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (∀𝑥 ∈ 𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷–1-1→𝑆)
Theorem	fviunfun 7887*	The function value of an indexed union is the value of one of the indexed functions. (Contributed by AV, 4-Nov-2023.)
⊢ 𝑈 = ∪ 𝑖 ∈ 𝐼 (𝐹‘𝑖)    ⇒   ⊢ ((Fun 𝑈 ∧ 𝐽 ∈ 𝐼 ∧ 𝑋 ∈ dom (𝐹‘𝐽)) → (𝑈‘𝑋) = ((𝐹‘𝐽)‘𝑋))
Theorem	ffoss 7888*	Relationship between a mapping and an onto mapping. Figure 38 of [Enderton] p. 145. (Contributed by NM, 10-May-1998.)
⊢ 𝐹 ∈ V    ⇒   ⊢ (𝐹:𝐴⟶𝐵 ↔ ∃𝑥(𝐹:𝐴–onto→𝑥 ∧ 𝑥 ⊆ 𝐵))
Theorem	f11o 7889*	Relationship between one-to-one and one-to-one onto function. (Contributed by NM, 4-Apr-1998.)
⊢ 𝐹 ∈ V    ⇒   ⊢ (𝐹:𝐴–1-1→𝐵 ↔ ∃𝑥(𝐹:𝐴–1-1-onto→𝑥 ∧ 𝑥 ⊆ 𝐵))
Theorem	resfunexgALT 7890	Alternate proof of resfunexg 7155, shorter but requiring ax-pow 5307 and ax-un 7675. (Contributed by NM, 7-Apr-1995.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ↾ 𝐵) ∈ V)
Theorem	cofunexg 7891	Existence of a composition when the first member is a function. (Contributed by NM, 8-Oct-2007.)
⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ∘ 𝐵) ∈ V)
Theorem	cofunex2g 7892	Existence of a composition when the second member is one-to-one. (Contributed by NM, 8-Oct-2007.)
⊢ ((𝐴 ∈ 𝑉 ∧ Fun ◡𝐵) → (𝐴 ∘ 𝐵) ∈ V)
Theorem	fnexALT 7893	Alternate proof of fnex 7157, derived using the Axiom of Replacement in the form of funimaexg 6573. This version uses ax-pow 5307 and ax-un 7675, whereas fnex 7157 does not. (Contributed by NM, 14-Aug-1994.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐵) → 𝐹 ∈ V)
Theorem	funexw 7894	Weak version of funex 7159 that holds without ax-rep 5221. If the domain and codomain of a function exist, so does the function. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ ((Fun 𝐹 ∧ dom 𝐹 ∈ 𝐵 ∧ ran 𝐹 ∈ 𝐶) → 𝐹 ∈ V)
Theorem	mptexw 7895*	Weak version of mptex 7163 that holds without ax-rep 5221. If the domain and codomain of a function given by maps-to notation are sets, the function is a set. (Contributed by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V
Theorem	funrnex 7896	If the domain of a function exists, so does its range. Part of Theorem 4.15(v) of [Monk1] p. 46. This theorem is derived using the Axiom of Replacement in the form of funex 7159. (Contributed by NM, 11-Nov-1995.)
⊢ (dom 𝐹 ∈ 𝐵 → (Fun 𝐹 → ran 𝐹 ∈ V))
Theorem	zfrep6 7897*	A version of the Axiom of Replacement. Normally 𝜑 would have free variables 𝑥 and 𝑦. Axiom 6 of [Kunen] p. 12. The Separation Scheme ax-sep 5238 cannot be derived from this version and must be stated as a separate axiom in an axiom system (such as Kunen's) that uses this version in place of our ax-rep 5221. (Contributed by NM, 10-Oct-2003.)
⊢ (∀𝑥 ∈ 𝑧 ∃!𝑦𝜑 → ∃𝑤∀𝑥 ∈ 𝑧 ∃𝑦 ∈ 𝑤 𝜑)
Theorem	focdmex 7898	If the domain of an onto function exists, so does its codomain. (Contributed by NM, 23-Jul-2004.)
⊢ (𝐴 ∈ 𝐶 → (𝐹:𝐴–onto→𝐵 → 𝐵 ∈ V))
Theorem	f1dmex 7899	If the codomain of a one-to-one function exists, so does its domain. This theorem is equivalent to the Axiom of Replacement ax-rep 5221. (Contributed by NM, 4-Sep-2004.)
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)
Theorem	f1ovv 7900	The codomain/range of a 1-1 onto function is a set iff its domain is a set. (Contributed by AV, 21-Mar-2019.)
⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))