![]() |
Metamath
Proof Explorer Theorem List (p. 34 of 443) | < 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-28464) |
![]() (28465-29989) |
![]() (29990-44213) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | reean 3301* | Rearrange restricted existential quantifiers. (Contributed by NM, 27-Oct-2010.) (Proof shortened by Andrew Salmon, 30-May-2011.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | reeanv 3302* | Rearrange restricted existential quantifiers. (Contributed by NM, 9-May-1999.) |
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | 3reeanv 3303* | Rearrange three restricted existential quantifiers. (Contributed by Jeff Madsen, 11-Jun-2010.) |
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓 ∧ ∃𝑧 ∈ 𝐶 𝜒)) | ||
Theorem | 2ralor 3304* | Distribute restricted universal quantification over "or". (Contributed by Jeff Madsen, 19-Jun-2010.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∨ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∨ ∀𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | nfreu1 3305 | The setvar 𝑥 is not free in ∃!𝑥 ∈ 𝐴𝜑. (Contributed by NM, 19-Mar-1997.) |
⊢ Ⅎ𝑥∃!𝑥 ∈ 𝐴 𝜑 | ||
Theorem | nfrmo1 3306 | The setvar 𝑥 is not free in ∃*𝑥 ∈ 𝐴𝜑. (Contributed by NM, 16-Jun-2017.) |
⊢ Ⅎ𝑥∃*𝑥 ∈ 𝐴 𝜑 | ||
Theorem | nfreud 3307 | Deduction version of nfreu 3309. (Contributed by NM, 15-Feb-2013.) (Revised by Mario Carneiro, 8-Oct-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∃!𝑦 ∈ 𝐴 𝜓) | ||
Theorem | nfrmod 3308 | Deduction version of nfrmo 3310. (Contributed by NM, 17-Jun-2017.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∃*𝑦 ∈ 𝐴 𝜓) | ||
Theorem | nfreu 3309 | Bound-variable hypothesis builder for restricted unique existence. (Contributed by NM, 30-Oct-2010.) (Revised by Mario Carneiro, 8-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∃!𝑦 ∈ 𝐴 𝜑 | ||
Theorem | nfrmo 3310 | Bound-variable hypothesis builder for restricted uniqueness. (Contributed by NM, 16-Jun-2017.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∃*𝑦 ∈ 𝐴 𝜑 | ||
Theorem | rabid 3311 | 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 | rabrab 3312 | Abstract builder restricted to another restricted abstract builder. (Contributed by Thierry Arnoux, 30-Aug-2017.) |
⊢ {𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)} | ||
Theorem | rabidim1 3313 | Membership in a restricted abstraction, implication. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} → 𝑥 ∈ 𝐴) | ||
Theorem | rabid2 3314* | An "identity" law for restricted class abstraction. (Contributed by NM, 9-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) |
⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rabid2f 3315 | 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 | rabbi 3316 | Equivalent wff's correspond to equal restricted class abstractions. Closed theorem form of rabbidva 3396. (Contributed by NM, 25-Nov-2013.) |
⊢ (∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝜒) ↔ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒}) | ||
Theorem | rabswap 3317 | Swap with a membership relation in a restricted class abstraction. (Contributed by NM, 4-Jul-2005.) |
⊢ {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} = {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝐴} | ||
Theorem | nfrab1 3318 | The abstraction variable in a restricted class abstraction isn't free. (Contributed by NM, 19-Mar-1997.) |
⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 𝜑} | ||
Theorem | nfrab 3319 | A variable not free in a wff remains so in a restricted class abstraction. (Contributed by NM, 13-Oct-2003.) (Revised by Mario Carneiro, 9-Oct-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝜑} | ||
Theorem | reubida 3320 | Formula-building rule for restricted existential quantifier (deduction form). (Contributed by Mario Carneiro, 19-Nov-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | reubidva 3321* | 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 | reubidvaOLD 3322* | Obsolete version of reubidva 3321 as of 14-Jan-2023. (Contributed by NM, 13-Nov-2004.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | reubidv 3323* | Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 17-Oct-1996.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | reubiia 3324 | Formula-building rule for restricted existential quantifier (inference form). (Contributed by NM, 14-Nov-2004.) |
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜓) | ||
Theorem | reubii 3325 | Formula-building rule for restricted existential quantifier (inference form). (Contributed by NM, 22-Oct-1999.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜓) | ||
Theorem | rmobida 3326 | Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 16-Jun-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | rmobidva 3327* | Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 16-Jun-2017.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | rmobidv 3328* | Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 16-Jun-2017.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | rmobiia 3329 | Formula-building rule for restricted existential quantifier (inference form). (Contributed by NM, 16-Jun-2017.) |
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐴 𝜓) | ||
Theorem | rmobii 3330 | Formula-building rule for restricted existential quantifier (inference form). (Contributed by NM, 16-Jun-2017.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐴 𝜓) | ||
Theorem | raleqf 3331 | Equality theorem for restricted universal quantifier, with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by NM, 7-Mar-2004.) (Revised by Andrew Salmon, 11-Jul-2011.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | rexeqf 3332 | Equality theorem for restricted existential quantifier, with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by NM, 9-Oct-2003.) (Revised by Andrew Salmon, 11-Jul-2011.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | reueq1f 3333 | 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 | rmoeq1f 3334 | 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 3335* | Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.) Remove usage of ax-10 2077, ax-11 2091, and ax-12 2104 and reduce distinct variable conditions. (Revised by Steven Nguyen, 30-Apr-2023.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) | ||
Theorem | rexeqbidv 3336* | Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.) Remove usage of ax-10 2077, ax-11 2091, and ax-12 2104 and reduce distinct variable conditions. (Revised by Steven Nguyen, 30-Apr-2023.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒)) | ||
Theorem | raleqbi1dv 3337* | Equality deduction for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.) (Proof shortened by Steven Nguyen, 5-May-2023.) |
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | rexeqbi1dv 3338* | Equality deduction for restricted existential quantifier. (Contributed by NM, 18-Mar-1997.) (Proof shortened by Steven Nguyen, 5-May-2023.) |
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | raleq 3339* | Equality theorem for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.) Remove usage of ax-10 2077, ax-11 2091, and ax-12 2104. (Revised by Steven Nguyen, 30-Apr-2023.) |
⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | rexeq 3340* | Equality theorem for restricted existential quantifier. (Contributed by NM, 29-Oct-1995.) Remove usage of ax-10 2077, ax-11 2091, and ax-12 2104. (Revised by Steven Nguyen, 30-Apr-2023.) |
⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | reueq1 3341* | Equality theorem for restricted unique existential quantifier. (Contributed by NM, 5-Apr-2004.) Remove usage of ax-10 2077, ax-11 2091, and ax-12 2104. (Revised by Steven Nguyen, 30-Apr-2023.) |
⊢ (𝐴 = 𝐵 → (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | rmoeq1 3342* | Equality theorem for restricted at-most-one quantifier. (Contributed by Alexander van der Vekens, 17-Jun-2017.) Remove usage of ax-10 2077, ax-11 2091, and ax-12 2104. (Revised by Steven Nguyen, 30-Apr-2023.) |
⊢ (𝐴 = 𝐵 → (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | raleqOLD 3343* | Obsolete version of raleq 3339 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 3344* | Obsolete version of rexeq 3340 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 3345* | Obsolete version of reueq1 3341 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 3346* | Obsolete version of rmoeq1 3342 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 3347* | Equality inference for restricted universal quantifier. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑) | ||
Theorem | rexeqi 3348* | Equality inference for restricted existential quantifier. (Contributed by Mario Carneiro, 23-Apr-2015.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑) | ||
Theorem | raleqdv 3349* | Equality deduction for restricted universal quantifier. (Contributed by NM, 13-Nov-2005.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | rexeqdv 3350* | Equality deduction for restricted existential quantifier. (Contributed by NM, 14-Jan-2007.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | raleqbi1dvOLD 3351* | Obsolete version of raleqbi1dv 3337 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 3352* | Obsolete version of rexeqbi1dv 3338 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 3353* | Equality deduction for restricted unique existential quantifier. (Contributed by NM, 5-Apr-2004.) |
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 = 𝐵 → (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | rmoeqd 3354* | Equality deduction for restricted at-most-one quantifier. (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 = 𝐵 → (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | raleqbid 3355 | Equality deduction for restricted universal quantifier. (Contributed by Thierry Arnoux, 8-Mar-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) | ||
Theorem | rexeqbid 3356 | Equality deduction for restricted existential quantifier. (Contributed by Thierry Arnoux, 8-Mar-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒)) | ||
Theorem | raleqbidvOLD 3357* | Obsolete version of raleqbidv 3335 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 3358* | Obsolete version of rexeqbidv 3336 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 3359* | Equality deduction for restricted universal quantifier. (Contributed by Mario Carneiro, 5-Jan-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) | ||
Theorem | rexeqbidva 3360* | Equality deduction for restricted universal quantifier. (Contributed by Mario Carneiro, 5-Jan-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒)) | ||
Theorem | raleleq 3361* | All elements of a class are elements of a class equal to this class. (Contributed by AV, 30-Oct-2020.) |
⊢ (𝐴 = 𝐵 → ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵) | ||
Theorem | raleleqALT 3362* | Alternate proof of raleleq 3361 using ralel 3093, being longer and using more axioms. (Contributed by AV, 30-Oct-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐴 = 𝐵 → ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵) | ||
Theorem | mormo 3363 | Unrestricted "at most one" implies restricted "at most one". (Contributed by NM, 16-Jun-2017.) |
⊢ (∃*𝑥𝜑 → ∃*𝑥 ∈ 𝐴 𝜑) | ||
Theorem | reu5 3364 | Restricted uniqueness in terms of "at most one." (Contributed by NM, 23-May-1999.) (Revised by NM, 16-Jun-2017.) |
⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑)) | ||
Theorem | reurex 3365 | Restricted unique existence implies restricted existence. (Contributed by NM, 19-Aug-1999.) |
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜑) | ||
Theorem | 2reu2rex 3366 | Double restricted existential uniqueness, analogous to 2eu2ex 2669. (Contributed by Alexander van der Vekens, 25-Jun-2017.) |
⊢ (∃!𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) | ||
Theorem | reurmo 3367 | Restricted existential uniqueness implies restricted "at most one." (Contributed by NM, 16-Jun-2017.) |
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ∃*𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rmo5 3368 | Restricted "at most one" in term of uniqueness. (Contributed by NM, 16-Jun-2017.) |
⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 → ∃!𝑥 ∈ 𝐴 𝜑)) | ||
Theorem | nrexrmo 3369 | Nonexistence implies restricted "at most one". (Contributed by NM, 17-Jun-2017.) |
⊢ (¬ ∃𝑥 ∈ 𝐴 𝜑 → ∃*𝑥 ∈ 𝐴 𝜑) | ||
Theorem | reueubd 3370* | Restricted existential uniqueness is equivalent to existential uniqueness if the unique element is in the restricting class. (Contributed by AV, 4-Jan-2021.) |
⊢ ((𝜑 ∧ 𝜓) → 𝑥 ∈ 𝑉) ⇒ ⊢ (𝜑 → (∃!𝑥 ∈ 𝑉 𝜓 ↔ ∃!𝑥𝜓)) | ||
Theorem | cbvralf 3371 | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 7-Mar-2004.) (Revised by Mario Carneiro, 9-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvrexf 3372 | Rule used to change bound variables, using implicit substitution. (Contributed by FL, 27-Apr-2008.) (Revised by Mario Carneiro, 9-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvral 3373* | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 31-Jul-2003.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvrex 3374* | 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 3375* | Change the bound variable of a restricted unique existential quantifier using implicit substitution. (Contributed by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvrmo 3376* | Change the bound variable of a restricted at-most-one quantifier using implicit substitution. (Contributed by NM, 16-Jun-2017.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvralv 3377* | Change the bound variable of a restricted universal quantifier using implicit substitution. (Contributed by NM, 28-Jan-1997.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvrexv 3378* | Change the bound variable of a restricted existential quantifier using implicit substitution. (Contributed by NM, 2-Jun-1998.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvreuv 3379* | Change the bound variable of a restricted unique existential quantifier using implicit substitution. (Contributed by NM, 5-Apr-2004.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvrmov 3380* | 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 3381* | 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 3382* | 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 3383* | Obsolete version of cbvrexdva 3385 as of 12-Aug-2023. (Contributed by David Moews, 1-May-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒)) | ||
Theorem | cbvraldva 3384* | 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 3385* | 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 | cbvral2v 3386* | Change bound variables of double restricted universal quantification, using implicit substitution. (Contributed by NM, 10-Aug-2004.) |
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 𝜓) | ||
Theorem | cbvrex2v 3387* | Change bound variables of double restricted universal quantification, using implicit substitution. (Contributed by FL, 2-Jul-2012.) |
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝜓) | ||
Theorem | cbvral3v 3388* | Change bound variables of triple restricted universal quantification, using implicit substitution. (Contributed by NM, 10-May-2005.) |
⊢ (𝑥 = 𝑤 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝑣 → (𝜒 ↔ 𝜃)) & ⊢ (𝑧 = 𝑢 → (𝜃 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 ↔ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐵 ∀𝑢 ∈ 𝐶 𝜓) | ||
Theorem | cbvralsv 3389* | Change bound variable by using a substitution. (Contributed by NM, 20-Nov-2005.) (Revised by Andrew Salmon, 11-Jul-2011.) |
⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 [𝑦 / 𝑥]𝜑) | ||
Theorem | cbvrexsv 3390* | Change bound variable by using a substitution. (Contributed by NM, 2-Mar-2008.) (Revised by Andrew Salmon, 11-Jul-2011.) |
⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 [𝑦 / 𝑥]𝜑) | ||
Theorem | sbralie 3391* | Implicit to explicit substitution that swaps variables in a quantified expression. (Contributed by NM, 5-Sep-2004.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ([𝑥 / 𝑦]∀𝑥 ∈ 𝑦 𝜑 ↔ ∀𝑦 ∈ 𝑥 𝜓) | ||
Theorem | rabbiia 3392 | Equivalent wff's yield equal restricted class abstractions (inference form). (Contributed by NM, 22-May-1999.) |
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓} | ||
Theorem | rabbii 3393 | Equivalent wff's correspond to equal restricted class abstractions. Inference form of rabbidv 3397. (Contributed by Peter Mazsa, 1-Nov-2019.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓} | ||
Theorem | rabbidva2 3394* | Equivalent wff's yield equal restricted class abstractions. (Contributed by Thierry Arnoux, 4-Feb-2017.) |
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒))) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | rabbia2 3395 | Equivalent wff's yield equal restricted class abstractions. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒)) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒} | ||
Theorem | rabbidva 3396* | Equivalent wff's yield equal restricted class abstractions (deduction form). (Contributed by NM, 28-Nov-2003.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒}) | ||
Theorem | rabbidv 3397* | Equivalent wff's yield equal restricted class abstractions (deduction form). (Contributed by NM, 10-Feb-1995.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒}) | ||
Theorem | rabeqf 3398 | Equality theorem for restricted class abstractions, with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by NM, 7-Mar-2004.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑}) | ||
Theorem | rabeqi 3399 | Equality theorem for restricted class abstractions. Inference form of rabeqf 3398. (Contributed by Glauco Siliprandi, 26-Jun-2021.) Avoid ax-10 2077 and ax-11 2091. (Revised by Gino Giotto, 20-Aug-2023.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑} | ||
Theorem | rabeq 3400* | Equality theorem for restricted class abstractions. (Contributed by NM, 15-Oct-2003.) Avoid ax-10 2077, ax-11 2091, ax-12 2104. (Revised by Gino Giotto, 20-Aug-2023.) |
⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜑}) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |