![]() |
Metamath
Proof Explorer Theorem List (p. 451 of 491) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pwfin0 45001 | A finite set always belongs to a power class. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝒫 𝐴 ∩ Fin) ≠ ∅ | ||
Theorem | uzct 45002 | An upper integer set is countable. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ 𝑍 = (ℤ≥‘𝑁) ⇒ ⊢ 𝑍 ≼ ω | ||
Theorem | iunxsnf 45003* | A singleton index picks out an instance of an indexed union's argument. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑥𝐶 & ⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ ∪ 𝑥 ∈ {𝐴}𝐵 = 𝐶 | ||
Theorem | fiiuncl 45004* | 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 45005* | 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 45006* | 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 45007 | Equality theorem for infinite Cartesian product. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶) | ||
Theorem | disjxp1 45008* | 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 45009* | The sets in the cartesian product of singletons with other sets, are disjoint. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ Disj 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) | ||
Theorem | eliind 45010* | Membership in indexed intersection. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶) & ⊢ (𝜑 → 𝐾 ∈ 𝐵) & ⊢ (𝑥 = 𝐾 → (𝐴 ∈ 𝐶 ↔ 𝐴 ∈ 𝐷)) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐷) | ||
Theorem | rspcef 45011 | Restricted existential specialization, using implicit substitution. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑) | ||
Theorem | ixpssmapc 45012* | An infinite Cartesian product is a subset of set exponentiation. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 ⊆ (𝐶 ↑m 𝐴)) | ||
Theorem | elintd 45013* | Membership in class intersection. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ 𝑥) ⇒ ⊢ (𝜑 → 𝐴 ∈ ∩ 𝐵) | ||
Theorem | ssdf 45014* | A sufficient condition for a subclass relationship. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | ||
Theorem | brneqtrd 45015 | Substitution of equal classes into the negation of a binary relation. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ (𝜑 → ¬ 𝐴𝑅𝐵) & ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ¬ 𝐴𝑅𝐶) | ||
Theorem | ssnct 45016 | A set containing an uncountable set is itself uncountable. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ (𝜑 → ¬ 𝐴 ≼ ω) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐵 ≼ ω) | ||
Theorem | ssuniint 45017* | Sufficient condition for being a subclass of the union of an intersection. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ 𝑥) ⇒ ⊢ (𝜑 → 𝐴 ⊆ ∪ ∩ 𝐵) | ||
Theorem | elintdv 45018* | Membership in class intersection. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ 𝑥) ⇒ ⊢ (𝜑 → 𝐴 ∈ ∩ 𝐵) | ||
Theorem | ssd 45019* | A sufficient condition for a subclass relationship. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | ||
Theorem | ralimralim 45020 | Introducing any antecedent in a restricted universal quantification. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑)) | ||
Theorem | snelmap 45021 | Membership of the element in the range of a constant map. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → (𝐴 × {𝑥}) ∈ (𝐵 ↑m 𝐴)) ⇒ ⊢ (𝜑 → 𝑥 ∈ 𝐵) | ||
Theorem | xrnmnfpnf 45022 | An extended real that is neither real nor minus infinity, is plus infinity. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → ¬ 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≠ -∞) ⇒ ⊢ (𝜑 → 𝐴 = +∞) | ||
Theorem | nelrnmpt 45023* | Non-membership in the range of a function in maps-to notaion. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ≠ 𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐶 ∈ ran 𝐹) | ||
Theorem | iuneq1i 45024 | Equality theorem for indexed union. (Contributed by Glauco Siliprandi, 3-Mar-2021.) Remove DV conditions. (Revised by GG, 1-Sep-2025.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶 | ||
Theorem | nssrex 45025* | Negation of subclass relationship. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (¬ 𝐴 ⊆ 𝐵 ↔ ∃𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵) | ||
Theorem | ssinc 45026* | Inclusion relation for a monotonic sequence of sets. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑚 ∈ (𝑀..^𝑁)) → (𝐹‘𝑚) ⊆ (𝐹‘(𝑚 + 1))) ⇒ ⊢ (𝜑 → (𝐹‘𝑀) ⊆ (𝐹‘𝑁)) | ||
Theorem | ssdec 45027* | Inclusion relation for a monotonic sequence of sets. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑚 ∈ (𝑀..^𝑁)) → (𝐹‘(𝑚 + 1)) ⊆ (𝐹‘𝑚)) ⇒ ⊢ (𝜑 → (𝐹‘𝑁) ⊆ (𝐹‘𝑀)) | ||
Theorem | elixpconstg 45028* | Membership in an infinite Cartesian product of a constant 𝐵. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ 𝐹:𝐴⟶𝐵)) | ||
Theorem | iineq1d 45029* | Equality theorem for indexed intersection. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐶) | ||
Theorem | metpsmet 45030 | A metric is a pseudometric. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (PsMet‘𝑋)) | ||
Theorem | ixpssixp 45031 | Subclass theorem for infinite Cartesian product. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 ⊆ X𝑥 ∈ 𝐴 𝐶) | ||
Theorem | ballss3 45032* | A sufficient condition for a ball being a subset. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐷 ∈ (PsMet‘𝑋)) & ⊢ (𝜑 → 𝑃 ∈ 𝑋) & ⊢ (𝜑 → 𝑅 ∈ ℝ*) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅) → 𝑥 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑃(ball‘𝐷)𝑅) ⊆ 𝐴) | ||
Theorem | iunincfi 45033* | Given a sequence of increasing sets, the union of a finite subsequence, is its last element. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ⇒ ⊢ (𝜑 → ∪ 𝑛 ∈ (𝑀...𝑁)(𝐹‘𝑛) = (𝐹‘𝑁)) | ||
Theorem | nsstr 45034 | If it's not a subclass, it's not a subclass of a smaller one. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ ((¬ 𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐵) → ¬ 𝐴 ⊆ 𝐶) | ||
Theorem | rexanuz3 45035* | Combine two different upper integer properties into one, for a single integer. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑗𝜑 & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜒) & ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜓) & ⊢ (𝑘 = 𝑗 → (𝜒 ↔ 𝜃)) & ⊢ (𝑘 = 𝑗 → (𝜓 ↔ 𝜏)) ⇒ ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 (𝜃 ∧ 𝜏)) | ||
Theorem | cbvmpo2 45036* | Rule to change the second bound variable in a maps-to function, using implicit substitution. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑤𝐴 & ⊢ Ⅎ𝑤𝐶 & ⊢ Ⅎ𝑦𝐸 & ⊢ (𝑦 = 𝑤 → 𝐶 = 𝐸) ⇒ ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐸) | ||
Theorem | cbvmpo1 45037* | Rule to change the first bound variable in a maps-to function, using implicit substitution. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑧𝐵 & ⊢ Ⅎ𝑧𝐶 & ⊢ Ⅎ𝑥𝐸 & ⊢ (𝑥 = 𝑧 → 𝐶 = 𝐸) ⇒ ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) | ||
Theorem | eliuniin 45038* | Indexed union of indexed intersections. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ 𝐴 = ∪ 𝑥 ∈ 𝐵 ∩ 𝑦 ∈ 𝐶 𝐷 ⇒ ⊢ (𝑍 ∈ 𝑉 → (𝑍 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷)) | ||
Theorem | ssabf 45039 | Subclass of a class abstraction. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝐴 ⊆ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | ||
Theorem | pssnssi 45040 | A proper subclass does not include the other class. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ 𝐴 ⊊ 𝐵 ⇒ ⊢ ¬ 𝐵 ⊆ 𝐴 | ||
Theorem | rabidim2 45041 | Membership in a restricted abstraction, implication. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} → 𝜑) | ||
Theorem | eluni2f 45042* | Membership in class union. Restricted quantifier version. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥) | ||
Theorem | eliin2f 45043* | Membership in indexed intersection. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐵 ≠ ∅ → (𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)) | ||
Theorem | nssd 45044 | Negation of subclass relationship. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → ¬ 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐴 ⊆ 𝐵) | ||
Theorem | iineq12dv 45045* | Equality deduction for indexed intersection. (Contributed by Glauco Siliprandi, 26-Jun-2021.) Remove DV conditions. (Revised by GG, 1-Sep-2025.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐷) | ||
Theorem | supxrcld 45046 | The supremum of an arbitrary set of extended reals is an extended real. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ*) ⇒ ⊢ (𝜑 → sup(𝐴, ℝ*, < ) ∈ ℝ*) | ||
Theorem | elrestd 45047 | A sufficient condition for being an open set of a subspace topology. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐽 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝑋 ∈ 𝐽) & ⊢ 𝐴 = (𝑋 ∩ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ∈ (𝐽 ↾t 𝐵)) | ||
Theorem | eliuniincex 45048* | Counterexample to show that the additional conditions in eliuniin 45038 and eliuniin2 45059 are actually needed. Notice that the definition of 𝐴 is not even needed (it can be any class). (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ 𝐵 = {∅} & ⊢ 𝐶 = ∅ & ⊢ 𝐷 = ∅ & ⊢ 𝑍 = V ⇒ ⊢ ¬ (𝑍 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷) | ||
Theorem | eliincex 45049* | Counterexample to show that the additional conditions in eliin 5000 and eliin2 45055 are actually needed. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ 𝐴 = V & ⊢ 𝐵 = ∅ ⇒ ⊢ ¬ (𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶) | ||
Theorem | eliinid 45050* | Membership in an indexed intersection implies membership in any intersected set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ ((𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ 𝐶) | ||
Theorem | abssf 45051 | Class abstraction in a subclass relationship. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ ({𝑥 ∣ 𝜑} ⊆ 𝐴 ↔ ∀𝑥(𝜑 → 𝑥 ∈ 𝐴)) | ||
Theorem | supxrubd 45052 | A member of a set of extended reals is less than or equal to the set's supremum. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ 𝑆 = sup(𝐴, ℝ*, < ) ⇒ ⊢ (𝜑 → 𝐵 ≤ 𝑆) | ||
Theorem | ssrabf 45053 | Subclass of a restricted class abstraction. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝐵 ⊆ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ (𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | ssrabdf 45054 | Subclass of a restricted class abstraction (deduction form). (Contributed by Glauco Siliprandi, 5-Jan-2025.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝜓) ⇒ ⊢ (𝜑 → 𝐵 ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓}) | ||
Theorem | eliin2 45055* | Membership in indexed intersection. See eliincex 45049 for a counterexample showing that the precondition 𝐵 ≠ ∅ cannot be simply dropped. eliin 5000 uses an alternative precondition (and it doesn't have a disjoint var constraint between 𝐵 and 𝑥; see eliin2f 45043). (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝐵 ≠ ∅ → (𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)) | ||
Theorem | ssrab2f 45056 | Subclass relation for a restricted class. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴 | ||
Theorem | restuni3 45057 | The underlying set of a subspace induced by the subspace operator ↾t. The result can be applied, for instance, to topologies and sigma-algebras. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ∪ (𝐴 ↾t 𝐵) = (∪ 𝐴 ∩ 𝐵)) | ||
Theorem | rabssf 45058 | Restricted class abstraction in a subclass relationship. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐵 ⇒ ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 ∈ 𝐵)) | ||
Theorem | eliuniin2 45059* | Indexed union of indexed intersections. See eliincex 45049 for a counterexample showing that the precondition 𝐶 ≠ ∅ cannot be simply dropped. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑥𝐶 & ⊢ 𝐴 = ∪ 𝑥 ∈ 𝐵 ∩ 𝑦 ∈ 𝐶 𝐷 ⇒ ⊢ (𝐶 ≠ ∅ → (𝑍 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷)) | ||
Theorem | restuni4 45060 | The underlying set of a subspace induced by the ↾t operator. The result can be applied, for instance, to topologies and sigma-algebras. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ⊆ ∪ 𝐴) ⇒ ⊢ (𝜑 → ∪ (𝐴 ↾t 𝐵) = 𝐵) | ||
Theorem | restuni6 45061 | The underlying set of a subspace topology. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ∪ (𝐴 ↾t 𝐵) = (∪ 𝐴 ∩ 𝐵)) | ||
Theorem | restuni5 45062 | The underlying set of a subspace induced by the ↾t operator. The result can be applied, for instance, to topologies and sigma-algebras. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑋) → 𝐴 = ∪ (𝐽 ↾t 𝐴)) | ||
Theorem | unirestss 45063 | The union of an elementwise intersection is a subset of the underlying set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ∪ (𝐴 ↾t 𝐵) ⊆ ∪ 𝐴) | ||
Theorem | iniin1 45064* | Indexed intersection of intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝐴 ≠ ∅ → (∩ 𝑥 ∈ 𝐴 𝐶 ∩ 𝐵) = ∩ 𝑥 ∈ 𝐴 (𝐶 ∩ 𝐵)) | ||
Theorem | iniin2 45065* | Indexed intersection of intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝐴 ≠ ∅ → (𝐵 ∩ ∩ 𝑥 ∈ 𝐴 𝐶) = ∩ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶)) | ||
Theorem | cbvrabv2 45066* | A more general version of cbvrabv 3443. Usage of this theorem is discouraged because it depends on ax-13 2374. Use of cbvrabv2w 45067 is preferred. (Contributed by Glauco Siliprandi, 23-Oct-2021.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐵 ∣ 𝜓} | ||
Theorem | cbvrabv2w 45067* | A more general version of cbvrabv 3443. Version of cbvrabv2 45066 with a disjoint variable condition, which does not require ax-13 2374. (Contributed by Glauco Siliprandi, 23-Oct-2021.) (Revised by GG, 14-Aug-2025.) |
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐵 ∣ 𝜓} | ||
Theorem | iinssiin 45068 | Subset implication for an indexed intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ ∩ 𝑥 ∈ 𝐴 𝐶) | ||
Theorem | eliind2 45069* | Membership in indexed intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶) | ||
Theorem | iinssd 45070* | Subset implication for an indexed intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝑥 = 𝑋 → 𝐵 = 𝐷) & ⊢ (𝜑 → 𝐷 ⊆ 𝐶) ⇒ ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶) | ||
Theorem | rabbida2 45071 | Equivalent wff's yield equal restricted class abstractions. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | iinexd 45072* | 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 45073 | Separation Scheme in terms of a restricted class abstraction. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝐴 & ⊢ 𝐴 ∈ 𝑉 ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V | ||
Theorem | rabbida3 45074 | Equivalent wff's yield equal restricted class abstractions. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒))) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | r19.36vf 45075 | Restricted quantifier version of one direction of 19.36 2227. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∃𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 → 𝜓)) | ||
Theorem | raleqd 45076 | Equality deduction for restricted universal quantifier. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | iinssf 45077 | Subset implication for an indexed intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝐶 ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶) | ||
Theorem | iinssdf 45078 | Subset implication for an indexed intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝑋 & ⊢ Ⅎ𝑥𝐶 & ⊢ Ⅎ𝑥𝐷 & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝑥 = 𝑋 → 𝐵 = 𝐷) & ⊢ (𝜑 → 𝐷 ⊆ 𝐶) ⇒ ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶) | ||
Theorem | resabs2i 45079 | Absorption law for restriction. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ ((𝐴 ↾ 𝐵) ↾ 𝐶) = (𝐴 ↾ 𝐵) | ||
Theorem | ssdf2 45080 | A sufficient condition for a subclass relationship. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | ||
Theorem | rabssd 45081 | Restricted class abstraction in a subclass relationship. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐵 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝜒) → 𝑥 ∈ 𝐵) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜒} ⊆ 𝐵) | ||
Theorem | rexnegd 45082 | Minus a real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → -𝑒𝐴 = -𝐴) | ||
Theorem | rexlimd3 45083 | * Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜒 & ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) | ||
Theorem | resabs1i 45084 | Absorption law for restriction. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ 𝐵 ⊆ 𝐶 ⇒ ⊢ ((𝐴 ↾ 𝐶) ↾ 𝐵) = (𝐴 ↾ 𝐵) | ||
Theorem | nel1nelin 45085 | Membership in an intersection implies membership in the first set. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (¬ 𝐴 ∈ 𝐵 → ¬ 𝐴 ∈ (𝐵 ∩ 𝐶)) | ||
Theorem | nel2nelin 45086 | Membership in an intersection implies membership in the second set. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (¬ 𝐴 ∈ 𝐶 → ¬ 𝐴 ∈ (𝐵 ∩ 𝐶)) | ||
Theorem | nel1nelini 45087 | Membership in an intersection implies membership in the first set. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ ¬ 𝐴 ∈ 𝐵 ⇒ ⊢ ¬ 𝐴 ∈ (𝐵 ∩ 𝐶) | ||
Theorem | nel2nelini 45088 | Membership in an intersection implies membership in the second set. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ ¬ 𝐴 ∈ 𝐶 ⇒ ⊢ ¬ 𝐴 ∈ (𝐵 ∩ 𝐶) | ||
Theorem | eliunid 45089* | Membership in indexed union. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵) → 𝐶 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) | ||
Theorem | reximdd 45090 | Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝜓) → 𝜒) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒) | ||
Theorem | inopnd 45091 | The intersection of two open sets of a topology is an open set. (Contributed by Glauco Siliprandi, 21-Dec-2024.) |
⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝐴 ∈ 𝐽) & ⊢ (𝜑 → 𝐵 ∈ 𝐽) ⇒ ⊢ (𝜑 → (𝐴 ∩ 𝐵) ∈ 𝐽) | ||
Theorem | ss2rabdf 45092 | Deduction of restricted abstraction subclass from implication. (Contributed by Glauco Siliprandi, 21-Dec-2024.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜒}) | ||
Theorem | restopn3 45093 | If 𝐴 is open, then 𝐴 is open in the restriction to itself. (Contributed by Glauco Siliprandi, 21-Dec-2024.) |
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽) → 𝐴 ∈ (𝐽 ↾t 𝐴)) | ||
Theorem | restopnssd 45094 | 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 45095 | A subset belongs in the space it generates via restriction. (Contributed by Glauco Siliprandi, 21-Dec-2024.) |
⊢ (𝜑 → 𝐽 ∈ 𝑉) & ⊢ (𝜑 → ∪ 𝐽 ∈ 𝐽) & ⊢ (𝜑 → 𝐴 ⊆ ∪ 𝐽) ⇒ ⊢ (𝜑 → 𝐴 ∈ (𝐽 ↾t 𝐴)) | ||
Theorem | toprestsubel 45096 | A subset is open in the topology it generates via restriction. (Contributed by Glauco Siliprandi, 21-Dec-2024.) |
⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝐴 ⊆ ∪ 𝐽) ⇒ ⊢ (𝜑 → 𝐴 ∈ (𝐽 ↾t 𝐴)) | ||
Theorem | rabidd 45097 | 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 45098 | Subset theorem for an indexed union. (Contributed by Glauco Siliprandi, 24-Jan-2025.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐶 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶) | ||
Theorem | iinss2d 45099 | Subset implication for an indexed intersection. (Contributed by Glauco Siliprandi, 24-Jan-2025.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐶) ⇒ ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶) | ||
Theorem | r19.3rzf 45100 | Restricted quantification of wff not containing quantified variable. (Contributed by Glauco Siliprandi, 24-Jan-2025.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝐴 ≠ ∅ → (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |