![]() |
Metamath
Proof Explorer Theorem List (p. 35 of 480) | < 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-30439) |
![]() (30440-31962) |
![]() (31963-47940) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rmobida 3401 | Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 16-Jun-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | reubida 3402 | Formula-building rule for restricted existential quantifier (deduction form). (Contributed by Mario Carneiro, 19-Nov-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | rmobidvaOLD 3403* | Obsolete version of rmobidv 3392 as of 23-Nov-2024. (Contributed by NM, 16-Jun-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | cbvrmow 3404* | Change the bound variable of a restricted at-most-one quantifier using implicit substitution. Version of cbvrmo 3424 with a disjoint variable condition, which does not require ax-10 2136, ax-13 2370. (Contributed by NM, 16-Jun-2017.) Avoid ax-10 2136, ax-13 2370. (Revised by Gino Giotto, 23-May-2024.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvreuw 3405* | Change the bound variable of a restricted unique existential quantifier using implicit substitution. Version of cbvreu 3423 with a disjoint variable condition, which does not require ax-13 2370. (Contributed by Mario Carneiro, 15-Oct-2016.) Avoid ax-13 2370. (Revised by Gino Giotto, 10-Jan-2024.) Avoid ax-10 2136. (Revised by Wolf Lammen, 10-Dec-2024.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐴 𝜓) | ||
Theorem | nfrmo1 3406 | The setvar 𝑥 is not free in ∃*𝑥 ∈ 𝐴𝜑. (Contributed by NM, 16-Jun-2017.) |
⊢ Ⅎ𝑥∃*𝑥 ∈ 𝐴 𝜑 | ||
Theorem | nfreu1 3407 | The setvar 𝑥 is not free in ∃!𝑥 ∈ 𝐴𝜑. (Contributed by NM, 19-Mar-1997.) |
⊢ Ⅎ𝑥∃!𝑥 ∈ 𝐴 𝜑 | ||
Theorem | nfrmow 3408* | Bound-variable hypothesis builder for restricted uniqueness. Version of nfrmo 3429 with a disjoint variable condition, which does not require ax-13 2370. (Contributed by NM, 16-Jun-2017.) Avoid ax-13 2370. (Revised by Gino Giotto, 10-Jan-2024.) Avoid ax-9 2115, ax-ext 2702. (Revised by Wolf Lammen, 21-Nov-2024.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∃*𝑦 ∈ 𝐴 𝜑 | ||
Theorem | nfreuw 3409* | Bound-variable hypothesis builder for restricted unique existence. Version of nfreu 3430 with a disjoint variable condition, which does not require ax-13 2370. (Contributed by NM, 30-Oct-2010.) Avoid ax-13 2370. (Revised by Gino Giotto, 10-Jan-2024.) Avoid ax-9 2115, ax-ext 2702. (Revised by Wolf Lammen, 21-Nov-2024.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∃!𝑦 ∈ 𝐴 𝜑 | ||
Theorem | cbvrmowOLD 3410* | Obsolete version of cbvrmow 3404 as of 23-May-2024. (Contributed by NM, 16-Jun-2017.) (Revised by Gino Giotto, 10-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvreuwOLD 3411* | Obsolete version of cbvreuw 3405 as of 10-Dec-2024. (Contributed by Mario Carneiro, 15-Oct-2016.) (Revised by Gino Giotto, 10-Jan-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvreuvwOLD 3412* | Obsolete version of cbvreuvw 3399 as of 30-Sep-2024. (Contributed by NM, 5-Apr-2004.) (Revised by Gino Giotto, 10-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐴 𝜓) | ||
Theorem | rmoeq1 3413* | Equality theorem for restricted at-most-one quantifier. (Contributed by Alexander van der Vekens, 17-Jun-2017.) Remove usage of ax-10 2136, ax-11 2153, and ax-12 2170. (Revised by Steven Nguyen, 30-Apr-2023.) Avoid ax-8 2107. (Revised by Wolf Lammen, 12-Mar-2025.) |
⊢ (𝐴 = 𝐵 → (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | reueq1 3414* | Equality theorem for restricted unique existential quantifier. (Contributed by NM, 5-Apr-2004.) Remove usage of ax-10 2136, ax-11 2153, and ax-12 2170. (Revised by Steven Nguyen, 30-Apr-2023.) Avoid ax-8 2107. (Revised by Wolf Lammen, 12-Mar-2025.) |
⊢ (𝐴 = 𝐵 → (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | rmoeq1OLD 3415* | Obsolete version of rmoeq1 3413 as of 12-Mar-2025. (Contributed by Alexander van der Vekens, 17-Jun-2017.) Remove usage of ax-10 2136, ax-11 2153, and ax-12 2170. (Revised by Steven Nguyen, 30-Apr-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 = 𝐵 → (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | reueq1OLD 3416* | Obsolete version of reueq1 3414 as of 12-Mar-2025. (Contributed by NM, 5-Apr-2004.) Remove usage of ax-10 2136, ax-11 2153, and ax-12 2170. (Revised by Steven Nguyen, 30-Apr-2023.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐴 = 𝐵 → (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | rmoeqd 3417* | Equality deduction for restricted at-most-one quantifier. (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 = 𝐵 → (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | reueqd 3418* | Equality deduction for restricted unique existential quantifier. (Contributed by NM, 5-Apr-2004.) |
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 = 𝐵 → (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | rmoeq1f 3419 | Equality theorem for restricted at-most-one quantifier, with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 = 𝐵 → (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | reueq1f 3420 | Equality theorem for restricted unique existential quantifier, with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by NM, 5-Apr-2004.) (Revised by Andrew Salmon, 11-Jul-2011.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 = 𝐵 → (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | nfreuwOLD 3421* | Obsolete version of nfreuw 3409 as of 21-Nov-2024. (Contributed by NM, 30-Oct-2010.) (Revised by Gino Giotto, 10-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∃!𝑦 ∈ 𝐴 𝜑 | ||
Theorem | nfrmowOLD 3422* | Obsolete version of nfrmow 3408 as of 21-Nov-2024. (Contributed by NM, 16-Jun-2017.) (Revised by Gino Giotto, 10-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∃*𝑦 ∈ 𝐴 𝜑 | ||
Theorem | cbvreu 3423* | Change the bound variable of a restricted unique existential quantifier using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2370. Use the weaker cbvreuw 3405 when possible. (Contributed by Mario Carneiro, 15-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvrmo 3424* | Change the bound variable of a restricted at-most-one quantifier using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2370. Use the weaker cbvrmow 3404, cbvrmovw 3398 when possible. (Contributed by NM, 16-Jun-2017.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvrmov 3425* | Change the bound variable of a restricted at-most-one quantifier using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2370. (Contributed by Alexander van der Vekens, 17-Jun-2017.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvreuv 3426* | Change the bound variable of a restricted unique existential quantifier using implicit substitution. See cbvreuvw 3399 for a version without ax-13 2370, but extra disjoint variables. Usage of this theorem is discouraged because it depends on ax-13 2370. Use the weaker cbvreuvw 3399 when possible. (Contributed by NM, 5-Apr-2004.) (Revised by Mario Carneiro, 15-Oct-2016.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐴 𝜓) | ||
Theorem | nfrmod 3427 | Deduction version of nfrmo 3429. Usage of this theorem is discouraged because it depends on ax-13 2370. (Contributed by NM, 17-Jun-2017.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∃*𝑦 ∈ 𝐴 𝜓) | ||
Theorem | nfreud 3428 | Deduction version of nfreu 3430. Usage of this theorem is discouraged because it depends on ax-13 2370. (Contributed by NM, 15-Feb-2013.) (Revised by Mario Carneiro, 8-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∃!𝑦 ∈ 𝐴 𝜓) | ||
Theorem | nfrmo 3429 | Bound-variable hypothesis builder for restricted uniqueness. Usage of this theorem is discouraged because it depends on ax-13 2370. Use the weaker nfrmow 3408 when possible. (Contributed by NM, 16-Jun-2017.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∃*𝑦 ∈ 𝐴 𝜑 | ||
Theorem | nfreu 3430 | Bound-variable hypothesis builder for restricted unique existence. Usage of this theorem is discouraged because it depends on ax-13 2370. Use the weaker nfreuw 3409 when possible. (Contributed by NM, 30-Oct-2010.) (Revised by Mario Carneiro, 8-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∃!𝑦 ∈ 𝐴 𝜑 | ||
Syntax | crab 3431 | Extend class notation to include the restricted class abstraction (class builder). |
class {𝑥 ∈ 𝐴 ∣ 𝜑} | ||
Definition | df-rab 3432 |
Define a restricted class abstraction (class builder): {𝑥 ∈ 𝐴 ∣ 𝜑}
is the class of all sets 𝑥 in 𝐴 such that 𝜑(𝑥) is true.
Definition of [TakeutiZaring] p.
20.
For the interpretation given in the previous paragraph to be correct, we need to assume Ⅎ𝑥𝐴, which is the case as soon as 𝑥 and 𝐴 are disjoint, which is generally the case. If 𝐴 were to depend on 𝑥, then the interpretation would be less obvious (think of the two extreme cases 𝐴 = {𝑥} and 𝐴 = 𝑥, for instance). See also df-ral 3061. (Contributed by NM, 22-Nov-1994.) |
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} | ||
Theorem | rabbidva2 3433* | Equivalent wff's yield equal restricted class abstractions. (Contributed by Thierry Arnoux, 4-Feb-2017.) |
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒))) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | rabbia2 3434 | Equivalent wff's yield equal restricted class abstractions. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒)) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒} | ||
Theorem | rabbiia 3435 | Equivalent formulas yield equal restricted class abstractions (inference form). (Contributed by NM, 22-May-1999.) (Proof shortened by Wolf Lammen, 12-Jan-2025.) |
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓} | ||
Theorem | rabbiiaOLD 3436 | Obsolete version of rabbiia 3435 as of 12-Jan-2025. (Contributed by NM, 22-May-1999.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓} | ||
Theorem | rabbii 3437 | Equivalent wff's correspond to equal restricted class abstractions. Inference form of rabbidv 3439. (Contributed by Peter Mazsa, 1-Nov-2019.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓} | ||
Theorem | rabbidva 3438* | Equivalent wff's yield equal restricted class abstractions (deduction form). (Contributed by NM, 28-Nov-2003.) (Proof shortened by SN, 3-Dec-2023.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒}) | ||
Theorem | rabbidv 3439* | Equivalent wff's yield equal restricted class abstractions (deduction form). (Contributed by NM, 10-Feb-1995.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒}) | ||
Theorem | rabswap 3440 | Swap with a membership relation in a restricted class abstraction. (Contributed by NM, 4-Jul-2005.) |
⊢ {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} = {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝐴} | ||
Theorem | cbvrabv 3441* | Rule to change the bound variable in a restricted class abstraction, using implicit substitution. (Contributed by NM, 26-May-1999.) Require 𝑥, 𝑦 be disjoint to avoid ax-11 2153 and ax-13 2370. (Revised by Steven Nguyen, 4-Dec-2022.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓} | ||
Theorem | rabeqcda 3442* | When 𝜓 is always true in a context, a restricted class abstraction is equal to the restricting class. Deduction form of rabeqc 3443. (Contributed by Steven Nguyen, 7-Jun-2023.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = 𝐴) | ||
Theorem | rabeqc 3443* | A restricted class abstraction equals the restricting class if its condition follows from the membership of the free setvar variable in the restricting class. (Contributed by AV, 20-Apr-2022.) (Proof shortened by SN, 15-Jan-2025.) |
⊢ (𝑥 ∈ 𝐴 → 𝜑) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = 𝐴 | ||
Theorem | rabeqi 3444 | Equality theorem for restricted class abstractions. Inference form of rabeqf 3465. (Contributed by Glauco Siliprandi, 26-Jun-2021.) Avoid ax-10 2136, ax-11 2153, ax-12 2170. (Revised by Gino Giotto, 3-Jun-2024.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑} | ||
Theorem | rabeq 3445* | Equality theorem for restricted class abstractions. (Contributed by NM, 15-Oct-2003.) Avoid ax-10 2136, ax-11 2153, ax-12 2170. (Revised by Gino Giotto, 20-Aug-2023.) |
⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑}) | ||
Theorem | rabeqdv 3446* | Equality of restricted class abstractions. Deduction form of rabeq 3445. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓}) | ||
Theorem | rabeqbidva 3447* | Equality of restricted class abstractions. (Contributed by Mario Carneiro, 26-Jan-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | rabeqbidv 3448* | Equality of restricted class abstractions. (Contributed by Jeff Madsen, 1-Dec-2009.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | rabrabi 3449* | Abstract builder restricted to another restricted abstract builder with implicit substitution. (Contributed by AV, 2-Aug-2022.) Avoid ax-10 2136, ax-11 2153 and ax-12 2170. (Revised by Gino Giotto, 12-Oct-2024.) |
⊢ (𝑥 = 𝑦 → (𝜒 ↔ 𝜑)) ⇒ ⊢ {𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑} ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ (𝜒 ∧ 𝜓)} | ||
Theorem | nfrab1 3450 | The abstraction variable in a restricted class abstraction isn't free. (Contributed by NM, 19-Mar-1997.) |
⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 𝜑} | ||
Theorem | rabid 3451 | An "identity" law of concretion for restricted abstraction. Special case of Definition 2.1 of [Quine] p. 16. (Contributed by NM, 9-Oct-2003.) |
⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ (𝑥 ∈ 𝐴 ∧ 𝜑)) | ||
Theorem | rabidim1 3452 | Membership in a restricted abstraction, implication. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} → 𝑥 ∈ 𝐴) | ||
Theorem | reqabi 3453 | Inference from equality of a class variable and a restricted class abstraction. (Contributed by NM, 16-Feb-2004.) |
⊢ 𝐴 = {𝑥 ∈ 𝐵 ∣ 𝜑} ⇒ ⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐵 ∧ 𝜑)) | ||
Theorem | rabrab 3454 | Abstract builder restricted to another restricted abstract builder. (Contributed by Thierry Arnoux, 30-Aug-2017.) |
⊢ {𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)} | ||
Theorem | rabrabiOLD 3455* | Obsolete version of rabrabi 3449 as of 12-Oct-2024. (Contributed by AV, 2-Aug-2022.) Avoid ax-10 2136 and ax-11 2153. (Revised by Gino Giotto, 20-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜒 ↔ 𝜑)) ⇒ ⊢ {𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑} ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ (𝜒 ∧ 𝜓)} | ||
Theorem | rabbida4 3456 | Version of rabbidva2 3433 with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒))) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | rabbida 3457 | Equivalent wff's yield equal restricted class abstractions (deduction form). Version of rabbidva 3438 with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.) Avoid ax-10 2136, ax-11 2153. (Revised by Wolf Lammen, 14-Mar-2025.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒}) | ||
Theorem | rabbid 3458 | Version of rabbidv 3439 with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒}) | ||
Theorem | rabeqd 3459 | Deduction form of rabeq 3445. Note that contrary to rabeq 3445 it has no disjoint variable condition. (Contributed by BJ, 27-Apr-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓}) | ||
Theorem | rabeqbida 3460 | Version of rabeqbidva 3447 with two disjoint variable conditions removed and the third replaced by a nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | rabbi 3461 | Equivalent wff's correspond to equal restricted class abstractions. Closed theorem form of rabbii 3437. (Contributed by NM, 25-Nov-2013.) |
⊢ (∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝜒) ↔ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒}) | ||
Theorem | rabid2f 3462 | An "identity" law for restricted class abstraction. (Contributed by NM, 9-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Revised by Thierry Arnoux, 13-Mar-2017.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rabid2 3463* | An "identity" law for restricted class abstraction. (Contributed by NM, 9-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2024.) |
⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rabid2OLD 3464* | Obsolete version of rabid2 3463 as of 24-Nov-2024. (Contributed by NM, 9-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rabeqf 3465 | Equality theorem for restricted class abstractions, with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by NM, 7-Mar-2004.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑}) | ||
Theorem | cbvrabw 3466* | Rule to change the bound variable in a restricted class abstraction, using implicit substitution. Version of cbvrab 3472 with a disjoint variable condition, which does not require ax-13 2370. (Contributed by Andrew Salmon, 11-Jul-2011.) Avoid ax-13 2370. (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓} | ||
Theorem | nfrabw 3467* | A variable not free in a wff remains so in a restricted class abstraction. Version of nfrab 3471 with a disjoint variable condition, which does not require ax-13 2370. (Contributed by NM, 13-Oct-2003.) Avoid ax-13 2370. (Revised by Gino Giotto, 10-Jan-2024.) (Proof shortened by Wolf Lammen, 23-Nov-2024.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝜑} | ||
Theorem | nfrabwOLD 3468* | Obsolete version of nfrabw 3467 as of 23-Nov2024. (Contributed by NM, 13-Oct-2003.) (Revised by Gino Giotto, 10-Jan-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝜑} | ||
Theorem | rabbidaOLD 3469 | Obsolete version of rabbida 3457 as of 14-Mar-2025. (Contributed by BJ, 27-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒}) | ||
Theorem | rabeqiOLD 3470 | Obsolete version of rabeqi 3444 as of 3-Jun-2024. (Contributed by Glauco Siliprandi, 26-Jun-2021.) Avoid ax-10 2136 and ax-11 2153. (Revised by Gino Giotto, 20-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑} | ||
Theorem | nfrab 3471 | A variable not free in a wff remains so in a restricted class abstraction. Usage of this theorem is discouraged because it depends on ax-13 2370. Use the weaker nfrabw 3467 when possible. (Contributed by NM, 13-Oct-2003.) (Revised by Mario Carneiro, 9-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝜑} | ||
Theorem | cbvrab 3472 | Rule to change the bound variable in a restricted class abstraction, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2370. Use the weaker cbvrabw 3466 when possible. (Contributed by Andrew Salmon, 11-Jul-2011.) (Revised by Mario Carneiro, 9-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓} | ||
Syntax | cvv 3473 | Extend class notation to include the universal class symbol. |
class V | ||
Theorem | vjust 3474 | Justification theorem for df-v 3475. (Contributed by Rodolfo Medina, 27-Apr-2010.) |
⊢ {𝑥 ∣ 𝑥 = 𝑥} = {𝑦 ∣ 𝑦 = 𝑦} | ||
Definition | df-v 3475 |
Define the universal class. Definition 5.20 of [TakeutiZaring] p. 21.
Also Definition 2.9 of [Quine] p. 19. The
class V can be described
as the "class of all sets"; vprc 5315
proves that V is not itself a set
in ZF. We will frequently use the expression 𝐴 ∈ V as a short way
to
say "𝐴 is a set", and isset 3486 proves that this expression has the
same meaning as ∃𝑥𝑥 = 𝐴.
In well-founded set theories without urelements, like ZF, the class V is equal to the von Neumann universe. However, the letter "V" does not stand for "von Neumann". The letter "V" was used earlier by Peano in 1889 for the universe of sets, where the letter V is derived from the Latin word "Verum", referring to the true truth constant 𝑇. Peano's notation V was adopted by Whitehead and Russell in Principia Mathematica for the class of all sets in 1910. The class constant V is the first class constant introduced in this database. As a constant, as opposed to a variable, it cannot be substituted with anything, and in particular it is not part of any disjoint variable condition. For a general discussion of the theory of classes, see mmset.html#class 3486. See dfv2 3476 for an alternate definition. (Contributed by NM, 26-May-1993.) |
⊢ V = {𝑥 ∣ 𝑥 = 𝑥} | ||
Theorem | dfv2 3476 | Alternate definition of the universal class (see df-v 3475). (Contributed by BJ, 30-Nov-2019.) |
⊢ V = {𝑥 ∣ ⊤} | ||
Theorem | vex 3477 | All setvar variables are sets (see isset 3486). Theorem 6.8 of [Quine] p. 43. A shorter proof is possible from eleq2i 2824 but it uses more axioms. (Contributed by NM, 26-May-1993.) Remove use of ax-12 2170. (Revised by SN, 28-Aug-2023.) (Proof shortened by BJ, 4-Sep-2024.) |
⊢ 𝑥 ∈ V | ||
Theorem | vexOLD 3478 | Obsolete version of vex 3477 as of 4-Sep-2024. (Contributed by NM, 26-May-1993.) Remove use of ax-12 2170. (Revised by SN, 28-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝑥 ∈ V | ||
Theorem | elv 3479 | If a proposition is implied by 𝑥 ∈ V (which is true, see vex 3477), then it is true. (Contributed by Peter Mazsa, 13-Oct-2018.) |
⊢ (𝑥 ∈ V → 𝜑) ⇒ ⊢ 𝜑 | ||
Theorem | elvd 3480 | If a proposition is implied by 𝑥 ∈ V (which is true, see vex 3477) and another antecedent, then it is implied by that other antecedent. Deduction associated with elv 3479. (Contributed by Peter Mazsa, 23-Oct-2018.) |
⊢ ((𝜑 ∧ 𝑥 ∈ V) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | el2v 3481 | If a proposition is implied by 𝑥 ∈ V and 𝑦 ∈ V (which is true, see vex 3477), then it is true. (Contributed by Peter Mazsa, 13-Oct-2018.) |
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → 𝜑) ⇒ ⊢ 𝜑 | ||
Theorem | eqv 3482* | The universe contains every set. (Contributed by NM, 11-Sep-2006.) Remove dependency on ax-10 2136, ax-11 2153, ax-13 2370. (Revised by BJ, 10-Aug-2022.) |
⊢ (𝐴 = V ↔ ∀𝑥 𝑥 ∈ 𝐴) | ||
Theorem | eqvf 3483 | The universe contains every set. (Contributed by BJ, 15-Jul-2021.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝐴 = V ↔ ∀𝑥 𝑥 ∈ 𝐴) | ||
Theorem | abv 3484 | The class of sets verifying a property is the universal class if and only if that property is a tautology. The reverse implication (bj-abv 36090) requires fewer axioms. (Contributed by BJ, 19-Mar-2021.) Avoid df-clel 2809, ax-8 2107. (Revised by Gino Giotto, 30-Aug-2024.) (Proof shortened by BJ, 30-Aug-2024.) |
⊢ ({𝑥 ∣ 𝜑} = V ↔ ∀𝑥𝜑) | ||
Theorem | abvALT 3485 | Alternate proof of abv 3484, shorter but using more axioms. (Contributed by BJ, 19-Mar-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ({𝑥 ∣ 𝜑} = V ↔ ∀𝑥𝜑) | ||
Theorem | isset 3486* |
Two ways to express that "𝐴 is a set": A class 𝐴 is a
member
of the universal class V (see df-v 3475)
if and only if the class
𝐴 exists (i.e., there exists some set
𝑥
equal to class 𝐴).
Theorem 6.9 of [Quine] p. 43.
A class 𝐴 which is not a set is called a proper class. Conventions: We will often use the expression "𝐴 ∈ V " to mean "𝐴 is a set", for example in uniex 7735. To make some theorems more readily applicable, we will also use the more general expression 𝐴 ∈ 𝑉 instead of 𝐴 ∈ V to mean "𝐴 is a set", typically in an antecedent, or in a hypothesis for theorems in deduction form (see for instance uniexg 7734 compared with uniex 7735). That this is more general is seen either by substitution (when the variable 𝑉 has no other occurrences), or by elex 3492. (Contributed by NM, 26-May-1993.) |
⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴) | ||
Theorem | issetft 3487 | Closed theorem form of isset 3486 that does not require 𝑥 and 𝐴 to be distinct. Extracted from the proof of vtoclgft 3540. (Contributed by Wolf Lammen, 9-Apr-2025.) |
⊢ (Ⅎ𝑥𝐴 → (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)) | ||
Theorem | issetf 3488 | A version of isset 3486 that does not require 𝑥 and 𝐴 to be distinct. (Contributed by Andrew Salmon, 6-Jun-2011.) (Revised by Mario Carneiro, 10-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴) | ||
Theorem | isseti 3489* | A way to say "𝐴 is a set" (inference form). (Contributed by NM, 24-Jun-1993.) Remove dependencies on axioms. (Revised by BJ, 13-Jul-2019.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ∃𝑥 𝑥 = 𝐴 | ||
Theorem | issetri 3490* | A way to say "𝐴 is a set" (inference form). (Contributed by NM, 21-Jun-1993.) |
⊢ ∃𝑥 𝑥 = 𝐴 ⇒ ⊢ 𝐴 ∈ V | ||
Theorem | eqvisset 3491 | A class equal to a variable is a set. Note the absence of disjoint variable condition, contrary to isset 3486 and issetri 3490. (Contributed by BJ, 27-Apr-2019.) |
⊢ (𝑥 = 𝐴 → 𝐴 ∈ V) | ||
Theorem | elex 3492 | If a class is a member of another class, then it is a set. Theorem 6.12 of [Quine] p. 44. (Contributed by NM, 26-May-1993.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) |
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V) | ||
Theorem | elexi 3493 | If a class is a member of another class, then it is a set. Inference associated with elex 3492. (Contributed by NM, 11-Jun-1994.) |
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ 𝐴 ∈ V | ||
Theorem | elexd 3494 | If a class is a member of another class, then it is a set. Deduction associated with elex 3492. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐴 ∈ V) | ||
Theorem | elex2OLD 3495* | Obsolete version of elex2 2811 as of 30-Nov-2024. (Contributed by Alan Sare, 25-Sep-2011.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵) | ||
Theorem | elex22 3496* | If two classes each contain another class, then both contain some set. (Contributed by Alan Sare, 24-Oct-2011.) |
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)) | ||
Theorem | prcnel 3497 | A proper class doesn't belong to any class. (Contributed by Glauco Siliprandi, 17-Aug-2020.) (Proof shortened by AV, 14-Nov-2020.) |
⊢ (¬ 𝐴 ∈ V → ¬ 𝐴 ∈ 𝑉) | ||
Theorem | ralv 3498 | A universal quantifier restricted to the universe is unrestricted. (Contributed by NM, 26-Mar-2004.) |
⊢ (∀𝑥 ∈ V 𝜑 ↔ ∀𝑥𝜑) | ||
Theorem | rexv 3499 | An existential quantifier restricted to the universe is unrestricted. (Contributed by NM, 26-Mar-2004.) |
⊢ (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥𝜑) | ||
Theorem | reuv 3500 | A unique existential quantifier restricted to the universe is unrestricted. (Contributed by NM, 1-Nov-2010.) |
⊢ (∃!𝑥 ∈ V 𝜑 ↔ ∃!𝑥𝜑) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |