![]() |
Metamath
Proof Explorer Theorem List (p. 34 of 486) | < 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-30854) |
![]() (30855-32377) |
![]() (32378-48571) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nfrexw 3301* | Bound-variable hypothesis builder for restricted quantification. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2019.) Add disjoint variable condition to avoid ax-13 2366. See nfrex 3359 for a less restrictive version requiring more axioms. (Revised by GG, 20-Jan-2024.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑 | ||
Theorem | r19.12 3302* | Restricted quantifier version of 19.12 2316. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) Avoid ax-13 2366, ax-ext 2697. (Revised by Wolf Lammen, 17-Jun-2023.) (Proof shortened by Wolf Lammen, 4-Nov-2024.) |
⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) | ||
Theorem | r19.12OLD 3303* | Obsolete version of 19.12 2316 as of 4-Nov-2024. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) Avoid ax-13 2366, ax-ext 2697. (Revised by Wolf Lammen, 17-Jun-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) | ||
Theorem | reean 3304* | Rearrange restricted existential quantifiers. For a version based on fewer axioms see reeanv 3217. (Contributed by NM, 27-Oct-2010.) (Proof shortened by Andrew Salmon, 30-May-2011.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | cbvralsvw 3305* | Change bound variable by using a substitution. Version of cbvralsv 3350 with a disjoint variable condition, which does not require ax-13 2366. (Contributed by NM, 20-Nov-2005.) Avoid ax-13 2366. (Revised by GG, 10-Jan-2024.) (Proof shortened by Wolf Lammen, 8-Mar-2025.) |
⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 [𝑦 / 𝑥]𝜑) | ||
Theorem | cbvrexsvw 3306* | Change bound variable by using a substitution. Version of cbvrexsv 3351 with a disjoint variable condition, which does not require ax-13 2366. (Contributed by NM, 2-Mar-2008.) Avoid ax-13 2366. (Revised by GG, 10-Jan-2024.) (Proof shortened by Wolf Lammen, 8-Mar-2025.) |
⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 [𝑦 / 𝑥]𝜑) | ||
Theorem | cbvralsvwOLD 3307* | Obsolete version of cbvralsvw 3305 as of 8-Mar-2025. (Contributed by NM, 20-Nov-2005.) Avoid ax-13 2366. (Revised by GG, 10-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 [𝑦 / 𝑥]𝜑) | ||
Theorem | cbvrexsvwOLD 3308* | Obsolete version of cbvrexsvw 3306 as of 8-Mar-2025. (Contributed by NM, 20-Nov-2005.) Avoid ax-13 2366. (Revised by GG, 10-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 [𝑦 / 𝑥]𝜑) | ||
Theorem | nfraldwOLD 3309* | Obsolete version of nfraldw 3297 as of 24-Sep-2024. (Contributed by NM, 15-Feb-2013.) (Revised by GG, 10-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜓) | ||
Theorem | nfra2wOLDOLD 3310* | Obsolete version of nfra2w 3287 as of 24-Sep-2024. (Contributed by Alan Sare, 31-Dec-2011.) (Revised by GG, 10-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑦∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 | ||
Theorem | rexeq 3311* | Equality theorem for restricted existential quantifier. (Contributed by NM, 29-Oct-1995.) Remove usage of ax-10 2130, ax-11 2147, and ax-12 2167. (Revised by Steven Nguyen, 30-Apr-2023.) Shorten other proofs. (Revised by Wolf Lammen, 8-Mar-2025.) |
⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | raleq 3312* | Equality theorem for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.) Remove usage of ax-10 2130, ax-11 2147, and ax-12 2167. (Revised by Steven Nguyen, 30-Apr-2023.) Shorten other proofs. (Revised by Wolf Lammen, 8-Mar-2025.) |
⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | raleqi 3313* | Equality inference for restricted universal quantifier. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑) | ||
Theorem | rexeqi 3314* | Equality inference for restricted existential quantifier. (Contributed by Mario Carneiro, 23-Apr-2015.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑) | ||
Theorem | raleqdv 3315* | Equality deduction for restricted universal quantifier. (Contributed by NM, 13-Nov-2005.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | rexeqdv 3316* | Equality deduction for restricted existential quantifier. (Contributed by NM, 14-Jan-2007.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | raleqbidva 3317* | Equality deduction for restricted universal quantifier. (Contributed by Mario Carneiro, 5-Jan-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) | ||
Theorem | rexeqbidva 3318* | Equality deduction for restricted universal quantifier. (Contributed by Mario Carneiro, 5-Jan-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒)) | ||
Theorem | raleqbidvv 3319* | Version of raleqbidv 3330 with additional disjoint variable conditions, not requiring ax-8 2101 nor df-clel 2803. (Contributed by BJ, 22-Sep-2024.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) | ||
Theorem | raleqbidvvOLD 3320* | Obsolete version of raleqbidvv 3319 as of 9-Mar-2025. (Contributed by BJ, 22-Sep-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) | ||
Theorem | rexeqbidvv 3321* | Version of rexeqbidv 3331 with additional disjoint variable conditions, not requiring ax-8 2101 nor df-clel 2803. (Contributed by Wolf Lammen, 25-Sep-2024.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒)) | ||
Theorem | rexeqbidvvOLD 3322* | Obsolete version of rexeqbidvv 3321 as of 9-Mar-2025. (Contributed by Wolf Lammen, 25-Sep-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒)) | ||
Theorem | raleqbi1dv 3323* | Equality deduction for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.) (Proof shortened by Steven Nguyen, 5-May-2023.) |
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | rexeqbi1dv 3324* | Equality deduction for restricted existential quantifier. (Contributed by NM, 18-Mar-1997.) (Proof shortened by Steven Nguyen, 5-May-2023.) |
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | raleqOLD 3325* | Obsolete version of raleq 3312 as of 9-Mar-2025. (Contributed by NM, 16-Nov-1995.) Remove usage of ax-10 2130, ax-11 2147, and ax-12 2167. (Revised by Steven Nguyen, 30-Apr-2023.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | rexeqOLD 3326* | Obsolete version of raleq 3312 as of 9-Mar-2025. (Contributed by NM, 29-Oct-1995.) Remove usage of ax-10 2130, ax-11 2147, and ax-12 2167. (Revised by Steven Nguyen, 30-Apr-2023.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | raleleq 3327* | All elements of a class are elements of a class equal to this class. (Contributed by AV, 30-Oct-2020.) |
⊢ (𝐴 = 𝐵 → ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵) | ||
Theorem | raleqbii 3328 | Equality deduction for restricted universal quantifier, changing both formula and quantifier domain. Inference form. (Contributed by David Moews, 1-May-2017.) |
⊢ 𝐴 = 𝐵 & ⊢ (𝜓 ↔ 𝜒) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒) | ||
Theorem | rexeqbii 3329 | Equality deduction for restricted existential quantifier, changing both formula and quantifier domain. Inference form. (Contributed by David Moews, 1-May-2017.) |
⊢ 𝐴 = 𝐵 & ⊢ (𝜓 ↔ 𝜒) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒) | ||
Theorem | raleqbidv 3330* | Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.) Remove usage of ax-10 2130, ax-11 2147, and ax-12 2167 and reduce distinct variable conditions. (Revised by Steven Nguyen, 30-Apr-2023.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) | ||
Theorem | rexeqbidv 3331* | Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.) Remove usage of ax-10 2130, ax-11 2147, and ax-12 2167 and reduce distinct variable conditions. (Revised by Steven Nguyen, 30-Apr-2023.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒)) | ||
Theorem | cbvraldva2 3332* | 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 3333* | 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, 8-Jan-2025.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒)) | ||
Theorem | cbvrexdva2OLD 3334* | Obsolete version of cbvrexdva2 3333 as of 8-Jan-2025. (Contributed by David Moews, 1-May-2017.) (Proof shortened by Wolf Lammen, 12-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒)) | ||
Theorem | cbvraldvaOLD 3335* | Obsolete version of cbvraldva 3227 as of 9-Mar-2025. (Contributed by David Moews, 1-May-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑦 ∈ 𝐴 𝜒)) | ||
Theorem | cbvrexdvaOLD 3336* | Obsolete version of cbvrexdva 3228 as of 9-Mar-2025. (Contributed by David Moews, 1-May-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑦 ∈ 𝐴 𝜒)) | ||
Theorem | raleqf 3337 | Equality theorem for restricted universal quantifier, with bound-variable hypotheses instead of distinct variable restrictions. See raleq 3312 for a version based on fewer axioms. (Contributed by NM, 7-Mar-2004.) (Revised by Andrew Salmon, 11-Jul-2011.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | rexeqf 3338 | Equality theorem for restricted existential quantifier, with bound-variable hypotheses instead of distinct variable restrictions. See rexeq 3311 for a version based on fewer axioms. (Contributed by NM, 9-Oct-2003.) (Revised by Andrew Salmon, 11-Jul-2011.) (Proof shortened by Wolf Lammen, 9-Mar-2025.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | rexeqfOLD 3339 | Obsolete version of rexeqf 3338 as of 9-Mar-2025. (Contributed by NM, 9-Oct-2003.) (Revised by Andrew Salmon, 11-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | raleqbid 3340 | Equality deduction for restricted universal quantifier. See raleqbidv 3330 for a version based on fewer axioms. (Contributed by Thierry Arnoux, 8-Mar-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) | ||
Theorem | rexeqbid 3341 | Equality deduction for restricted existential quantifier. See rexeqbidv 3331 for a version based on fewer axioms. (Contributed by Thierry Arnoux, 8-Mar-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒)) | ||
Theorem | sbralie 3342* | Implicit to explicit substitution that swaps variables in a rectrictedly universally quantified expression. (Contributed by NM, 5-Sep-2004.) Avoid ax-ext 2697, df-cleq 2718, df-clel 2803. (Revised by Wolf Lammen, 10-Mar-2025.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝑦 𝜑 ↔ [𝑦 / 𝑥]∀𝑦 ∈ 𝑥 𝜓) | ||
Theorem | sbralieALT 3343* | Alternative shorter proof of sbralie 3342 dependent on ax-ext 2697, df-cleq 2718, df-clel 2803. (Contributed by NM, 5-Sep-2004.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝑦 𝜑 ↔ [𝑦 / 𝑥]∀𝑦 ∈ 𝑥 𝜓) | ||
Theorem | cbvralf 3344 | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker cbvralfw 3292 when possible. (Contributed by NM, 7-Mar-2004.) (Revised by Mario Carneiro, 9-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvrexf 3345 | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker cbvrexfw 3293 when possible. (Contributed by FL, 27-Apr-2008.) (Revised by Mario Carneiro, 9-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvral 3346* | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker cbvralw 3294 when possible. (Contributed by NM, 31-Jul-2003.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvrex 3347* | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker cbvrexw 3295 when possible. (Contributed by NM, 31-Jul-2003.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvralv 3348* | Change the bound variable of a restricted universal quantifier using implicit substitution. See cbvralvw 3225 based on fewer axioms , but extra disjoint variables. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker cbvralvw 3225 when possible. (Contributed by NM, 28-Jan-1997.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvrexv 3349* | Change the bound variable of a restricted existential quantifier using implicit substitution. See cbvrexvw 3226 based on fewer axioms , but extra disjoint variables. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker cbvrexvw 3226 when possible. (Contributed by NM, 2-Jun-1998.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvralsv 3350* | Change bound variable by using a substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker cbvralsvw 3305 when possible. (Contributed by NM, 20-Nov-2005.) (Revised by Andrew Salmon, 11-Jul-2011.) (New usage is discouraged.) |
⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 [𝑦 / 𝑥]𝜑) | ||
Theorem | cbvrexsv 3351* | Change bound variable by using a substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker cbvrexsvw 3306 when possible. (Contributed by NM, 2-Mar-2008.) (Revised by Andrew Salmon, 11-Jul-2011.) (New usage is discouraged.) |
⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 [𝑦 / 𝑥]𝜑) | ||
Theorem | cbvral2v 3352* | Change bound variables of double restricted universal quantification, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker cbvral2vw 3229 when possible. (Contributed by NM, 10-Aug-2004.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 𝜓) | ||
Theorem | cbvrex2v 3353* | Change bound variables of double restricted universal quantification, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker cbvrex2vw 3230 when possible. (Contributed by FL, 2-Jul-2012.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝜓) | ||
Theorem | cbvral3v 3354* | Change bound variables of triple restricted universal quantification, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker cbvral3vw 3231 when possible. (Contributed by NM, 10-May-2005.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑤 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝑣 → (𝜒 ↔ 𝜃)) & ⊢ (𝑧 = 𝑢 → (𝜃 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 ↔ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐵 ∀𝑢 ∈ 𝐶 𝜓) | ||
Theorem | rgen2a 3355* | Generalization rule for restricted quantification. Note that 𝑥 and 𝑦 are not required to be disjoint. This proof illustrates the use of dvelim 2445. This theorem relies on the full set of axioms up to ax-ext 2697 and it should no longer be used. Usage of rgen2 3188 is highly encouraged. (Contributed by NM, 23-Nov-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 1-Jan-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → 𝜑) ⇒ ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝜑 | ||
Theorem | nfrald 3356 | Deduction version of nfral 3358. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker nfraldw 3297 when possible. (Contributed by NM, 15-Feb-2013.) (Revised by Mario Carneiro, 7-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜓) | ||
Theorem | nfrexd 3357 | Deduction version of nfrex 3359. Usage of this theorem is discouraged because it depends on ax-13 2366. See nfrexdw 3298 for a version with a disjoint variable condition, but not requiring ax-13 2366. (Contributed by Mario Carneiro, 14-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜓) | ||
Theorem | nfral 3358 | Bound-variable hypothesis builder for restricted quantification. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker nfralw 3299 when possible. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 7-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑 | ||
Theorem | nfrex 3359 | Bound-variable hypothesis builder for restricted quantification. Usage of this theorem is discouraged because it depends on ax-13 2366. See nfrexw 3301 for a version with a disjoint variable condition, but not requiring ax-13 2366. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2019.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑 | ||
Theorem | nfra2 3360* | Similar to Lemma 24 of [Monk2] p. 114, except the quantification of the antecedent is restricted. Derived automatically from hbra2VD 44554. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker nfra2w 3287 when possible. (Contributed by Alan Sare, 31-Dec-2011.) (New usage is discouraged.) |
⊢ Ⅎ𝑦∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 | ||
Theorem | ralcom2 3361* | Commutation of restricted universal quantifiers. Note that 𝑥 and 𝑦 need not be disjoint (this makes the proof longer). This theorem relies on the full set of axioms up to ax-ext 2697 and it should no longer be used. Usage of ralcom 3277 is highly encouraged. (Contributed by NM, 24-Nov-1994.) (Proof shortened by Mario Carneiro, 17-Oct-2016.) (New usage is discouraged.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝜑 → ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 𝜑) | ||
Syntax | wreu 3362 | Extend wff notation to include restricted existential uniqueness. |
wff ∃!𝑥 ∈ 𝐴 𝜑 | ||
Syntax | wrmo 3363 | Extend wff notation to include restricted "at most one". |
wff ∃*𝑥 ∈ 𝐴 𝜑 | ||
Definition | df-rmo 3364 |
Define restricted "at most one". Note: This notation is most often
used
to express that 𝜑 holds for at most one element of a
given class
𝐴. For this reading Ⅎ𝑥𝐴 is required, though, for example,
asserted when 𝑥 and 𝐴 are disjoint.
Should instead 𝐴 depend on 𝑥, you rather assert at most one 𝑥 fulfilling 𝜑 happens to be contained in the corresponding 𝐴(𝑥). This interpretation is rarely needed (see also df-ral 3052). (Contributed by NM, 16-Jun-2017.) |
⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | ||
Definition | df-reu 3365 |
Define restricted existential uniqueness.
Note: This notation is most often used to express that 𝜑 holds for exactly one element of a given class 𝐴. For this reading Ⅎ𝑥𝐴 is required, though, for example, asserted when 𝑥 and 𝐴 are disjoint. Should instead 𝐴 depend on 𝑥, you rather assert exactly one 𝑥 fulfilling 𝜑 happens to be contained in the corresponding 𝐴(𝑥). This interpretation is rarely needed (see also df-ral 3052). (Contributed by NM, 22-Nov-1994.) |
⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | ||
Theorem | reu5 3366 | Restricted uniqueness in terms of "at most one". (Contributed by NM, 23-May-1999.) (Revised by NM, 16-Jun-2017.) |
⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑)) | ||
Theorem | reurmo 3367 | Restricted existential uniqueness implies restricted "at most one." (Contributed by NM, 16-Jun-2017.) |
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ∃*𝑥 ∈ 𝐴 𝜑) | ||
Theorem | reurex 3368 | Restricted unique existence implies restricted existence. (Contributed by NM, 19-Aug-1999.) |
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜑) | ||
Theorem | mormo 3369 | Unrestricted "at most one" implies restricted "at most one". (Contributed by NM, 16-Jun-2017.) |
⊢ (∃*𝑥𝜑 → ∃*𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rmobiia 3370 | Formula-building rule for restricted existential quantifier (inference form). (Contributed by NM, 16-Jun-2017.) |
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐴 𝜓) | ||
Theorem | reubiia 3371 | Formula-building rule for restricted existential quantifier (inference form). (Contributed by NM, 14-Nov-2004.) |
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜓) | ||
Theorem | rmobii 3372 | Formula-building rule for restricted existential quantifier (inference form). (Contributed by NM, 16-Jun-2017.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐴 𝜓) | ||
Theorem | reubii 3373 | Formula-building rule for restricted existential quantifier (inference form). (Contributed by NM, 22-Oct-1999.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜓) | ||
Theorem | rmoanid 3374 | Cancellation law for restricted at-most-one quantification. (Contributed by Peter Mazsa, 24-May-2018.) (Proof shortened by Wolf Lammen, 12-Jan-2025.) |
⊢ (∃*𝑥 ∈ 𝐴 (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃*𝑥 ∈ 𝐴 𝜑) | ||
Theorem | reuanid 3375 | Cancellation law for restricted unique existential quantification. (Contributed by Peter Mazsa, 12-Feb-2018.) (Proof shortened by Wolf Lammen, 12-Jan-2025.) |
⊢ (∃!𝑥 ∈ 𝐴 (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃!𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rmoanidOLD 3376 | Obsolete version of rmoanid 3374 as of 12-Jan-2025. (Contributed by Peter Mazsa, 24-May-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∃*𝑥 ∈ 𝐴 (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃*𝑥 ∈ 𝐴 𝜑) | ||
Theorem | reuanidOLD 3377 | Obsolete version of reuanid 3375 as of 12-Jan-2025. (Contributed by Peter Mazsa, 12-Feb-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∃!𝑥 ∈ 𝐴 (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃!𝑥 ∈ 𝐴 𝜑) | ||
Theorem | 2reu2rex 3378 | Double restricted existential uniqueness, analogous to 2eu2ex 2632. (Contributed by Alexander van der Vekens, 25-Jun-2017.) |
⊢ (∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) | ||
Theorem | rmobidva 3379* | Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 16-Jun-2017.) Avoid ax-6 1964, ax-7 2004, ax-12 2167. (Revised by Wolf Lammen, 23-Nov-2024.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | reubidva 3380* | Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 13-Nov-2004.) Reduce axiom usage. (Revised by Wolf Lammen, 14-Jan-2023.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | rmobidv 3381* | Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 16-Jun-2017.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | reubidv 3382* | Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 17-Oct-1996.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | reueubd 3383* | Restricted existential uniqueness is equivalent to existential uniqueness if the unique element is in the restricting class. (Contributed by AV, 4-Jan-2021.) |
⊢ ((𝜑 ∧ 𝜓) → 𝑥 ∈ 𝑉) ⇒ ⊢ (𝜑 → (∃!𝑥 ∈ 𝑉 𝜓 ↔ ∃!𝑥𝜓)) | ||
Theorem | rmo5 3384 | Restricted "at most one" in term of uniqueness. (Contributed by NM, 16-Jun-2017.) |
⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 → ∃!𝑥 ∈ 𝐴 𝜑)) | ||
Theorem | nrexrmo 3385 | Nonexistence implies restricted "at most one". (Contributed by NM, 17-Jun-2017.) |
⊢ (¬ ∃𝑥 ∈ 𝐴 𝜑 → ∃*𝑥 ∈ 𝐴 𝜑) | ||
Theorem | moel 3386* | "At most one" element in a set. (Contributed by Thierry Arnoux, 26-Jul-2018.) Avoid ax-11 2147. (Revised by Wolf Lammen, 23-Nov-2024.) |
⊢ (∃*𝑥 𝑥 ∈ 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 = 𝑦) | ||
Theorem | cbvrmovw 3387* | Change the bound variable of a restricted at-most-one quantifier using implicit substitution. Version of cbvrmov 3413 with a disjoint variable condition, which requires fewer axioms. (Contributed by NM, 16-Jun-2017.) (Revised by GG, 30-Sep-2024.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvreuvw 3388* | Change the bound variable of a restricted unique existential quantifier using implicit substitution. Version of cbvreuv 3414 with a disjoint variable condition, which requires fewer axioms. (Contributed by NM, 5-Apr-2004.) (Revised by GG, 30-Sep-2024.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐴 𝜓) | ||
Theorem | moelOLD 3389* | Obsolete version of moel 3386 as of 23-Nov-2024. (Contributed by Thierry Arnoux, 26-Jul-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∃*𝑥 𝑥 ∈ 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 = 𝑦) | ||
Theorem | rmobida 3390 | Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 16-Jun-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | reubida 3391 | Formula-building rule for restricted existential quantifier (deduction form). (Contributed by Mario Carneiro, 19-Nov-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | rmobidvaOLD 3392* | Obsolete version of rmobidv 3381 as of 23-Nov-2024. (Contributed by NM, 16-Jun-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | cbvrmow 3393* | Change the bound variable of a restricted at-most-one quantifier using implicit substitution. Version of cbvrmo 3412 with a disjoint variable condition, which does not require ax-10 2130, ax-13 2366. (Contributed by NM, 16-Jun-2017.) Avoid ax-10 2130, ax-13 2366. (Revised by GG, 23-May-2024.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvreuw 3394* | Change the bound variable of a restricted unique existential quantifier using implicit substitution. Version of cbvreu 3411 with a disjoint variable condition, which does not require ax-13 2366. (Contributed by Mario Carneiro, 15-Oct-2016.) Avoid ax-13 2366. (Revised by GG, 10-Jan-2024.) Avoid ax-10 2130. (Revised by Wolf Lammen, 10-Dec-2024.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐴 𝜓) | ||
Theorem | nfrmo1 3395 | The setvar 𝑥 is not free in ∃*𝑥 ∈ 𝐴𝜑. (Contributed by NM, 16-Jun-2017.) |
⊢ Ⅎ𝑥∃*𝑥 ∈ 𝐴 𝜑 | ||
Theorem | nfreu1 3396 | The setvar 𝑥 is not free in ∃!𝑥 ∈ 𝐴𝜑. (Contributed by NM, 19-Mar-1997.) |
⊢ Ⅎ𝑥∃!𝑥 ∈ 𝐴 𝜑 | ||
Theorem | nfrmow 3397* | Bound-variable hypothesis builder for restricted uniqueness. Version of nfrmo 3417 with a disjoint variable condition, which does not require ax-13 2366. (Contributed by NM, 16-Jun-2017.) Avoid ax-13 2366. (Revised by GG, 10-Jan-2024.) Avoid ax-9 2109, ax-ext 2697. (Revised by Wolf Lammen, 21-Nov-2024.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∃*𝑦 ∈ 𝐴 𝜑 | ||
Theorem | nfreuw 3398* | Bound-variable hypothesis builder for restricted unique existence. Version of nfreu 3418 with a disjoint variable condition, which does not require ax-13 2366. (Contributed by NM, 30-Oct-2010.) Avoid ax-13 2366. (Revised by GG, 10-Jan-2024.) Avoid ax-9 2109, ax-ext 2697. (Revised by Wolf Lammen, 21-Nov-2024.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∃!𝑦 ∈ 𝐴 𝜑 | ||
Theorem | cbvreuwOLD 3399* | Obsolete version of cbvreuw 3394 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 | cbvreuvwOLD 3400* | Obsolete version of cbvreuvw 3388 as of 30-Sep-2024. (Contributed by NM, 5-Apr-2004.) (Revised by GG, 10-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐴 𝜓) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |