P. 452 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 45101-45200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	iinssiin 45101	Subset implication for an indexed intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ ∩ 𝑥 ∈ 𝐴 𝐶)
Theorem	eliind2 45102*	Membership in indexed intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶)
Theorem	iinssd 45103*	Subset implication for an indexed intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝑥 = 𝑋 → 𝐵 = 𝐷)    &   ⊢ (𝜑 → 𝐷 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)
Theorem	rabbida2 45104	Equivalent wff's yield equal restricted class abstractions. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})
Theorem	iinexd 45105*	The existence of an indexed union. 𝑥 is normally a free-variable parameter in 𝐵, which should be read 𝐵(𝑥). (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶)    ⇒   ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ V)
Theorem	rabexf 45106	Separation Scheme in terms of a restricted class abstraction. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝐴    &   ⊢ 𝐴 ∈ 𝑉    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V
Theorem	rabbida3 45107	Equivalent wff's yield equal restricted class abstractions. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒)))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})
Theorem	r19.36vf 45108	Restricted quantifier version of one direction of 19.36 2230. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∃𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 → 𝜓))
Theorem	raleqd 45109	Equality deduction for restricted universal quantifier. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓))
Theorem	iinssf 45110	Subset implication for an indexed intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝐶    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)
Theorem	iinssdf 45111	Subset implication for an indexed intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝑋    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ Ⅎ𝑥𝐷    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝑥 = 𝑋 → 𝐵 = 𝐷)    &   ⊢ (𝜑 → 𝐷 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)
Theorem	resabs2i 45112	Absorption law for restriction. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ 𝐵 ⊆ 𝐶    ⇒   ⊢ ((𝐴 ↾ 𝐵) ↾ 𝐶) = (𝐴 ↾ 𝐵)
Theorem	ssdf2 45113	A sufficient condition for a subclass relationship. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
Theorem	rabssd 45114	Restricted class abstraction in a subclass relationship. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝜒) → 𝑥 ∈ 𝐵)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜒} ⊆ 𝐵)
Theorem	rexnegd 45115	Minus a real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → -𝑒𝐴 = -𝐴)
Theorem	rexlimd3 45116	* Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
Theorem	nel1nelini 45117	Membership in an intersection implies membership in the first set. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ ¬ 𝐴 ∈ 𝐵    ⇒   ⊢ ¬ 𝐴 ∈ (𝐵 ∩ 𝐶)
Theorem	nel2nelini 45118	Membership in an intersection implies membership in the second set. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ ¬ 𝐴 ∈ 𝐶    ⇒   ⊢ ¬ 𝐴 ∈ (𝐵 ∩ 𝐶)
Theorem	eliunid 45119*	Membership in indexed union. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵) → 𝐶 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	reximdd 45120	Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝜓) → 𝜒)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒)
Theorem	inopnd 45121	The intersection of two open sets of a topology is an open set. (Contributed by Glauco Siliprandi, 21-Dec-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐽)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐽)    ⇒   ⊢ (𝜑 → (𝐴 ∩ 𝐵) ∈ 𝐽)
Theorem	ss2rabdf 45122	Deduction of restricted abstraction subclass from implication. (Contributed by Glauco Siliprandi, 21-Dec-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜒})
Theorem	restopn3 45123	If 𝐴 is open, then 𝐴 is open in the restriction to itself. (Contributed by Glauco Siliprandi, 21-Dec-2024.)
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽) → 𝐴 ∈ (𝐽 ↾t 𝐴))
Theorem	restopnssd 45124	A topology restricted to an open set is a subset of the original topology. (Contributed by Glauco Siliprandi, 21-Dec-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐽)    ⇒   ⊢ (𝜑 → (𝐽 ↾t 𝐴) ⊆ 𝐽)
Theorem	restsubel 45125	A subset belongs in the space it generates via restriction. (Contributed by Glauco Siliprandi, 21-Dec-2024.)
⊢ (𝜑 → 𝐽 ∈ 𝑉)    &   ⊢ (𝜑 → ∪ 𝐽 ∈ 𝐽)    &   ⊢ (𝜑 → 𝐴 ⊆ ∪ 𝐽)    ⇒   ⊢ (𝜑 → 𝐴 ∈ (𝐽 ↾t 𝐴))
Theorem	toprestsubel 45126	A subset is open in the topology it generates via restriction. (Contributed by Glauco Siliprandi, 21-Dec-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝐴 ⊆ ∪ 𝐽)    ⇒   ⊢ (𝜑 → 𝐴 ∈ (𝐽 ↾t 𝐴))
Theorem	rabidd 45127	An "identity" law of concretion for restricted abstraction. Special case of Definition 2.1 of [Quine] p. 16. (Contributed by Glauco Siliprandi, 24-Jan-2025.)
⊢ (𝜑 → 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → 𝜒)    ⇒   ⊢ (𝜑 → 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜒})
Theorem	iunssdf 45128	Subset theorem for an indexed union. (Contributed by Glauco Siliprandi, 24-Jan-2025.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)
Theorem	iinss2d 45129	Subset implication for an indexed intersection. (Contributed by Glauco Siliprandi, 24-Jan-2025.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)
Theorem	r19.3rzf 45130	Restricted quantification of wff not containing quantified variable. (Contributed by Glauco Siliprandi, 24-Jan-2025.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 ≠ ∅ → (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑))
Theorem	r19.28zf 45131	Restricted quantifier version of Theorem 19.28 of [Margaris] p. 90. It is valid only when the domain of quantification is not empty. (Contributed by Glauco Siliprandi, 24-Jan-2025.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓)))
Theorem	iindif2f 45132	Indexed intersection of class difference. Generalization of half of theorem "De Morgan's laws". (Contributed by Glauco Siliprandi, 24-Jan-2025.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 (𝐵 ∖ 𝐶) = (𝐵 ∖ ∪ 𝑥 ∈ 𝐴 𝐶))
Theorem	ralfal 45133	Two ways of expressing empty set. (Contributed by Glauco Siliprandi, 24-Jan-2024.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 = ∅ ↔ ∀𝑥 ∈ 𝐴 ⊥)
Theorem	archd 45134*	Archimedean property of real numbers. For any real number, there is an integer greater than it. Theorem I.29 of [Apostol] p. 26. (Contributed by Glauco Siliprandi, 1-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → ∃𝑛 ∈ ℕ 𝐴 < 𝑛)
Theorem	nimnbi 45135	If an implication is false, the biconditional is false. (Contributed by Glauco Siliprandi, 15-Feb-2025.)
⊢ ¬ (𝜑 → 𝜓)    ⇒   ⊢ ¬ (𝜑 ↔ 𝜓)
Theorem	nimnbi2 45136	If an implication is false, the biconditional is false. (Contributed by Glauco Siliprandi, 15-Feb-2025.)
⊢ ¬ (𝜓 → 𝜑)    ⇒   ⊢ ¬ (𝜑 ↔ 𝜓)
Theorem	notbicom 45137	Commutative law for the negation of a biconditional. (Contributed by Glauco Siliprandi, 15-Feb-2025.)
⊢ ¬ (𝜑 ↔ 𝜓)    ⇒   ⊢ ¬ (𝜓 ↔ 𝜑)
Theorem	rexeqif 45138	Equality inference for restricted existential quantifier. (Contributed by Glauco Siliprandi, 15-Feb-2025.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ 𝐴 = 𝐵    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑)
Theorem	rspced 45139	Restricted existential specialization, using implicit substitution. (Contributed by Glauco Siliprandi, 15-Feb-2025.)
⊢ Ⅎ𝑥𝜒    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓)
21.43.2  Functions
Theorem	fnresdmss 45140	A function does not change when restricted to a set that contains its domain. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ⊆ 𝐵) → (𝐹 ↾ 𝐵) = 𝐹)
Theorem	fmptsnxp 45141*	Maps-to notation and Cartesian product for a singleton function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝑥 ∈ {𝐴} ↦ 𝐵) = ({𝐴} × {𝐵}))
Theorem	fvmpt2bd 45142*	Value of a function given by the maps-to notation. Deduction version. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐹‘𝑥) = 𝐵)
Theorem	rnmptfi 45143*	The range of a function with finite domain is finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐴 = (𝑥 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ (𝐵 ∈ Fin → ran 𝐴 ∈ Fin)
Theorem	fresin2 45144	Restriction of a function with respect to the intersection with its domain. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐹:𝐴⟶𝐵 → (𝐹 ↾ (𝐶 ∩ 𝐴)) = (𝐹 ↾ 𝐶))
Theorem	ffi 45145	A function with finite domain is finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ Fin) → 𝐹 ∈ Fin)
Theorem	suprnmpt 45146*	An explicit bound for the range of a bounded function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ 𝐶 = sup(ran 𝐹, ℝ, < )    ⇒   ⊢ (𝜑 → (𝐶 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝐶))
Theorem	rnffi 45147	The range of a function with finite domain is finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ Fin) → ran 𝐹 ∈ Fin)
Theorem	mptelpm 45148*	A function in maps-to notation is a partial map . (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (𝐶 ↑pm 𝐷))
Theorem	rnmptpr 45149*	Range of a function defined on an unordered pair. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ 𝐹 = (𝑥 ∈ {𝐴, 𝐵} ↦ 𝐶)    &   ⊢ (𝑥 = 𝐴 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝐵 → 𝐶 = 𝐸)    ⇒   ⊢ (𝜑 → ran 𝐹 = {𝐷, 𝐸})
Theorem	resmpti 45150*	Restriction of the mapping operation. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ 𝐵 ⊆ 𝐴    ⇒   ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ 𝐶)
Theorem	founiiun 45151*	Union expressed as an indexed union, when a map onto is given. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝐹:𝐴–onto→𝐵 → ∪ 𝐵 = ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥))
Theorem	rnresun 45152	Distribution law for range of a restriction over a union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ran (𝐹 ↾ (𝐴 ∪ 𝐵)) = (ran (𝐹 ↾ 𝐴) ∪ ran (𝐹 ↾ 𝐵))
Theorem	elrnmptf 45153	The range of a function in maps-to notation. Same as elrnmpt 5938, but using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑥𝐶    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵))
Theorem	rnmptssrn 45154*	Inclusion relation for two ranges expressed in maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ 𝐶 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → ran (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ ran (𝑦 ∈ 𝐶 ↦ 𝐷))
Theorem	disjf1 45155*	A 1 to 1 mapping built from disjoint, nonempty sets. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≠ ∅)    &   ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵)    ⇒   ⊢ (𝜑 → 𝐹:𝐴–1-1→𝑉)
Theorem	rnsnf 45156	The range of a function whose domain is a singleton. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:{𝐴}⟶𝐵)    ⇒   ⊢ (𝜑 → ran 𝐹 = {(𝐹‘𝐴)})
Theorem	wessf1ornlem 45157*	Given a function 𝐹 on a well-ordered domain 𝐴 there exists a subset of 𝐴 such that 𝐹 restricted to such subset is injective and onto the range of 𝐹 (without using the axiom of choice). (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ 𝐺 = (𝑦 ∈ ran 𝐹 ↦ (℩𝑥 ∈ (◡𝐹 “ {𝑦})∀𝑧 ∈ (◡𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝒫 𝐴(𝐹 ↾ 𝑥):𝑥–1-1-onto→ran 𝐹)
Theorem	wessf1orn 45158*	Given a function 𝐹 on a well-ordered domain 𝐴 there exists a subset of 𝐴 such that 𝐹 restricted to such subset is injective and onto the range of 𝐹 (without using the axiom of choice). (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 We 𝐴)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝒫 𝐴(𝐹 ↾ 𝑥):𝑥–1-1-onto→ran 𝐹)
Theorem	nelrnres 45159	If 𝐴 is not in the range, it is not in the range of any restriction. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (¬ 𝐴 ∈ ran 𝐵 → ¬ 𝐴 ∈ ran (𝐵 ↾ 𝐶))
Theorem	disjrnmpt2 45160*	Disjointness of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 → Disj 𝑦 ∈ ran 𝐹 𝑦)
Theorem	elrnmpt1sf 45161*	Elementhood in an image set. Same as elrnmpt1s 5939, but using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑥𝐶    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ (𝑥 = 𝐷 → 𝐵 = 𝐶)    ⇒   ⊢ ((𝐷 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → 𝐶 ∈ ran 𝐹)
Theorem	founiiun0 45162*	Union expressed as an indexed union, when a map onto is given. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝐹:𝐴–onto→(𝐵 ∪ {∅}) → ∪ 𝐵 = ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥))
Theorem	disjf1o 45163*	A bijection built from disjoint sets. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵)    &   ⊢ 𝐶 = {𝑥 ∈ 𝐴 ∣ 𝐵 ≠ ∅}    &   ⊢ 𝐷 = (ran 𝐹 ∖ {∅})    ⇒   ⊢ (𝜑 → (𝐹 ↾ 𝐶):𝐶–1-1-onto→𝐷)
Theorem	disjinfi 45164*	Only a finite number of disjoint sets can have a nonempty intersection with a finite set 𝐶. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ Fin)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ∈ Fin)
Theorem	fvovco 45165	Value of the composition of an operator, with a given function. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝐹:𝑋⟶(𝑉 × 𝑊))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ((𝑂 ∘ 𝐹)‘𝑌) = ((1st ‘(𝐹‘𝑌))𝑂(2nd ‘(𝐹‘𝑌))))
Theorem	ssnnf1octb 45166*	There exists a bijection between a subset of ℕ and a given nonempty countable set. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ ((𝐴 ≼ ω ∧ 𝐴 ≠ ∅) → ∃𝑓(dom 𝑓 ⊆ ℕ ∧ 𝑓:dom 𝑓–1-1-onto→𝐴))
Theorem	nnf1oxpnn 45167	There is a bijection between the set of positive integers and the Cartesian product of the set of positive integers with itself. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ ∃𝑓 𝑓:ℕ–1-1-onto→(ℕ × ℕ)
Theorem	rnmptssd 45168*	The range of a function given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)    ⇒   ⊢ (𝜑 → ran 𝐹 ⊆ 𝐶)
Theorem	projf1o 45169*	A biijection from a set to a projection in a two dimensional space. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ ⟨𝐴, 𝑥⟩)    ⇒   ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→({𝐴} × 𝐵))
Theorem	fvmap 45170	Function value for a member of a set exponentiation. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐴 ↑m 𝐵))    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹‘𝐶) ∈ 𝐴)
Theorem	fvixp2 45171*	Projection of a factor of an indexed Cartesian product. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ ((𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)
Theorem	choicefi 45172*	For a finite set, a choice function exists, without using the axiom of choice. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≠ ∅)    ⇒   ⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵))
Theorem	mpct 45173	The exponentiation of a countable set to a finite set is countable. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝜑 → 𝐴 ≼ ω)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    ⇒   ⊢ (𝜑 → (𝐴 ↑m 𝐵) ≼ ω)
Theorem	cnmetcoval 45174	Value of the distance function of the metric space of complex numbers, composed with a function. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ 𝐷 = (abs ∘ − )    &   ⊢ (𝜑 → 𝐹:𝐴⟶(ℂ × ℂ))    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ((𝐷 ∘ 𝐹)‘𝐵) = (abs‘((1st ‘(𝐹‘𝐵)) − (2nd ‘(𝐹‘𝐵)))))
Theorem	fcomptss 45175*	Express composition of two functions as a maps-to applying both in sequence. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)    &   ⊢ (𝜑 → 𝐺:𝐶⟶𝐷)    ⇒   ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ (𝐺‘(𝐹‘𝑥))))
Theorem	elmapsnd 45176	Membership in a set exponentiated to a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐹 Fn {𝐴})    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝐹‘𝐴) ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐵 ↑m {𝐴}))
Theorem	mapss2 45177	Subset inheritance for set exponentiation. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑍)    &   ⊢ (𝜑 → 𝐶 ≠ ∅)    ⇒   ⊢ (𝜑 → (𝐴 ⊆ 𝐵 ↔ (𝐴 ↑m 𝐶) ⊆ (𝐵 ↑m 𝐶)))
Theorem	fsneq 45178	Equality condition for two functions defined on a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ 𝐵 = {𝐴}    &   ⊢ (𝜑 → 𝐹 Fn 𝐵)    &   ⊢ (𝜑 → 𝐺 Fn 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 = 𝐺 ↔ (𝐹‘𝐴) = (𝐺‘𝐴)))
Theorem	difmap 45179	Difference of two sets exponentiations. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑍)    &   ⊢ (𝜑 → 𝐶 ≠ ∅)    ⇒   ⊢ (𝜑 → ((𝐴 ∖ 𝐵) ↑m 𝐶) ⊆ ((𝐴 ↑m 𝐶) ∖ (𝐵 ↑m 𝐶)))
Theorem	unirnmap 45180	Given a subset of a set exponentiation, the base set can be restricted. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ⊆ (𝐵 ↑m 𝐴))    ⇒   ⊢ (𝜑 → 𝑋 ⊆ (ran ∪ 𝑋 ↑m 𝐴))
Theorem	inmap 45181	Intersection of two sets exponentiations. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑍)    ⇒   ⊢ (𝜑 → ((𝐴 ↑m 𝐶) ∩ (𝐵 ↑m 𝐶)) = ((𝐴 ∩ 𝐵) ↑m 𝐶))
Theorem	fcoss 45182	Composition of two mappings. Similar to fco 6729, but with a weaker condition on the domain of 𝐹. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐺:𝐷⟶𝐶)    ⇒   ⊢ (𝜑 → (𝐹 ∘ 𝐺):𝐷⟶𝐵)
Theorem	fsneqrn 45183	Equality condition for two functions defined on a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ 𝐵 = {𝐴}    &   ⊢ (𝜑 → 𝐹 Fn 𝐵)    &   ⊢ (𝜑 → 𝐺 Fn 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 = 𝐺 ↔ (𝐹‘𝐴) ∈ ran 𝐺))
Theorem	difmapsn 45184	Difference of two sets exponentiatiated to a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑍)    ⇒   ⊢ (𝜑 → ((𝐴 ↑m {𝐶}) ∖ (𝐵 ↑m {𝐶})) = ((𝐴 ∖ 𝐵) ↑m {𝐶}))
Theorem	mapssbi 45185	Subset inheritance for set exponentiation. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑍)    &   ⊢ (𝜑 → 𝐶 ≠ ∅)    ⇒   ⊢ (𝜑 → (𝐴 ⊆ 𝐵 ↔ (𝐴 ↑m 𝐶) ⊆ (𝐵 ↑m 𝐶)))
Theorem	unirnmapsn 45186	Equality theorem for a subset of a set exponentiation, where the exponent is a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ 𝐶 = {𝐴}    &   ⊢ (𝜑 → 𝑋 ⊆ (𝐵 ↑m 𝐶))    ⇒   ⊢ (𝜑 → 𝑋 = (ran ∪ 𝑋 ↑m 𝐶))
Theorem	iunmapss 45187*	The indexed union of set exponentiations is a subset of the set exponentiation of the indexed union. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 (𝐵 ↑m 𝐶) ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐶))
Theorem	ssmapsn 45188*	A subset 𝐶 of a set exponentiation to a singleton, is its projection 𝐷 exponentiated to the singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ Ⅎ𝑓𝐷    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ⊆ (𝐵 ↑m {𝐴}))    &   ⊢ 𝐷 = ∪ 𝑓 ∈ 𝐶 ran 𝑓    ⇒   ⊢ (𝜑 → 𝐶 = (𝐷 ↑m {𝐴}))
Theorem	iunmapsn 45189*	The indexed union of set exponentiations to a singleton is equal to the set exponentiation of the indexed union. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑍)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 (𝐵 ↑m {𝐶}) = (∪ 𝑥 ∈ 𝐴 𝐵 ↑m {𝐶}))
Theorem	absfico 45190	Mapping domain and codomain of the absolute value function. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ abs:ℂ⟶(0[,)+∞)
Theorem	icof 45191	The set of left-closed right-open intervals of extended reals maps to subsets of extended reals. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ [,):(ℝ* × ℝ*)⟶𝒫 ℝ*
Theorem	elpmrn 45192	The range of a partial function. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝐹 ∈ (𝐴 ↑pm 𝐵) → ran 𝐹 ⊆ 𝐴)
Theorem	imaexi 45193	The image of a set is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) (Proof shortened by SN, 27-Apr-2025.)
⊢ 𝐴 ∈ 𝑉    ⇒   ⊢ (𝐴 “ 𝐵) ∈ V
Theorem	axccdom 45194*	Relax the constraint on ax-cc to dominance instead of equinumerosity. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑋 ≼ ω)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → 𝑧 ≠ ∅)    ⇒   ⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝑋 ∧ ∀𝑧 ∈ 𝑋 (𝑓‘𝑧) ∈ 𝑧))
Theorem	dmmptdff 45195	The domain of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 21-Dec-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ 𝐴 = (𝑥 ∈ 𝐵 ↦ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝑉)    ⇒   ⊢ (𝜑 → dom 𝐴 = 𝐵)
Theorem	dmmptdf 45196*	The domain of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ 𝐴 = (𝑥 ∈ 𝐵 ↦ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝑉)    ⇒   ⊢ (𝜑 → dom 𝐴 = 𝐵)
Theorem	elpmi2 45197	The domain of a partial function. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝐹 ∈ (𝐴 ↑pm 𝐵) → dom 𝐹 ⊆ 𝐵)
Theorem	dmrelrnrel 45198*	A relation preserving function. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐹‘𝑥)𝑆(𝐹‘𝑦)))    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐵𝑅𝐶)    ⇒   ⊢ (𝜑 → (𝐹‘𝐵)𝑆(𝐹‘𝐶))
Theorem	fvcod 45199	Value of a function composition. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → Fun 𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ dom 𝐺)    &   ⊢ 𝐻 = (𝐹 ∘ 𝐺)    ⇒   ⊢ (𝜑 → (𝐻‘𝐴) = (𝐹‘(𝐺‘𝐴)))
Theorem	elrnmpoid 45200*	Membership in the range of an operation class abstraction. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉) → (𝑥𝐹𝑦) ∈ ran 𝐹)