![]() |
Metamath
Proof Explorer Theorem List (p. 35 of 479) | < 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cbvreuvw 3401* | Change the bound variable of a restricted unique existential quantifier using implicit substitution. Version of cbvreuv 3428 with a disjoint variable condition, which requires fewer axioms. (Contributed by NM, 5-Apr-2004.) (Revised by Gino Giotto, 30-Sep-2024.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐴 𝜓) | ||
Theorem | moelOLD 3402* | Obsolete version of moel 3399 as of 23-Nov-2024. (Contributed by Thierry Arnoux, 26-Jul-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∃*𝑥 𝑥 ∈ 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 = 𝑦) | ||
Theorem | rmobida 3403 | Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 16-Jun-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | reubida 3404 | Formula-building rule for restricted existential quantifier (deduction form). (Contributed by Mario Carneiro, 19-Nov-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | rmobidvaOLD 3405* | Obsolete version of rmobidv 3394 as of 23-Nov-2024. (Contributed by NM, 16-Jun-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | cbvrmow 3406* | Change the bound variable of a restricted at-most-one quantifier using implicit substitution. Version of cbvrmo 3426 with a disjoint variable condition, which does not require ax-10 2138, ax-13 2372. (Contributed by NM, 16-Jun-2017.) Avoid ax-10 2138, ax-13 2372. (Revised by Gino Giotto, 23-May-2024.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvreuw 3407* | Change the bound variable of a restricted unique existential quantifier using implicit substitution. Version of cbvreu 3425 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by Mario Carneiro, 15-Oct-2016.) Avoid ax-13 2372. (Revised by Gino Giotto, 10-Jan-2024.) Avoid ax-10 2138. (Revised by Wolf Lammen, 10-Dec-2024.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐴 𝜓) | ||
Theorem | nfrmo1 3408 | The setvar 𝑥 is not free in ∃*𝑥 ∈ 𝐴𝜑. (Contributed by NM, 16-Jun-2017.) |
⊢ Ⅎ𝑥∃*𝑥 ∈ 𝐴 𝜑 | ||
Theorem | nfreu1 3409 | The setvar 𝑥 is not free in ∃!𝑥 ∈ 𝐴𝜑. (Contributed by NM, 19-Mar-1997.) |
⊢ Ⅎ𝑥∃!𝑥 ∈ 𝐴 𝜑 | ||
Theorem | nfrmow 3410* | Bound-variable hypothesis builder for restricted uniqueness. Version of nfrmo 3431 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by NM, 16-Jun-2017.) Avoid ax-13 2372. (Revised by Gino Giotto, 10-Jan-2024.) Avoid ax-9 2117, ax-ext 2704. (Revised by Wolf Lammen, 21-Nov-2024.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∃*𝑦 ∈ 𝐴 𝜑 | ||
Theorem | nfreuw 3411* | Bound-variable hypothesis builder for restricted unique existence. Version of nfreu 3432 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by NM, 30-Oct-2010.) Avoid ax-13 2372. (Revised by Gino Giotto, 10-Jan-2024.) Avoid ax-9 2117, ax-ext 2704. (Revised by Wolf Lammen, 21-Nov-2024.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∃!𝑦 ∈ 𝐴 𝜑 | ||
Theorem | cbvrmowOLD 3412* | Obsolete version of cbvrmow 3406 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 3413* | Obsolete version of cbvreuw 3407 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 3414* | Obsolete version of cbvreuvw 3401 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 3415* | Equality theorem for restricted at-most-one quantifier. (Contributed by Alexander van der Vekens, 17-Jun-2017.) Remove usage of ax-10 2138, ax-11 2155, and ax-12 2172. (Revised by Steven Nguyen, 30-Apr-2023.) Avoid ax-8 2109. (Revised by Wolf Lammen, 12-Mar-2025.) |
⊢ (𝐴 = 𝐵 → (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | reueq1 3416* | Equality theorem for restricted unique existential quantifier. (Contributed by NM, 5-Apr-2004.) Remove usage of ax-10 2138, ax-11 2155, and ax-12 2172. (Revised by Steven Nguyen, 30-Apr-2023.) Avoid ax-8 2109. (Revised by Wolf Lammen, 12-Mar-2025.) |
⊢ (𝐴 = 𝐵 → (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | rmoeq1OLD 3417* | Obsolete version of rmoeq1 3415 as of 12-Mar-2025. (Contributed by Alexander van der Vekens, 17-Jun-2017.) Remove usage of ax-10 2138, ax-11 2155, and ax-12 2172. (Revised by Steven Nguyen, 30-Apr-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 = 𝐵 → (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | reueq1OLD 3418* | Obsolete version of reueq1 3416 as of 12-Mar-2025. (Contributed by NM, 5-Apr-2004.) Remove usage of ax-10 2138, ax-11 2155, and ax-12 2172. (Revised by Steven Nguyen, 30-Apr-2023.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐴 = 𝐵 → (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | rmoeqd 3419* | Equality deduction for restricted at-most-one quantifier. (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 = 𝐵 → (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | reueqd 3420* | Equality deduction for restricted unique existential quantifier. (Contributed by NM, 5-Apr-2004.) |
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 = 𝐵 → (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | rmoeq1f 3421 | 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 3422 | 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 3423* | Obsolete version of nfreuw 3411 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 3424* | Obsolete version of nfrmow 3410 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 3425* | 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 2372. Use the weaker cbvreuw 3407 when possible. (Contributed by Mario Carneiro, 15-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvrmo 3426* | 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 2372. Use the weaker cbvrmow 3406, cbvrmovw 3400 when possible. (Contributed by NM, 16-Jun-2017.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvrmov 3427* | 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 2372. (Contributed by Alexander van der Vekens, 17-Jun-2017.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvreuv 3428* | Change the bound variable of a restricted unique existential quantifier using implicit substitution. See cbvreuvw 3401 for a version without ax-13 2372, but extra disjoint variables. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker cbvreuvw 3401 when possible. (Contributed by NM, 5-Apr-2004.) (Revised by Mario Carneiro, 15-Oct-2016.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐴 𝜓) | ||
Theorem | nfrmod 3429 | Deduction version of nfrmo 3431. Usage of this theorem is discouraged because it depends on ax-13 2372. (Contributed by NM, 17-Jun-2017.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∃*𝑦 ∈ 𝐴 𝜓) | ||
Theorem | nfreud 3430 | Deduction version of nfreu 3432. Usage of this theorem is discouraged because it depends on ax-13 2372. (Contributed by NM, 15-Feb-2013.) (Revised by Mario Carneiro, 8-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∃!𝑦 ∈ 𝐴 𝜓) | ||
Theorem | nfrmo 3431 | Bound-variable hypothesis builder for restricted uniqueness. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker nfrmow 3410 when possible. (Contributed by NM, 16-Jun-2017.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∃*𝑦 ∈ 𝐴 𝜑 | ||
Theorem | nfreu 3432 | Bound-variable hypothesis builder for restricted unique existence. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker nfreuw 3411 when possible. (Contributed by NM, 30-Oct-2010.) (Revised by Mario Carneiro, 8-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∃!𝑦 ∈ 𝐴 𝜑 | ||
Syntax | crab 3433 | Extend class notation to include the restricted class abstraction (class builder). |
class {𝑥 ∈ 𝐴 ∣ 𝜑} | ||
Definition | df-rab 3434 |
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 3063. (Contributed by NM, 22-Nov-1994.) |
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} | ||
Theorem | rabbidva2 3435* | Equivalent wff's yield equal restricted class abstractions. (Contributed by Thierry Arnoux, 4-Feb-2017.) |
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒))) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | rabbia2 3436 | Equivalent wff's yield equal restricted class abstractions. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒)) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒} | ||
Theorem | rabbiia 3437 | 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 3438 | Obsolete version of rabbiia 3437 as of 12-Jan-2025. (Contributed by NM, 22-May-1999.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓} | ||
Theorem | rabbii 3439 | Equivalent wff's correspond to equal restricted class abstractions. Inference form of rabbidv 3441. (Contributed by Peter Mazsa, 1-Nov-2019.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓} | ||
Theorem | rabbidva 3440* | 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 3441* | Equivalent wff's yield equal restricted class abstractions (deduction form). (Contributed by NM, 10-Feb-1995.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒}) | ||
Theorem | rabswap 3442 | Swap with a membership relation in a restricted class abstraction. (Contributed by NM, 4-Jul-2005.) |
⊢ {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} = {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝐴} | ||
Theorem | cbvrabv 3443* | 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 2155 and ax-13 2372. (Revised by Steven Nguyen, 4-Dec-2022.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓} | ||
Theorem | rabeqcda 3444* | When 𝜓 is always true in a context, a restricted class abstraction is equal to the restricting class. Deduction form of rabeqc 3445. (Contributed by Steven Nguyen, 7-Jun-2023.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = 𝐴) | ||
Theorem | rabeqc 3445* | 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 3446 | Equality theorem for restricted class abstractions. Inference form of rabeqf 3467. (Contributed by Glauco Siliprandi, 26-Jun-2021.) Avoid ax-10 2138, ax-11 2155, ax-12 2172. (Revised by Gino Giotto, 3-Jun-2024.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑} | ||
Theorem | rabeq 3447* | Equality theorem for restricted class abstractions. (Contributed by NM, 15-Oct-2003.) Avoid ax-10 2138, ax-11 2155, ax-12 2172. (Revised by Gino Giotto, 20-Aug-2023.) |
⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑}) | ||
Theorem | rabeqdv 3448* | Equality of restricted class abstractions. Deduction form of rabeq 3447. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓}) | ||
Theorem | rabeqbidva 3449* | Equality of restricted class abstractions. (Contributed by Mario Carneiro, 26-Jan-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | rabeqbidv 3450* | Equality of restricted class abstractions. (Contributed by Jeff Madsen, 1-Dec-2009.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | rabrabi 3451* | Abstract builder restricted to another restricted abstract builder with implicit substitution. (Contributed by AV, 2-Aug-2022.) Avoid ax-10 2138, ax-11 2155 and ax-12 2172. (Revised by Gino Giotto, 12-Oct-2024.) |
⊢ (𝑥 = 𝑦 → (𝜒 ↔ 𝜑)) ⇒ ⊢ {𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑} ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ (𝜒 ∧ 𝜓)} | ||
Theorem | nfrab1 3452 | The abstraction variable in a restricted class abstraction isn't free. (Contributed by NM, 19-Mar-1997.) |
⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 𝜑} | ||
Theorem | rabid 3453 | 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 3454 | Membership in a restricted abstraction, implication. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} → 𝑥 ∈ 𝐴) | ||
Theorem | reqabi 3455 | Inference from equality of a class variable and a restricted class abstraction. (Contributed by NM, 16-Feb-2004.) |
⊢ 𝐴 = {𝑥 ∈ 𝐵 ∣ 𝜑} ⇒ ⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐵 ∧ 𝜑)) | ||
Theorem | rabrab 3456 | Abstract builder restricted to another restricted abstract builder. (Contributed by Thierry Arnoux, 30-Aug-2017.) |
⊢ {𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)} | ||
Theorem | rabrabiOLD 3457* | Obsolete version of rabrabi 3451 as of 12-Oct-2024. (Contributed by AV, 2-Aug-2022.) Avoid ax-10 2138 and ax-11 2155. (Revised by Gino Giotto, 20-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜒 ↔ 𝜑)) ⇒ ⊢ {𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑} ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ (𝜒 ∧ 𝜓)} | ||
Theorem | rabbida4 3458 | Version of rabbidva2 3435 with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒))) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | rabbida 3459 | Equivalent wff's yield equal restricted class abstractions (deduction form). Version of rabbidva 3440 with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.) Avoid ax-10 2138, ax-11 2155. (Revised by Wolf Lammen, 14-Mar-2025.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒}) | ||
Theorem | rabbid 3460 | Version of rabbidv 3441 with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒}) | ||
Theorem | rabeqd 3461 | Deduction form of rabeq 3447. Note that contrary to rabeq 3447 it has no disjoint variable condition. (Contributed by BJ, 27-Apr-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓}) | ||
Theorem | rabeqbida 3462 | Version of rabeqbidva 3449 with two disjoint variable conditions removed and the third replaced by a nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | rabbi 3463 | Equivalent wff's correspond to equal restricted class abstractions. Closed theorem form of rabbii 3439. (Contributed by NM, 25-Nov-2013.) |
⊢ (∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝜒) ↔ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒}) | ||
Theorem | rabid2f 3464 | 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 3465* | 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 3466* | Obsolete version of rabid2 3465 as of 24-11-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 3467 | Equality theorem for restricted class abstractions, with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by NM, 7-Mar-2004.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑}) | ||
Theorem | cbvrabw 3468* | Rule to change the bound variable in a restricted class abstraction, using implicit substitution. Version of cbvrab 3474 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by Andrew Salmon, 11-Jul-2011.) Avoid ax-13 2372. (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓} | ||
Theorem | nfrabw 3469* | A variable not free in a wff remains so in a restricted class abstraction. Version of nfrab 3473 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by NM, 13-Oct-2003.) Avoid ax-13 2372. (Revised by Gino Giotto, 10-Jan-2024.) (Proof shortened by Wolf Lammen, 23-Nov-2024.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝜑} | ||
Theorem | nfrabwOLD 3470* | Obsolete version of nfrabw 3469 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 3471 | Obsolete version of rabbida 3459 as of 14-Mar-2025. (Contributed by BJ, 27-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒}) | ||
Theorem | rabeqiOLD 3472 | Obsolete version of rabeqi 3446 as of 3-Jun-2024. (Contributed by Glauco Siliprandi, 26-Jun-2021.) Avoid ax-10 2138 and ax-11 2155. (Revised by Gino Giotto, 20-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑} | ||
Theorem | nfrab 3473 | 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 2372. Use the weaker nfrabw 3469 when possible. (Contributed by NM, 13-Oct-2003.) (Revised by Mario Carneiro, 9-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝜑} | ||
Theorem | cbvrab 3474 | 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 2372. Use the weaker cbvrabw 3468 when possible. (Contributed by Andrew Salmon, 11-Jul-2011.) (Revised by Mario Carneiro, 9-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓} | ||
Syntax | cvv 3475 | Extend class notation to include the universal class symbol. |
class V | ||
Theorem | vjust 3476 | Justification theorem for df-v 3477. (Contributed by Rodolfo Medina, 27-Apr-2010.) |
⊢ {𝑥 ∣ 𝑥 = 𝑥} = {𝑦 ∣ 𝑦 = 𝑦} | ||
Definition | df-v 3477 |
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 5316
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 3488 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 3488. See dfv2 3478 for an alternate definition. (Contributed by NM, 26-May-1993.) |
⊢ V = {𝑥 ∣ 𝑥 = 𝑥} | ||
Theorem | dfv2 3478 | Alternate definition of the universal class (see df-v 3477). (Contributed by BJ, 30-Nov-2019.) |
⊢ V = {𝑥 ∣ ⊤} | ||
Theorem | vex 3479 | All setvar variables are sets (see isset 3488). Theorem 6.8 of [Quine] p. 43. A shorter proof is possible from eleq2i 2826 but it uses more axioms. (Contributed by NM, 26-May-1993.) Remove use of ax-12 2172. (Revised by SN, 28-Aug-2023.) (Proof shortened by BJ, 4-Sep-2024.) |
⊢ 𝑥 ∈ V | ||
Theorem | vexOLD 3480 | Obsolete version of vex 3479 as of 4-Sep-2024. (Contributed by NM, 26-May-1993.) Remove use of ax-12 2172. (Revised by SN, 28-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝑥 ∈ V | ||
Theorem | elv 3481 | If a proposition is implied by 𝑥 ∈ V (which is true, see vex 3479), then it is true. (Contributed by Peter Mazsa, 13-Oct-2018.) |
⊢ (𝑥 ∈ V → 𝜑) ⇒ ⊢ 𝜑 | ||
Theorem | elvd 3482 | If a proposition is implied by 𝑥 ∈ V (which is true, see vex 3479) and another antecedent, then it is implied by that other antecedent. Deduction associated with elv 3481. (Contributed by Peter Mazsa, 23-Oct-2018.) |
⊢ ((𝜑 ∧ 𝑥 ∈ V) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | el2v 3483 | If a proposition is implied by 𝑥 ∈ V and 𝑦 ∈ V (which is true, see vex 3479), then it is true. (Contributed by Peter Mazsa, 13-Oct-2018.) |
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → 𝜑) ⇒ ⊢ 𝜑 | ||
Theorem | eqv 3484* | The universe contains every set. (Contributed by NM, 11-Sep-2006.) Remove dependency on ax-10 2138, ax-11 2155, ax-13 2372. (Revised by BJ, 10-Aug-2022.) |
⊢ (𝐴 = V ↔ ∀𝑥 𝑥 ∈ 𝐴) | ||
Theorem | eqvf 3485 | The universe contains every set. (Contributed by BJ, 15-Jul-2021.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝐴 = V ↔ ∀𝑥 𝑥 ∈ 𝐴) | ||
Theorem | abv 3486 | 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 35786) requires fewer axioms. (Contributed by BJ, 19-Mar-2021.) Avoid df-clel 2811, ax-8 2109. (Revised by Gino Giotto, 30-Aug-2024.) (Proof shortened by BJ, 30-Aug-2024.) |
⊢ ({𝑥 ∣ 𝜑} = V ↔ ∀𝑥𝜑) | ||
Theorem | abvALT 3487 | Alternate proof of abv 3486, shorter but using more axioms. (Contributed by BJ, 19-Mar-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ({𝑥 ∣ 𝜑} = V ↔ ∀𝑥𝜑) | ||
Theorem | isset 3488* |
Two ways to express that "𝐴 is a set": A class 𝐴 is a
member
of the universal class V (see df-v 3477)
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 7731. 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 7730 compared with uniex 7731). That this is more general is seen either by substitution (when the variable 𝑉 has no other occurrences), or by elex 3493. (Contributed by NM, 26-May-1993.) |
⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴) | ||
Theorem | issetf 3489 | A version of isset 3488 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 3490* | 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 3491* | A way to say "𝐴 is a set" (inference form). (Contributed by NM, 21-Jun-1993.) |
⊢ ∃𝑥 𝑥 = 𝐴 ⇒ ⊢ 𝐴 ∈ V | ||
Theorem | eqvisset 3492 | A class equal to a variable is a set. Note the absence of disjoint variable condition, contrary to isset 3488 and issetri 3491. (Contributed by BJ, 27-Apr-2019.) |
⊢ (𝑥 = 𝐴 → 𝐴 ∈ V) | ||
Theorem | elex 3493 | 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 3494 | If a class is a member of another class, then it is a set. Inference associated with elex 3493. (Contributed by NM, 11-Jun-1994.) |
⊢ 𝐴 ∈ 𝐵 ⇒ ⊢ 𝐴 ∈ V | ||
Theorem | elexd 3495 | If a class is a member of another class, then it is a set. Deduction associated with elex 3493. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐴 ∈ V) | ||
Theorem | elex2OLD 3496* | Obsolete version of elex2 2813 as of 30-Nov-2024. (Contributed by Alan Sare, 25-Sep-2011.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵) | ||
Theorem | elex22 3497* | If two classes each contain another class, then both contain some set. (Contributed by Alan Sare, 24-Oct-2011.) |
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)) | ||
Theorem | prcnel 3498 | 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 3499 | A universal quantifier restricted to the universe is unrestricted. (Contributed by NM, 26-Mar-2004.) |
⊢ (∀𝑥 ∈ V 𝜑 ↔ ∀𝑥𝜑) | ||
Theorem | rexv 3500 | An existential quantifier restricted to the universe is unrestricted. (Contributed by NM, 26-Mar-2004.) |
⊢ (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥𝜑) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |