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