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