Home | Metamath
Proof Explorer Theorem List (p. 35 of 449) | < 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: | Metamath Proof Explorer
(1-28689) |
Hilbert Space Explorer
(28690-30212) |
Users' Mathboxes
(30213-44900) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | raleqbidv 3401* | Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.) Remove usage of ax-10 2141, ax-11 2157, and ax-12 2173 and reduce distinct variable conditions. (Revised by Steven Nguyen, 30-Apr-2023.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) | ||
Theorem | rexeqbidv 3402* | Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.) Remove usage of ax-10 2141, ax-11 2157, and ax-12 2173 and reduce distinct variable conditions. (Revised by Steven Nguyen, 30-Apr-2023.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒)) | ||
Theorem | raleqbi1dv 3403* | Equality deduction for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.) (Proof shortened by Steven Nguyen, 5-May-2023.) |
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | rexeqbi1dv 3404* | Equality deduction for restricted existential quantifier. (Contributed by NM, 18-Mar-1997.) (Proof shortened by Steven Nguyen, 5-May-2023.) |
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | raleq 3405* | Equality theorem for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.) Remove usage of ax-10 2141, ax-11 2157, and ax-12 2173. (Revised by Steven Nguyen, 30-Apr-2023.) |
⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | rexeq 3406* | Equality theorem for restricted existential quantifier. (Contributed by NM, 29-Oct-1995.) Remove usage of ax-10 2141, ax-11 2157, and ax-12 2173. (Revised by Steven Nguyen, 30-Apr-2023.) |
⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | reueq1 3407* | 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 2173. (Revised by Steven Nguyen, 30-Apr-2023.) |
⊢ (𝐴 = 𝐵 → (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | rmoeq1 3408* | 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 2173. (Revised by Steven Nguyen, 30-Apr-2023.) |
⊢ (𝐴 = 𝐵 → (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | raleqOLD 3409* | Obsolete version of raleq 3405 as of 5-May-2023. Equality theorem for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | rexeqOLD 3410* | Obsolete version of rexeq 3406 as of 5-May-2023. Equality theorem for restricted existential quantifier. (Contributed by NM, 29-Oct-1995.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | reueq1OLD 3411* | Obsolete version of reueq1 3407 as of 5-May-2023. Equality theorem for restricted unique existential quantifier. (Contributed by NM, 5-Apr-2004.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐴 = 𝐵 → (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | rmoeq1OLD 3412* | Obsolete version of rmoeq1 3408 as of 5-May-2023. Equality theorem for restricted at-most-one quantifier. (Contributed by Alexander van der Vekens, 17-Jun-2017.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐴 = 𝐵 → (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | raleqi 3413* | Equality inference for restricted universal quantifier. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑) | ||
Theorem | rexeqi 3414* | Equality inference for restricted existential quantifier. (Contributed by Mario Carneiro, 23-Apr-2015.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑) | ||
Theorem | raleqdv 3415* | Equality deduction for restricted universal quantifier. (Contributed by NM, 13-Nov-2005.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | rexeqdv 3416* | Equality deduction for restricted existential quantifier. (Contributed by NM, 14-Jan-2007.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | raleqbi1dvOLD 3417* | Obsolete version of raleqbi1dv 3403 as of 5-May-2023. Equality deduction for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | rexeqbi1dvOLD 3418* | Obsolete version of rexeqbi1dv 3404 as of 5-May-2023. Equality deduction for restricted existential quantifier. (Contributed by NM, 18-Mar-1997.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | reueqd 3419* | Equality deduction for restricted unique existential quantifier. (Contributed by NM, 5-Apr-2004.) |
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 = 𝐵 → (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | rmoeqd 3420* | Equality deduction for restricted at-most-one quantifier. (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 = 𝐵 → (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | raleqbid 3421 | Equality deduction for restricted universal quantifier. (Contributed by Thierry Arnoux, 8-Mar-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) | ||
Theorem | rexeqbid 3422 | Equality deduction for restricted existential quantifier. (Contributed by Thierry Arnoux, 8-Mar-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒)) | ||
Theorem | raleqbidvOLD 3423* | Obsolete version of raleqbidv 3401 as of 30-Apr-2023. Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) | ||
Theorem | rexeqbidvOLD 3424* | Obsolete version of rexeqbidv 3402 as of 30-Apr-2023. Equality deduction for restricted existential quantifier. (Contributed by NM, 6-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒)) | ||
Theorem | raleqbidva 3425* | Equality deduction for restricted universal quantifier. (Contributed by Mario Carneiro, 5-Jan-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) | ||
Theorem | rexeqbidva 3426* | Equality deduction for restricted universal quantifier. (Contributed by Mario Carneiro, 5-Jan-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒)) | ||
Theorem | raleleq 3427* | All elements of a class are elements of a class equal to this class. (Contributed by AV, 30-Oct-2020.) |
⊢ (𝐴 = 𝐵 → ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵) | ||
Theorem | raleleqALT 3428* | Alternate proof of raleleq 3427 using ralel 3149, being longer and using more axioms. (Contributed by AV, 30-Oct-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐴 = 𝐵 → ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵) | ||
Theorem | mormo 3429 | Unrestricted "at most one" implies restricted "at most one". (Contributed by NM, 16-Jun-2017.) |
⊢ (∃*𝑥𝜑 → ∃*𝑥 ∈ 𝐴 𝜑) | ||
Theorem | reu5 3430 | Restricted uniqueness in terms of "at most one." (Contributed by NM, 23-May-1999.) (Revised by NM, 16-Jun-2017.) |
⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑)) | ||
Theorem | reurex 3431 | Restricted unique existence implies restricted existence. (Contributed by NM, 19-Aug-1999.) |
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜑) | ||
Theorem | 2reu2rex 3432 | Double restricted existential uniqueness, analogous to 2eu2ex 2724. (Contributed by Alexander van der Vekens, 25-Jun-2017.) |
⊢ (∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) | ||
Theorem | reurmo 3433 | Restricted existential uniqueness implies restricted "at most one." (Contributed by NM, 16-Jun-2017.) |
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ∃*𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rmo5 3434 | Restricted "at most one" in term of uniqueness. (Contributed by NM, 16-Jun-2017.) |
⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 → ∃!𝑥 ∈ 𝐴 𝜑)) | ||
Theorem | nrexrmo 3435 | Nonexistence implies restricted "at most one". (Contributed by NM, 17-Jun-2017.) |
⊢ (¬ ∃𝑥 ∈ 𝐴 𝜑 → ∃*𝑥 ∈ 𝐴 𝜑) | ||
Theorem | reueubd 3436* | Restricted existential uniqueness is equivalent to existential uniqueness if the unique element is in the restricting class. (Contributed by AV, 4-Jan-2021.) |
⊢ ((𝜑 ∧ 𝜓) → 𝑥 ∈ 𝑉) ⇒ ⊢ (𝜑 → (∃!𝑥 ∈ 𝑉 𝜓 ↔ ∃!𝑥𝜓)) | ||
Theorem | cbvralfw 3437* | Rule used to change bound variables, using implicit substitution. Version of cbvralf 3439 with a disjoint variable condition, which does not require ax-13 2386. (Contributed by NM, 7-Mar-2004.) (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvrexfw 3438* | Rule used to change bound variables, using implicit substitution. Version of cbvrexf 3440 with a disjoint variable condition, which does not require ax-13 2386. (Contributed by FL, 27-Apr-2008.) (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvralf 3439 | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2386. Use the weaker cbvralfw 3437 when possible. (Contributed by NM, 7-Mar-2004.) (Revised by Mario Carneiro, 9-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvrexf 3440 | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2386. Use the weaker cbvrexfw 3438 when possible. (Contributed by FL, 27-Apr-2008.) (Revised by Mario Carneiro, 9-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvralw 3441* | Rule used to change bound variables, using implicit substitution. Version of cbvral 3445 with a disjoint variable condition, which does not require ax-13 2386. (Contributed by NM, 31-Jul-2003.) (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvrexw 3442* | Rule used to change bound variables, using implicit substitution. Version of cbvrex 3446 with a disjoint variable condition, which does not require ax-13 2386. (Contributed by NM, 31-Jul-2003.) (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvreuw 3443* | Change the bound variable of a restricted unique existential quantifier using implicit substitution. Version of cbvreu 3447 with a disjoint variable condition, which does not require ax-13 2386. (Contributed by Mario Carneiro, 15-Oct-2016.) (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvrmow 3444* | Change the bound variable of a restricted at-most-one quantifier using implicit substitution. Version of cbvrmo 3448 with a disjoint variable condition, which does not require ax-13 2386. (Contributed by NM, 16-Jun-2017.) (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvral 3445* | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2386. Use the weaker cbvralw 3441 when possible. (Contributed by NM, 31-Jul-2003.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvrex 3446* | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2386. Use the weaker cbvrexw 3442 when possible. (Contributed by NM, 31-Jul-2003.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvreu 3447* | 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 2386. Use the weaker cbvreuw 3443 when possible. (Contributed by Mario Carneiro, 15-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvrmo 3448* | 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 2386. Use the weaker cbvrmow 3444 when possible. (Contributed by NM, 16-Jun-2017.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvralvw 3449* | Change the bound variable of a restricted universal quantifier using implicit substitution. Version of cbvralv 3452 with a disjoint variable condition, which does not require ax-10 2141, ax-11 2157, ax-12 2173, ax-13 2386. (Contributed by NM, 28-Jan-1997.) (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvrexvw 3450* | Change the bound variable of a restricted existential quantifier using implicit substitution. Version of cbvrexv 3453 with a disjoint variable condition, which does not require ax-10 2141, ax-11 2157, ax-12 2173, ax-13 2386. (Contributed by NM, 2-Jun-1998.) (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvreuvw 3451* | Change the bound variable of a restricted unique existential quantifier using implicit substitution. Version of cbvreuv 3454 with a disjoint variable condition, which does not require ax-13 2386. (Contributed by NM, 5-Apr-2004.) (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvralv 3452* | Change the bound variable of a restricted universal quantifier using implicit substitution. See cbvralvw 3449 based on fewer axioms , but extra disjoint variables. Usage of this theorem is discouraged because it depends on ax-13 2386. Use the weaker cbvralvw 3449 when possible. (Contributed by NM, 28-Jan-1997.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvrexv 3453* | Change the bound variable of a restricted existential quantifier using implicit substitution. See cbvrexvw 3450 based on fewer axioms , but extra disjoint variables. Usage of this theorem is discouraged because it depends on ax-13 2386. Use the weaker cbvrexvw 3450 when possible. (Contributed by NM, 2-Jun-1998.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvreuv 3454* | Change the bound variable of a restricted unique existential quantifier using implicit substitution. See cbvreuvw 3451 for a version without ax-13 2386, but extra disjoint variables. Usage of this theorem is discouraged because it depends on ax-13 2386. Use the weaker cbvreuvw 3451 when possible. (Contributed by NM, 5-Apr-2004.) (Revised by Mario Carneiro, 15-Oct-2016.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvrmov 3455* | 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 2386. (Contributed by Alexander van der Vekens, 17-Jun-2017.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvraldva2 3456* | Rule used to change the bound variable in a restricted universal quantifier with implicit substitution which also changes the quantifier domain. Deduction form. (Contributed by David Moews, 1-May-2017.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒)) | ||
Theorem | cbvrexdva2 3457* | Rule used to change the bound variable in a restricted existential quantifier with implicit substitution which also changes the quantifier domain. Deduction form. (Contributed by David Moews, 1-May-2017.) (Proof shortened by Wolf Lammen, 12-Aug-2023.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒)) | ||
Theorem | cbvrexdva2OLD 3458* | Obsolete version of cbvrexdva 3460 as of 12-Aug-2023. (Contributed by David Moews, 1-May-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒)) | ||
Theorem | cbvraldva 3459* | Rule used to change the bound variable in a restricted universal quantifier with implicit substitution. Deduction form. (Contributed by David Moews, 1-May-2017.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑦 ∈ 𝐴 𝜒)) | ||
Theorem | cbvrexdva 3460* | Rule used to change the bound variable in a restricted existential quantifier with implicit substitution. Deduction form. (Contributed by David Moews, 1-May-2017.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑦 ∈ 𝐴 𝜒)) | ||
Theorem | cbvral2vw 3461* | Change bound variables of double restricted universal quantification, using implicit substitution. Version of cbvral2v 3464 with a disjoint variable condition, which does not require ax-13 2386. (Contributed by NM, 10-Aug-2004.) (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 𝜓) | ||
Theorem | cbvrex2vw 3462* | Change bound variables of double restricted universal quantification, using implicit substitution. Version of cbvrex2v 3465 with a disjoint variable condition, which does not require ax-13 2386. (Contributed by FL, 2-Jul-2012.) (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝜓) | ||
Theorem | cbvral3vw 3463* | Change bound variables of triple restricted universal quantification, using implicit substitution. Version of cbvral3v 3466 with a disjoint variable condition, which does not require ax-13 2386. (Contributed by NM, 10-May-2005.) (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ (𝑥 = 𝑤 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝑣 → (𝜒 ↔ 𝜃)) & ⊢ (𝑧 = 𝑢 → (𝜃 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 ↔ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐵 ∀𝑢 ∈ 𝐶 𝜓) | ||
Theorem | cbvral2v 3464* | Change bound variables of double restricted universal quantification, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2386. Use the weaker cbvral2vw 3461 when possible. (Contributed by NM, 10-Aug-2004.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 𝜓) | ||
Theorem | cbvrex2v 3465* | Change bound variables of double restricted universal quantification, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2386. Use the weaker cbvrex2vw 3462 when possible. (Contributed by FL, 2-Jul-2012.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝜓) | ||
Theorem | cbvral3v 3466* | Change bound variables of triple restricted universal quantification, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2386. Use the weaker cbvral3vw 3463 when possible. (Contributed by NM, 10-May-2005.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑤 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝑣 → (𝜒 ↔ 𝜃)) & ⊢ (𝑧 = 𝑢 → (𝜃 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 ↔ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐵 ∀𝑢 ∈ 𝐶 𝜓) | ||
Theorem | cbvralsvw 3467* | Change bound variable by using a substitution. Version of cbvralsv 3469 with a disjoint variable condition, which does not require ax-13 2386. (Contributed by NM, 20-Nov-2005.) (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 [𝑦 / 𝑥]𝜑) | ||
Theorem | cbvrexsvw 3468* | Change bound variable by using a substitution. Version of cbvrexsv 3470 with a disjoint variable condition, which does not require ax-13 2386. (Contributed by NM, 2-Mar-2008.) (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 [𝑦 / 𝑥]𝜑) | ||
Theorem | cbvralsv 3469* | Change bound variable by using a substitution. Usage of this theorem is discouraged because it depends on ax-13 2386. Use the weaker cbvralsvw 3467 when possible. (Contributed by NM, 20-Nov-2005.) (Revised by Andrew Salmon, 11-Jul-2011.) (New usage is discouraged.) |
⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 [𝑦 / 𝑥]𝜑) | ||
Theorem | cbvrexsv 3470* | Change bound variable by using a substitution. Usage of this theorem is discouraged because it depends on ax-13 2386. Use the weaker cbvrexsvw 3468 when possible. (Contributed by NM, 2-Mar-2008.) (Revised by Andrew Salmon, 11-Jul-2011.) (New usage is discouraged.) |
⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 [𝑦 / 𝑥]𝜑) | ||
Theorem | sbralie 3471* | Implicit to explicit substitution that swaps variables in a quantified expression. (Contributed by NM, 5-Sep-2004.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝑦 𝜑 ↔ [𝑦 / 𝑥]∀𝑦 ∈ 𝑥 𝜓) | ||
Theorem | rabbiia 3472 | Equivalent wff's yield equal restricted class abstractions (inference form). (Contributed by NM, 22-May-1999.) |
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓} | ||
Theorem | rabbii 3473 | Equivalent wff's correspond to equal restricted class abstractions. Inference form of rabbidv 3480. (Contributed by Peter Mazsa, 1-Nov-2019.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓} | ||
Theorem | rabbida 3474 | Equivalent wff's yield equal restricted class abstractions (deduction form). Version of rabbidva 3478 with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒}) | ||
Theorem | rabbid 3475 | Version of rabbidv 3480 with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒}) | ||
Theorem | rabbidva2 3476* | Equivalent wff's yield equal restricted class abstractions. (Contributed by Thierry Arnoux, 4-Feb-2017.) |
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒))) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | rabbia2 3477 | Equivalent wff's yield equal restricted class abstractions. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒)) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒} | ||
Theorem | rabbidva 3478* | Equivalent wff's yield equal restricted class abstractions (deduction form). (Contributed by NM, 28-Nov-2003.) (Proof shortened by SN, 3-Dec-2023.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒}) | ||
Theorem | rabbidvaOLD 3479* | Obsolete proof of rabbidva 3478 as of 4-Dec-2023. (Contributed by NM, 28-Nov-2003.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒}) | ||
Theorem | rabbidv 3480* | Equivalent wff's yield equal restricted class abstractions (deduction form). (Contributed by NM, 10-Feb-1995.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒}) | ||
Theorem | rabeqf 3481 | Equality theorem for restricted class abstractions, with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by NM, 7-Mar-2004.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑}) | ||
Theorem | rabeqi 3482 | Equality theorem for restricted class abstractions. Inference form of rabeqf 3481. (Contributed by Glauco Siliprandi, 26-Jun-2021.) Avoid ax-10 2141 and ax-11 2157. (Revised by Gino Giotto, 20-Aug-2023.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑} | ||
Theorem | rabeq 3483* | Equality theorem for restricted class abstractions. (Contributed by NM, 15-Oct-2003.) Avoid ax-10 2141, ax-11 2157, ax-12 2173. (Revised by Gino Giotto, 20-Aug-2023.) |
⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑}) | ||
Theorem | rabeqdv 3484* | Equality of restricted class abstractions. Deduction form of rabeq 3483. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓}) | ||
Theorem | rabeqbidv 3485* | Equality of restricted class abstractions. (Contributed by Jeff Madsen, 1-Dec-2009.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | rabeqbidva 3486* | Equality of restricted class abstractions. (Contributed by Mario Carneiro, 26-Jan-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | rabeq2i 3487 | Inference from equality of a class variable and a restricted class abstraction. (Contributed by NM, 16-Feb-2004.) |
⊢ 𝐴 = {𝑥 ∈ 𝐵 ∣ 𝜑} ⇒ ⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐵 ∧ 𝜑)) | ||
Theorem | rabswap 3488 | Swap with a membership relation in a restricted class abstraction. (Contributed by NM, 4-Jul-2005.) |
⊢ {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} = {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝐴} | ||
Theorem | cbvrabw 3489* | Rule to change the bound variable in a restricted class abstraction, using implicit substitution. Version of cbvrab 3490 with a disjoint variable condition, which does not require ax-13 2386. (Contributed by Andrew Salmon, 11-Jul-2011.) (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓} | ||
Theorem | cbvrab 3490 | 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 2386. Use the weaker cbvrabw 3489 when possible. (Contributed by Andrew Salmon, 11-Jul-2011.) (Revised by Mario Carneiro, 9-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓} | ||
Theorem | cbvrabv 3491* | 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 2386. (Revised by Steven Nguyen, 4-Dec-2022.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓} | ||
Theorem | cbvrabvOLD 3492* | Obsolete version of cbvrabv 3491 as of 14-Jun-2023. Rule to change the bound variable in a restricted class abstraction, using implicit substitution. (Contributed by NM, 26-May-1999.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓} | ||
Theorem | rabrabi 3493* | Abstract builder restricted to another restricted abstract builder with implicit substitution. (Contributed by AV, 2-Aug-2022.) Avoid ax-10 2141 and ax-11 2157. (Revised by Gino Giotto, 20-Aug-2023.) |
⊢ (𝑥 = 𝑦 → (𝜒 ↔ 𝜑)) ⇒ ⊢ {𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑} ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ (𝜒 ∧ 𝜓)} | ||
Syntax | cvv 3494 | Extend class notation to include the universal class symbol. |
class V | ||
Theorem | vjust 3495 | Soundness justification theorem for df-v 3496. (Contributed by Rodolfo Medina, 27-Apr-2010.) |
⊢ {𝑥 ∣ 𝑥 = 𝑥} = {𝑦 ∣ 𝑦 = 𝑦} | ||
Definition | df-v 3496 | 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 5211 proves that V is not itself a set in ZFC. We will frequently use the expression 𝐴 ∈ V as a short way to say "𝐴 is a set", and isset 3506 proves that this expression has the same meaning as ∃𝑥𝑥 = 𝐴. The class V is called the "von Neumann universe", however, the letter "V" is not a tribute to the name of 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 word "Verum". Peano's notation V was adopted by Whitehead and Russell in Principia Mathematica for the class of all sets in 1910. For a general discussion of the theory of classes, see mmset.html#class 3506. (Contributed by NM, 26-May-1993.) |
⊢ V = {𝑥 ∣ 𝑥 = 𝑥} | ||
Theorem | vex 3497 | All setvar variables are sets (see isset 3506). Theorem 6.8 of [Quine] p. 43. (Contributed by NM, 26-May-1993.) Remove use of ax-12 2173. (Revised by SN, 28-Aug-2023.) |
⊢ 𝑥 ∈ V | ||
Theorem | vexOLD 3498 | Obsolete version of vex 3497 as of 28-Aug-2023. All setvar variables are sets (see isset 3506). Theorem 6.8 of [Quine] p. 43. (Contributed by NM, 26-May-1993.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝑥 ∈ V | ||
Theorem | elv 3499 | If a proposition is implied by 𝑥 ∈ V (which is true, see vex 3497), then it is true. (Contributed by Peter Mazsa, 13-Oct-2018.) |
⊢ (𝑥 ∈ V → 𝜑) ⇒ ⊢ 𝜑 | ||
Theorem | elvd 3500 | If a proposition is implied by 𝑥 ∈ V (which is true, see vex 3497) and another antecedent, then it is implied by that other antecedent. Deduction associated with elv 3499. (Contributed by Peter Mazsa, 23-Oct-2018.) |
⊢ ((𝜑 ∧ 𝑥 ∈ V) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |