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	wfaxrep 45101*	The class of well-founded sets models the Axiom of Replacement ax-rep 5221. Actually, our statement is stronger, since it is an instance of Replacement only when all quantifiers in ∀𝑦𝜑 are relativized to 𝑊. Essentially part of Corollary II.2.5 of [Kunen2] p. 112, but note that our Replacement is different from Kunen's. (Contributed by Eric Schmidt, 29-Sep-2025.)
⊢ 𝑊 = ∪ (𝑅1 “ On)    ⇒   ⊢ ∀𝑥 ∈ 𝑊 (∀𝑤 ∈ 𝑊 ∃𝑦 ∈ 𝑊 ∀𝑧 ∈ 𝑊 (∀𝑦𝜑 → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑊 ∀𝑧 ∈ 𝑊 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑊 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑)))
Theorem	wfaxsep 45102*	The class of well-founded sets models the Axiom of Separation ax-sep 5238. Actually, our statement is stronger, since it is an instance of Separation only when all quantifiers in 𝜑 are relativized to 𝑊. Part of Corollary II.2.5 of [Kunen2] p. 112. (Contributed by Eric Schmidt, 29-Sep-2025.)
⊢ 𝑊 = ∪ (𝑅1 “ On)    ⇒   ⊢ ∀𝑧 ∈ 𝑊 ∃𝑦 ∈ 𝑊 ∀𝑥 ∈ 𝑊 (𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
Theorem	wfaxnul 45103*	The class of well-founded sets models the Null Set Axiom ax-nul 5248. (Contributed by Eric Schmidt, 19-Oct-2025.)
⊢ 𝑊 = ∪ (𝑅1 “ On)    ⇒   ⊢ ∃𝑥 ∈ 𝑊 ∀𝑦 ∈ 𝑊 ¬ 𝑦 ∈ 𝑥
Theorem	wfaxpow 45104*	The class of well-founded sets models the Axioms of Power Sets. Part of Corollary II.2.9 of [Kunen2] p. 113. (Contributed by Eric Schmidt, 19-Oct-2025.)
⊢ 𝑊 = ∪ (𝑅1 “ On)    ⇒   ⊢ ∀𝑥 ∈ 𝑊 ∃𝑦 ∈ 𝑊 ∀𝑧 ∈ 𝑊 (∀𝑤 ∈ 𝑊 (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
Theorem	wfaxpr 45105*	The class of well-founded sets models the Axiom of Pairing ax-pr 5374. Part of Corollary II.2.5 of [Kunen2] p. 112. (Contributed by Eric Schmidt, 29-Sep-2025.)
⊢ 𝑊 = ∪ (𝑅1 “ On)    ⇒   ⊢ ∀𝑥 ∈ 𝑊 ∀𝑦 ∈ 𝑊 ∃𝑧 ∈ 𝑊 ∀𝑤 ∈ 𝑊 ((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)
Theorem	wfaxun 45106*	The class of well-founded sets models the Axiom of Union ax-un 7677. Part of Corollary II.2.5 of [Kunen2] p. 112. (Contributed by Eric Schmidt, 19-Oct-2025.)
⊢ 𝑊 = ∪ (𝑅1 “ On)    ⇒   ⊢ ∀𝑥 ∈ 𝑊 ∃𝑦 ∈ 𝑊 ∀𝑧 ∈ 𝑊 (∃𝑤 ∈ 𝑊 (𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
Theorem	wfaxreg 45107*	The class of well-founded sets models the Axiom of Regularity ax-reg 9488. Part of Corollary II.2.5 of [Kunen2] p. 112. (Contributed by Eric Schmidt, 19-Oct-2025.)
⊢ 𝑊 = ∪ (𝑅1 “ On)    ⇒   ⊢ ∀𝑥 ∈ 𝑊 (∃𝑦 ∈ 𝑊 𝑦 ∈ 𝑥 → ∃𝑦 ∈ 𝑊 (𝑦 ∈ 𝑥 ∧ ∀𝑧 ∈ 𝑊 (𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥)))
Theorem	wfaxinf2 45108*	The class of well-founded sets models the Axiom of Infinity ax-inf2 9541. Part of Corollary II.2.12 of [Kunen2] p. 114. (Contributed by Eric Schmidt, 19-Oct-2025.)
⊢ 𝑊 = ∪ (𝑅1 “ On)    ⇒   ⊢ ∃𝑥 ∈ 𝑊 (∃𝑦 ∈ 𝑊 (𝑦 ∈ 𝑥 ∧ ∀𝑧 ∈ 𝑊 ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑦 ∈ 𝑊 (𝑦 ∈ 𝑥 → ∃𝑧 ∈ 𝑊 (𝑧 ∈ 𝑥 ∧ ∀𝑤 ∈ 𝑊 (𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦)))))
Theorem	wfac8prim 45109*	The class of well-founded sets 𝑊 models the Axiom of Choice. Since the previous theorems show that all the ZF axioms hold in 𝑊, we may use any statement that ZF proves is equivalent to Choice to prove this. We use ac8prim 45098. Part of Corollary II.2.12 of [Kunen2] p. 114. (Contributed by Eric Schmidt, 19-Oct-2025.)
⊢ 𝑊 = ∪ (𝑅1 “ On)    ⇒   ⊢ ∀𝑥 ∈ 𝑊 ((∀𝑧 ∈ 𝑊 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑊 𝑤 ∈ 𝑧) ∧ ∀𝑧 ∈ 𝑊 ∀𝑤 ∈ 𝑊 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑊 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))) → ∃𝑦 ∈ 𝑊 ∀𝑧 ∈ 𝑊 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑊 ∀𝑣 ∈ 𝑊 ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤)))
21.42.9  Permutation models
Theorem	brpermmodel 45110	The membership relation in a permutation model. We use a permutation 𝐹 of the universe to define a relation 𝑅 that serves as the membership relation in our model. The conclusion of this theorem is Definition II.9.1 of [Kunen2] p. 148. All the axioms of ZFC except for Regularity hold in permutation models, and Regularity will be false if 𝐹 is chosen appropriately. Thus, permutation models can be used to show that Regularity does not follow from the other axioms (with the usual proviso that the axioms are consistent). (Contributed by Eric Schmidt, 6-Nov-2025.)
⊢ 𝐹:V–1-1-onto→V    &   ⊢ 𝑅 = (◡𝐹 ∘ E )    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴𝑅𝐵 ↔ 𝐴 ∈ (𝐹‘𝐵))
Theorem	brpermmodelcnv 45111	Ordinary membership expressed in terms of the permutation model's membership relation. (Contributed by Eric Schmidt, 6-Nov-2025.)
⊢ 𝐹:V–1-1-onto→V    &   ⊢ 𝑅 = (◡𝐹 ∘ E )    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴𝑅(◡𝐹‘𝐵) ↔ 𝐴 ∈ 𝐵)
Theorem	permaxext 45112*	The Axiom of Extensionality ax-ext 2705 holds in permutation models. Part of Exercise II.9.2 of [Kunen2] p. 148. (Contributed by Eric Schmidt, 6-Nov-2025.)
⊢ 𝐹:V–1-1-onto→V    &   ⊢ 𝑅 = (◡𝐹 ∘ E )    ⇒   ⊢ (∀𝑧(𝑧𝑅𝑥 ↔ 𝑧𝑅𝑦) → 𝑥 = 𝑦)
Theorem	permaxrep 45113*	The Axiom of Replacement ax-rep 5221 holds in permutation models. Part of Exercise II.9.2 of [Kunen2] p. 148. Note that, to prove that an instance of Replacement holds in the model, 𝜑 would need have all instances of ∈ replaced with 𝑅. But this still results in an instance of this theorem, so we do establish that Replacement holds. (Contributed by Eric Schmidt, 6-Nov-2025.)
⊢ 𝐹:V–1-1-onto→V    &   ⊢ 𝑅 = (◡𝐹 ∘ E )    ⇒   ⊢ (∀𝑤∃𝑦∀𝑧(∀𝑦𝜑 → 𝑧 = 𝑦) → ∃𝑦∀𝑧(𝑧𝑅𝑦 ↔ ∃𝑤(𝑤𝑅𝑥 ∧ ∀𝑦𝜑)))
Theorem	permaxsep 45114*	The Axiom of Separation ax-sep 5238 holds in permutation models. Part of Exercise II.9.2 of [Kunen2] p. 148. Note that, to prove that an instance of Separation holds in the model, 𝜑 would need have all instances of ∈ replaced with 𝑅. But this still results in an instance of this theorem, so we do establish that Separation holds. (Contributed by Eric Schmidt, 6-Nov-2025.)
⊢ 𝐹:V–1-1-onto→V    &   ⊢ 𝑅 = (◡𝐹 ∘ E )    ⇒   ⊢ ∃𝑦∀𝑥(𝑥𝑅𝑦 ↔ (𝑥𝑅𝑧 ∧ 𝜑))
Theorem	permaxnul 45115*	The Null Set Axiom ax-nul 5248 holds in permutation models. Part of Exercise II.9.2 of [Kunen2] p. 148. (Contributed by Eric Schmidt, 6-Nov-2025.)
⊢ 𝐹:V–1-1-onto→V    &   ⊢ 𝑅 = (◡𝐹 ∘ E )    ⇒   ⊢ ∃𝑥∀𝑦 ¬ 𝑦𝑅𝑥
Theorem	permaxpow 45116*	The Axiom of Power Sets ax-pow 5307 holds in permutation models. Part of Exercise II.9.2 of [Kunen2] p. 148. (Contributed by Eric Schmidt, 6-Nov-2025.)
⊢ 𝐹:V–1-1-onto→V    &   ⊢ 𝑅 = (◡𝐹 ∘ E )    ⇒   ⊢ ∃𝑦∀𝑧(∀𝑤(𝑤𝑅𝑧 → 𝑤𝑅𝑥) → 𝑧𝑅𝑦)
Theorem	permaxpr 45117*	The Axiom of Pairing ax-pr 5374 holds in permutation models. Part of Exercise II.9.2 of [Kunen2] p. 148. (Contributed by Eric Schmidt, 6-Nov-2025.)
⊢ 𝐹:V–1-1-onto→V    &   ⊢ 𝑅 = (◡𝐹 ∘ E )    ⇒   ⊢ ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤𝑅𝑧)
Theorem	permaxun 45118*	The Axiom of Union ax-un 7677 holds in permutation models. Part of Exercise II.9.2 of [Kunen2] p. 148. (Contributed by Eric Schmidt, 6-Nov-2025.)
⊢ 𝐹:V–1-1-onto→V    &   ⊢ 𝑅 = (◡𝐹 ∘ E )    ⇒   ⊢ ∃𝑦∀𝑧(∃𝑤(𝑧𝑅𝑤 ∧ 𝑤𝑅𝑥) → 𝑧𝑅𝑦)
Theorem	permaxinf2lem 45119*	Lemma for permaxinf2 45120. (Contributed by Eric Schmidt, 6-Nov-2025.)
⊢ 𝐹:V–1-1-onto→V    &   ⊢ 𝑅 = (◡𝐹 ∘ E )    &   ⊢ 𝑍 = (rec((𝑣 ∈ V ↦ (◡𝐹‘((𝐹‘𝑣) ∪ {𝑣}))), (◡𝐹‘∅)) “ ω)    ⇒   ⊢ ∃𝑥(∃𝑦(𝑦𝑅𝑥 ∧ ∀𝑧 ¬ 𝑧𝑅𝑦) ∧ ∀𝑦(𝑦𝑅𝑥 → ∃𝑧(𝑧𝑅𝑥 ∧ ∀𝑤(𝑤𝑅𝑧 ↔ (𝑤𝑅𝑦 ∨ 𝑤 = 𝑦)))))
Theorem	permaxinf2 45120*	The Axiom of Infinity ax-inf2 9541 holds in permutation models. Part of Exercise II.9.2 of [Kunen2] p. 148. (Contributed by Eric Schmidt, 6-Nov-2025.)
⊢ 𝐹:V–1-1-onto→V    &   ⊢ 𝑅 = (◡𝐹 ∘ E )    ⇒   ⊢ ∃𝑥(∃𝑦(𝑦𝑅𝑥 ∧ ∀𝑧 ¬ 𝑧𝑅𝑦) ∧ ∀𝑦(𝑦𝑅𝑥 → ∃𝑧(𝑧𝑅𝑥 ∧ ∀𝑤(𝑤𝑅𝑧 ↔ (𝑤𝑅𝑦 ∨ 𝑤 = 𝑦)))))
Theorem	permac8prim 45121*	The Axiom of Choice ac8prim 45098 holds in permutation models. Part of Exercise II.9.3 of [Kunen2] p. 149. Note that ax-ac 10360 requires Regularity for its derivation from the usual Axiom of Choice and does not necessarily hold in permutation models. (Contributed by Eric Schmidt, 16-Nov-2025.)
⊢ 𝐹:V–1-1-onto→V    &   ⊢ 𝑅 = (◡𝐹 ∘ E )    ⇒   ⊢ ((∀𝑧(𝑧𝑅𝑥 → ∃𝑤 𝑤𝑅𝑧) ∧ ∀𝑧∀𝑤((𝑧𝑅𝑥 ∧ 𝑤𝑅𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦(𝑦𝑅𝑧 → ¬ 𝑦𝑅𝑤)))) → ∃𝑦∀𝑧(𝑧𝑅𝑥 → ∃𝑤∀𝑣((𝑣𝑅𝑧 ∧ 𝑣𝑅𝑦) ↔ 𝑣 = 𝑤)))
Theorem	nregmodelf1o 45122	Define a permutation 𝐹 used to produce a model in which ax-reg 9488 is false. The permutation swaps ∅ and {∅} and leaves the rest of 𝑉 fixed. This is an example given after Exercise II.9.2 of [Kunen2] p. 148. (Contributed by Eric Schmidt, 16-Nov-2025.)
⊢ 𝐹 = (( I ↾ (V ∖ {∅, {∅}})) ∪ {⟨∅, {∅}⟩, ⟨{∅}, ∅⟩})    ⇒   ⊢ 𝐹:V–1-1-onto→V
Theorem	nregmodellem 45123	Lemma for nregmodel 45124. (Contributed by Eric Schmidt, 16-Nov-2025.)
⊢ 𝐹 = (( I ↾ (V ∖ {∅, {∅}})) ∪ {⟨∅, {∅}⟩, ⟨{∅}, ∅⟩})    &   ⊢ 𝑅 = (◡𝐹 ∘ E )    ⇒   ⊢ (𝑥𝑅∅ ↔ 𝑥 ∈ {∅})
Theorem	nregmodel 45124*	The Axiom of Regularity ax-reg 9488 is false in the permutation model defined from 𝐹. Since the other axioms of ZFC hold in all permutation models (permaxext 45112 through permac8prim 45121), we can conclude that Regularity does not follow from those axioms, assuming ZFC is consistent. (If we could prove Regularity from the other axioms, we could prove it in the permutation model and thus obtain a contradiction with this theorem.) Since we also know that Regularity is consistent with the other axioms (wfaxext 45100 through wfac8prim 45109), Regularity is neither provable nor disprovable from the other axioms; i.e., it is independent of them. (Contributed by Eric Schmidt, 16-Nov-2025.)
⊢ 𝐹 = (( I ↾ (V ∖ {∅, {∅}})) ∪ {⟨∅, {∅}⟩, ⟨{∅}, ∅⟩})    &   ⊢ 𝑅 = (◡𝐹 ∘ E )    ⇒   ⊢ ¬ ∀𝑥(∃𝑦 𝑦𝑅𝑥 → ∃𝑦(𝑦𝑅𝑥 ∧ ∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧𝑅𝑥)))
Theorem	nregmodelaxext 45125*	The Axiom of Extensionality ax-ext 2705 is true in the permutation model defined from 𝐹. This theorem is an immediate consequence of the fact that ax-ext 2705 holds in all permutation models and is provided as an illustration. (Contributed by Eric Schmidt, 16-Nov-2025.)
⊢ 𝐹 = (( I ↾ (V ∖ {∅, {∅}})) ∪ {⟨∅, {∅}⟩, ⟨{∅}, ∅⟩})    &   ⊢ 𝑅 = (◡𝐹 ∘ E )    ⇒   ⊢ (∀𝑧(𝑧𝑅𝑥 ↔ 𝑧𝑅𝑦) → 𝑥 = 𝑦)
21.43  Mathbox for Glauco Siliprandi
21.43.1  Miscellanea
Theorem	evth2f 45126*	A version of evth2 24896 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑦𝐹    &   ⊢ Ⅎ𝑥𝑋    &   ⊢ Ⅎ𝑦𝑋    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝑋 ≠ ∅)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐹‘𝑥) ≤ (𝐹‘𝑦))
Theorem	elunif 45127*	A version of eluni 4863 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))
Theorem	rzalf 45128	A version of rzal 4460 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑥 𝐴 = ∅    ⇒   ⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 𝜑)
Theorem	fvelrnbf 45129	A version of fvelrnb 6891 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝐹    ⇒   ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))
Theorem	rfcnpre1 45130	If F is a continuous function with respect to the standard topology, then the preimage A of the values greater than a given extended real B is an open set. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐴 = {𝑥 ∈ 𝑋 ∣ 𝐵 < (𝐹‘𝑥)}    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐽)
Theorem	ubelsupr 45131*	If U belongs to A and U is an upper bound, then U is the sup of A. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝑈 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑥 ≤ 𝑈) → 𝑈 = sup(𝐴, ℝ, < ))
Theorem	fsumcnf 45132*	A finite sum of functions to complex numbers from a common topological space is continuous, without disjoint var constraint x ph. The class expression for B normally contains free variables k and x to index it. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ 𝐾 = (TopOpen‘ℂfld)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵) ∈ (𝐽 Cn 𝐾))
Theorem	mulltgt0 45133	The product of a negative and a positive number is negative. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐴 < 0) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → (𝐴 · 𝐵) < 0)
Theorem	rspcegf 45134	A version of rspcev 3574 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)
Theorem	rabexgf 45135	A version of rabexg 5279 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)
Theorem	fcnre 45136	A function continuous with respect to the standard topology, is a real mapping. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ 𝑇 = ∪ 𝐽    &   ⊢ 𝐶 = (𝐽 Cn 𝐾)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐶)    ⇒   ⊢ (𝜑 → 𝐹:𝑇⟶ℝ)
Theorem	sumsnd 45137*	A sum of a singleton is the term. The deduction version of sumsn 15663. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ (𝜑 → Ⅎ𝑘𝐵)    &   ⊢ Ⅎ𝑘𝜑    &   ⊢ ((𝜑 ∧ 𝑘 = 𝑀) → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ {𝑀}𝐴 = 𝐵)
Theorem	evthf 45138*	A version of evth 24895 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑦𝐹    &   ⊢ Ⅎ𝑥𝑋    &   ⊢ Ⅎ𝑦𝑋    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝑋 ≠ ∅)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ (𝐹‘𝑥))
Theorem	cnfex 45139	The class of continuous functions between two topologies is a set. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝐽 Cn 𝐾) ∈ V)
Theorem	fnchoice 45140*	For a finite set, a choice function exists, without using the axiom of choice. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ (𝐴 ∈ Fin → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
Theorem	refsumcn 45141*	A finite sum of continuous real functions, from a common topological space, is continuous. The class expression for B normally contains free variables k and x to index it. See fsumcn 24798 for the analogous theorem on continuous complex functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵) ∈ (𝐽 Cn 𝐾))
Theorem	rfcnpre2 45142	If 𝐹 is a continuous function with respect to the standard topology, then the preimage A of the values smaller than a given extended real 𝐵, is an open set. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐴 = {𝑥 ∈ 𝑋 ∣ (𝐹‘𝑥) < 𝐵}    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐽)
Theorem	cncmpmax 45143*	When the hypothesis for the extreme value theorem hold, then the sup of the range of the function belongs to the range, it is real and it an upper bound of the range. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ 𝑇 = ∪ 𝐽    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝑇 ≠ ∅)    ⇒   ⊢ (𝜑 → (sup(ran 𝐹, ℝ, < ) ∈ ran 𝐹 ∧ sup(ran 𝐹, ℝ, < ) ∈ ℝ ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ≤ sup(ran 𝐹, ℝ, < )))
Theorem	rfcnpre3 45144*	If F is a continuous function with respect to the standard topology, then the preimage A of the values greater than or equal to a given real B is a closed set. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝐹    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ 𝑇 = ∪ 𝐽    &   ⊢ 𝐴 = {𝑡 ∈ 𝑇 ∣ 𝐵 ≤ (𝐹‘𝑡)}    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → 𝐴 ∈ (Clsd‘𝐽))
Theorem	rfcnpre4 45145*	If F is a continuous function with respect to the standard topology, then the preimage A of the values less than or equal to a given real B is a closed set. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝐹    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ 𝑇 = ∪ 𝐽    &   ⊢ 𝐴 = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ 𝐵}    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → 𝐴 ∈ (Clsd‘𝐽))
Theorem	sumpair 45146*	Sum of two distinct complex values. The class expression for 𝐴 and 𝐵 normally contain free variable 𝑘 to index it. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ (𝜑 → Ⅎ𝑘𝐷)    &   ⊢ (𝜑 → Ⅎ𝑘𝐸)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝐸 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 = 𝐴) → 𝐶 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑘 = 𝐵) → 𝐶 = 𝐸)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ {𝐴, 𝐵}𝐶 = (𝐷 + 𝐸))
Theorem	rfcnnnub 45147*	Given a real continuous function 𝐹 defined on a compact topological space, there is always a positive integer that is a strict upper bound of its range. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝐹    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ 𝑇 = ∪ 𝐽    &   ⊢ (𝜑 → 𝑇 ≠ ∅)    &   ⊢ 𝐶 = (𝐽 Cn 𝐾)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐶)    ⇒   ⊢ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) < 𝑛)
Theorem	refsum2cnlem1 45148*	This is the core Lemma for refsum2cn 45149: the sum of two continuous real functions (from a common topological space) is continuous. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐺    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ 𝐴 = (𝑘 ∈ {1, 2} ↦ if(𝑘 = 1, 𝐹, 𝐺))    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ((𝐹‘𝑥) + (𝐺‘𝑥))) ∈ (𝐽 Cn 𝐾))
Theorem	refsum2cn 45149*	The sum of two continuus real functions (from a common topological space) is continuous. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐺    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ((𝐹‘𝑥) + (𝐺‘𝑥))) ∈ (𝐽 Cn 𝐾))
Theorem	adantlllr 45150	Deduction adding a conjunct to antecedent. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (((((𝜑 ∧ 𝜂) ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
Theorem	3adantlr3 45151	Deduction adding a conjunct to antecedent. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜂)) ∧ 𝜃) → 𝜏)
Theorem	3adantll2 45152	Deduction adding a conjunct to antecedent. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((((𝜑 ∧ 𝜂 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
Theorem	3adantll3 45153	Deduction adding a conjunct to antecedent. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜂) ∧ 𝜒) ∧ 𝜃) → 𝜏)
Theorem	ssnel 45154	If not element of a set, then not element of a subset. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ⊆ 𝐵 ∧ ¬ 𝐶 ∈ 𝐵) → ¬ 𝐶 ∈ 𝐴)
Theorem	sncldre 45155	A singleton is closed w.r.t. the standard topology on the reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐴 ∈ ℝ → {𝐴} ∈ (Clsd‘(topGen‘ran (,))))
Theorem	n0p 45156	A polynomial with a nonzero coefficient is not the zero polynomial. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ ((𝑃 ∈ (Poly‘ℤ) ∧ 𝑁 ∈ ℕ0 ∧ ((coeff‘𝑃)‘𝑁) ≠ 0) → 𝑃 ≠ 0𝑝)
Theorem	pm2.65ni 45157	Inference rule for proof by contradiction. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (¬ 𝜑 → 𝜓)    &   ⊢ (¬ 𝜑 → ¬ 𝜓)    ⇒   ⊢ 𝜑
Theorem	iuneq2df 45158	Equality deduction for indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)
Theorem	nnfoctb 45159*	There exists a mapping from ℕ onto any (nonempty) countable set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ((𝐴 ≼ ω ∧ 𝐴 ≠ ∅) → ∃𝑓 𝑓:ℕ–onto→𝐴)
Theorem	elpwinss 45160	An element of the powerset of 𝐵 intersected with anything, is a subset of 𝐵. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝐴 ∈ (𝒫 𝐵 ∩ 𝐶) → 𝐴 ⊆ 𝐵)
Theorem	unidmex 45161	If 𝐹 is a set, then ∪ dom 𝐹 is a set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ 𝑋 = ∪ dom 𝐹    ⇒   ⊢ (𝜑 → 𝑋 ∈ V)
Theorem	ndisj2 45162*	A non-disjointness condition. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ (¬ Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 ∧ (𝐵 ∩ 𝐶) ≠ ∅))
Theorem	zenom 45163	The set of integer numbers is equinumerous to omega (the set of finite ordinal numbers). (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ℤ ≈ ω
Theorem	uzwo4 45164*	Well-ordering principle: any nonempty subset of an upper set of integers has the least element. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑗𝜓    &   ⊢ (𝑗 = 𝑘 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝑆 ⊆ (ℤ≥‘𝑀) ∧ ∃𝑗 ∈ 𝑆 𝜑) → ∃𝑗 ∈ 𝑆 (𝜑 ∧ ∀𝑘 ∈ 𝑆 (𝑘 < 𝑗 → ¬ 𝜓)))
Theorem	unisn0 45165	The union of the singleton of the empty set is the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ∪ {∅} = ∅
Theorem	ssin0 45166	If two classes are disjoint, two respective subclasses are disjoint. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵) → (𝐶 ∩ 𝐷) = ∅)
Theorem	inabs3 45167	Absorption law for intersection. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝐶 ⊆ 𝐵 → ((𝐴 ∩ 𝐵) ∩ 𝐶) = (𝐴 ∩ 𝐶))
Theorem	pwpwuni 45168	Relationship between power class and union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝒫 𝐵 ↔ ∪ 𝐴 ∈ 𝒫 𝐵))
Theorem	disjiun2 45169*	In a disjoint collection, an indexed union is disjoint from an additional term. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐷 ∈ (𝐴 ∖ 𝐶))    &   ⊢ (𝑥 = 𝐷 → 𝐵 = 𝐸)    ⇒   ⊢ (𝜑 → (∪ 𝑥 ∈ 𝐶 𝐵 ∩ 𝐸) = ∅)
Theorem	0pwfi 45170	The empty set is in any power set, and it's finite. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ∅ ∈ (𝒫 𝐴 ∩ Fin)
Theorem	ssinss2d 45171	Intersection preserves subclass relationship. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 ∩ 𝐵) ⊆ 𝐶)
Theorem	zct 45172	The set of integer numbers is countable. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ℤ ≼ ω
Theorem	pwfin0 45173	A finite set always belongs to a power class. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝒫 𝐴 ∩ Fin) ≠ ∅
Theorem	uzct 45174	An upper integer set is countable. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ 𝑍 = (ℤ≥‘𝑁)    ⇒   ⊢ 𝑍 ≼ ω
Theorem	iunxsnf 45175*	A singleton index picks out an instance of an indexed union's argument. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑥𝐶    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ ∪ 𝑥 ∈ {𝐴}𝐵 = 𝐶
Theorem	fiiuncl 45176*	If a set is closed under the union of two sets, then it is closed under finite indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷 ∧ 𝑧 ∈ 𝐷) → (𝑦 ∪ 𝑧) ∈ 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐷)
Theorem	iunp1 45177*	The addition of the next set to a union indexed by a finite set of sequential integers. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑘𝐵    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ (𝑘 = (𝑁 + 1) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ∪ 𝑘 ∈ (𝑀...(𝑁 + 1))𝐴 = (∪ 𝑘 ∈ (𝑀...𝑁)𝐴 ∪ 𝐵))
Theorem	fiunicl 45178*	If a set is closed under the union of two sets, then it is closed under finite union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∪ 𝑦) ∈ 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    ⇒   ⊢ (𝜑 → ∪ 𝐴 ∈ 𝐴)
Theorem	ixpeq2d 45179	Equality theorem for infinite Cartesian product. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶)
Theorem	disjxp1 45180*	The sets of a cartesian product are disjoint if the sets in the first argument are disjoint. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵)    ⇒   ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 (𝐵 × 𝐶))
Theorem	disjsnxp 45181*	The sets in the cartesian product of singletons with other sets, are disjoint. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ Disj 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)
Theorem	eliind 45182*	Membership in indexed intersection. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝜑 → 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐵)    &   ⊢ (𝑥 = 𝐾 → (𝐴 ∈ 𝐶 ↔ 𝐴 ∈ 𝐷))    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐷)
Theorem	rspcef 45183	Restricted existential specialization, using implicit substitution. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)
Theorem	ixpssmapc 45184*	An infinite Cartesian product is a subset of set exponentiation. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 ⊆ (𝐶 ↑m 𝐴))
Theorem	elintd 45185*	Membership in class intersection. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ 𝑥)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ∩ 𝐵)
Theorem	ssdf 45186*	A sufficient condition for a subclass relationship. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
Theorem	brneqtrd 45187	Substitution of equal classes into the negation of a binary relation. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝜑 → ¬ 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ¬ 𝐴𝑅𝐶)
Theorem	ssnct 45188	A set containing an uncountable set is itself uncountable. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝜑 → ¬ 𝐴 ≼ ω)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → ¬ 𝐵 ≼ ω)
Theorem	ssuniint 45189*	Sufficient condition for being a subclass of the union of an intersection. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ 𝑥)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ ∪ ∩ 𝐵)
Theorem	elintdv 45190*	Membership in class intersection. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ 𝑥)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ∩ 𝐵)
Theorem	ssd 45191*	A sufficient condition for a subclass relationship. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
Theorem	ralimralim 45192	Introducing any antecedent in a restricted universal quantification. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑))
Theorem	snelmap 45193	Membership of the element in the range of a constant map. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → (𝐴 × {𝑥}) ∈ (𝐵 ↑m 𝐴))    ⇒   ⊢ (𝜑 → 𝑥 ∈ 𝐵)
Theorem	xrnmnfpnf 45194	An extended real that is neither real nor minus infinity, is plus infinity. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → ¬ 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ -∞)    ⇒   ⊢ (𝜑 → 𝐴 = +∞)
Theorem	nelrnmpt 45195*	Non-membership in the range of a function in maps-to notaion. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ≠ 𝐵)    ⇒   ⊢ (𝜑 → ¬ 𝐶 ∈ ran 𝐹)
Theorem	iuneq1i 45196	Equality theorem for indexed union. (Contributed by Glauco Siliprandi, 3-Mar-2021.) Remove DV conditions. (Revised by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶
Theorem	nssrex 45197*	Negation of subclass relationship. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (¬ 𝐴 ⊆ 𝐵 ↔ ∃𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵)
Theorem	ssinc 45198*	Inclusion relation for a monotonic sequence of sets. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑚 ∈ (𝑀..^𝑁)) → (𝐹‘𝑚) ⊆ (𝐹‘(𝑚 + 1)))    ⇒   ⊢ (𝜑 → (𝐹‘𝑀) ⊆ (𝐹‘𝑁))
Theorem	ssdec 45199*	Inclusion relation for a monotonic sequence of sets. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑚 ∈ (𝑀..^𝑁)) → (𝐹‘(𝑚 + 1)) ⊆ (𝐹‘𝑚))    ⇒   ⊢ (𝜑 → (𝐹‘𝑁) ⊆ (𝐹‘𝑀))
Theorem	elixpconstg 45200*	Membership in an infinite Cartesian product of a constant 𝐵. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ 𝐹:𝐴⟶𝐵))