Home | Metamath
Proof Explorer Theorem List (p. 34 of 450) | < 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-28697) |
Hilbert Space Explorer
(28698-30220) |
Users' Mathboxes
(30221-44913) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 2rexbidva 3301* | Formula-building rule for restricted existential quantifiers (deduction form). (Contributed by NM, 15-Dec-2004.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)) | ||
Theorem | 2rexbidv 3302* | Formula-building rule for restricted existential quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)) | ||
Theorem | rexralbidv 3303* | Formula-building rule for restricted quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) | ||
Theorem | r2exlem 3304 | Lemma factoring out common proof steps in r2exf 3327 an r2ex 3305. Introduced to reduce dependencies on axioms. (Contributed by Wolf Lammen, 10-Jan-2020.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ¬ 𝜑)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)) | ||
Theorem | r2ex 3305* | Double restricted existential quantification. (Contributed by NM, 11-Nov-1995.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 10-Jan-2020.) |
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)) | ||
Theorem | rspe 3306 | Restricted specialization. (Contributed by NM, 12-Oct-1999.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rsp2e 3307 | Restricted specialization. (Contributed by FL, 4-Jun-2012.) (Proof shortened by Wolf Lammen, 7-Jan-2020.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) | ||
Theorem | nfre1 3308 | The setvar 𝑥 is not free in ∃𝑥 ∈ 𝐴𝜑. (Contributed by NM, 19-Mar-1997.) (Revised by Mario Carneiro, 7-Oct-2016.) |
⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝜑 | ||
Theorem | nfrexd 3309* | Deduction version of nfrex 3311. (Contributed by Mario Carneiro, 14-Oct-2016.) Add disjoint variable condition to avoid ax-13 2390. See nfrexdg 3310 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜓) | ||
Theorem | nfrexdg 3310 | Deduction version of nfrexg 3312. Usage of this theorem is discouraged because it depends on ax-13 2390. See nfrexd 3309 for a version with a disjoint variable condition, but not requiring ax-13 2390. (Contributed by Mario Carneiro, 14-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜓) | ||
Theorem | nfrex 3311* | 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 2390. See nfrexg 3312 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑 | ||
Theorem | nfrexg 3312 | Bound-variable hypothesis builder for restricted quantification. Usage of this theorem is discouraged because it depends on ax-13 2390. See nfrex 3311 for a version with a disjoint variable condition, but not requiring ax-13 2390. (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 | reximdai 3313 | Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 31-Aug-1999.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | reximd2a 3314 | Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by Thierry Arnoux, 27-Jan-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝑥 ∈ 𝐵) & ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜒) | ||
Theorem | r19.23t 3315 | Closed theorem form of r19.23 3316. (Contributed by NM, 4-Mar-2013.) (Revised by Mario Carneiro, 8-Oct-2016.) |
⊢ (Ⅎ𝑥𝜓 → (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓))) | ||
Theorem | r19.23 3316 | Restricted quantifier version of 19.23 2211. See r19.23v 3281 for a version requiring fewer axioms. (Contributed by NM, 22-Oct-2010.) (Proof shortened by Mario Carneiro, 8-Oct-2016.) |
⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)) | ||
Theorem | rexlimi 3317 | Restricted quantifier version of exlimi 2217. (Contributed by NM, 30-Nov-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) | ||
Theorem | rexlimd2 3318 | Version of rexlimd 3319 with deduction version of second hypothesis. (Contributed by NM, 21-Jul-2013.) (Revised by Mario Carneiro, 8-Oct-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) | ||
Theorem | rexlimd 3319 | Deduction form of rexlimd 3319. (Contributed by NM, 27-May-1998.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Proof shortened by Wolf Lammen, 14-Jan-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜒 & ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) | ||
Theorem | rexbida 3320 | Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 6-Oct-2003.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | rexbidvaALT 3321* | Alternate proof of rexbidva 3298, shorter but requires more axioms. (Contributed by NM, 9-Mar-1997.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | rexbid 3322 | Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 27-Jun-1998.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | rexbidvALT 3323* | Alternate proof of rexbidv 3299, shorter but requires more axioms. (Contributed by NM, 20-Nov-1994.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | ralrexbid 3324 | Formula-building rule for restricted existential quantifier, using a restricted universal quantifier to bind the quantified variable in the antecedent. (Contributed by AV, 21-Oct-2023.) Reduce axiom usage. (Revised by SN, 13-Nov-2023.) |
⊢ (𝜑 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜃)) | ||
Theorem | ralrexbidOLD 3325 | Obsolete version of ralrexbid 3324 as of 13-Nov-2023. (Contributed by AV, 21-Oct-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜃)) | ||
Theorem | r19.12 3326* | Restricted quantifier version of 19.12 2346. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) Avoid ax-13 2390, ax-ext 2795. (Revised by Wolf Lammen, 17-Jun-2023.) |
⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) | ||
Theorem | r2exf 3327* | Double restricted existential quantification. (Contributed by Mario Carneiro, 14-Oct-2016.) Use r2exlem 3304. (Revised by Wolf Lammen, 10-Jan-2020.) |
⊢ Ⅎ𝑦𝐴 ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)) | ||
Theorem | rexeqbii 3328 | Equality deduction for restricted existential quantifier, changing both formula and quantifier domain. Inference form. (Contributed by David Moews, 1-May-2017.) |
⊢ 𝐴 = 𝐵 & ⊢ (𝜓 ↔ 𝜒) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒) | ||
Theorem | r19.12OLD 3329* | Obsolete version of r19.12 3326 as of 19-May-2023. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) | ||
Theorem | reuanid 3330 | Cancellation law for restricted unique existential quantification. (Contributed by Peter Mazsa, 12-Feb-2018.) |
⊢ (∃!𝑥 ∈ 𝐴 (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃!𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rmoanid 3331 | Cancellation law for restricted at-most-one quantification. (Contributed by Peter Mazsa, 24-May-2018.) |
⊢ (∃*𝑥 ∈ 𝐴 (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃*𝑥 ∈ 𝐴 𝜑) | ||
Theorem | r19.29af2 3332 | A commonly used pattern based on r19.29 3256. (Contributed by Thierry Arnoux, 17-Dec-2017.) (Proof shortened by OpenAI, 25-Mar-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜒 & ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | r19.29af 3333* | A commonly used pattern based on r19.29 3256. See r19.29a 3291, r19.29an 3290 for a variant when 𝑥 is disjoint from 𝜑. (Contributed by Thierry Arnoux, 29-Nov-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | r19.29anOLD 3334* | Obsolete version of r19.29an 3290 as of 17-Jun-2023. (Contributed by Thierry Arnoux, 29-Dec-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → 𝜒) | ||
Theorem | r19.29aOLD 3335* | Obsolete proof of r19.29a 3291 as of 17-Jun-2023. (Contributed by Thierry Arnoux, 22-Nov-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | 2r19.29 3336 | Theorem r19.29 3256 with two quantifiers. (Contributed by Rodolfo Medina, 25-Sep-2010.) |
⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓)) | ||
Theorem | r19.29d2r 3337 | Theorem 19.29 of [Margaris] p. 90 with two restricted quantifiers, deduction version. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜓 ∧ 𝜒)) | ||
Theorem | r19.29vva 3338* | A commonly used pattern based on r19.29 3256, version with two restricted quantifiers. (Contributed by Thierry Arnoux, 26-Nov-2017.) (Proof shortened by Wolf Lammen, 29-Jun-2023.) |
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) → 𝜒) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | r19.29vvaOLD 3339* | Obsolete version of r19.29vva 3338 as of 28-Jun-2023. (Contributed by Thierry Arnoux, 26-Nov-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) → 𝜒) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | r19.30 3340 | Restricted quantifier version of 19.30 1882. (Contributed by Scott Fenton, 25-Feb-2011.) (Proof shortened by Wolf Lammen, 18-Jun-2023.) |
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | r19.30OLD 3341 | Obsolete version of r19.30 3340 as of 18-Jun-2023. (Contributed by Scott Fenton, 25-Feb-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | r19.32v 3342* | Restricted quantifier version of 19.32v 1941. (Contributed by NM, 25-Nov-2003.) |
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∀𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | r19.35 3343 | Restricted quantifier version of 19.35 1878. (Contributed by NM, 20-Sep-2003.) |
⊢ (∃𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | r19.36v 3344* | Restricted quantifier version of one direction of 19.36 2232. (The other direction holds iff 𝐴 is nonempty, see r19.36zv 4454.) (Contributed by NM, 22-Oct-2003.) |
⊢ (∃𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 → 𝜓)) | ||
Theorem | r19.37 3345 | Restricted quantifier version of one direction of 19.37 2234. (The other direction does not hold when 𝐴 is empty.) (Contributed by FL, 13-May-2012.) (Revised by Mario Carneiro, 11-Dec-2016.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∃𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | r19.37v 3346* | Restricted quantifier version of one direction of 19.37v 1998. (The other direction holds iff 𝐴 is nonempty, see r19.37zv 4449.) (Contributed by NM, 2-Apr-2004.) Reduce axiom usage. (Revised by Wolf Lammen, 18-Jun-2023.) |
⊢ (∃𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | r19.37vOLD 3347* | Obsolete version of r19.37v 3346 as of 18-Jun-2023. (Contributed by NM, 2-Apr-2004.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∃𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | r19.40 3348 | Restricted quantifier version of Theorem 19.40 of [Margaris] p. 90. (Contributed by NM, 2-Apr-2004.) |
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | r19.41v 3349* | Restricted quantifier version 19.41v 1950. Version of r19.41 3350 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 17-Dec-2003.) Reduce dependencies on axioms. (Revised by BJ, 29-Mar-2020.) |
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓)) | ||
Theorem | r19.41 3350 | Restricted quantifier version of 19.41 2237. See r19.41v 3349 for a version with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 1-Nov-2010.) |
⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓)) | ||
Theorem | r19.41vv 3351* | Version of r19.41v 3349 with two quantifiers. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ 𝜓)) | ||
Theorem | r19.42v 3352* | Restricted quantifier version of 19.42v 1954 (see also 19.42 2238). (Contributed by NM, 27-May-1998.) |
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | r19.43 3353 | Restricted quantifier version of 19.43 1883. (Contributed by NM, 27-May-1998.) (Proof shortened by Andrew Salmon, 30-May-2011.) |
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | r19.44v 3354* | One direction of a restricted quantifier version of 19.44 2239. The other direction holds when 𝐴 is nonempty, see r19.44zv 4451. (Contributed by NM, 2-Apr-2004.) |
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) → (∃𝑥 ∈ 𝐴 𝜑 ∨ 𝜓)) | ||
Theorem | r19.45v 3355* | Restricted quantifier version of one direction of 19.45 2240. The other direction holds when 𝐴 is nonempty, see r19.45zv 4450. (Contributed by NM, 2-Apr-2004.) |
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) → (𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | ralcom 3356* | Commutation of restricted universal quantifiers. See ralcom2 3365 for a version without disjoint variable condition on 𝑥, 𝑦. This theorem should be used in place of ralcom2 3365 since it depends on a smaller set of axioms. (Contributed by NM, 13-Oct-1999.) (Revised by Mario Carneiro, 14-Oct-2016.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rexcom 3357* | Commutation of restricted existential quantifiers. (Contributed by NM, 19-Nov-1995.) (Revised by Mario Carneiro, 14-Oct-2016.) (Proof shortened by BJ, 26-Aug-2023.) |
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rexcomOLD 3358* | Obsolete version of rexcom 3357 as of 26-Aug-2023. Commutation of restricted existential quantifiers. (Contributed by NM, 19-Nov-1995.) (Revised by Mario Carneiro, 14-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) | ||
Theorem | ralcomf 3359* | Commutation of restricted universal quantifiers. (Contributed by Mario Carneiro, 14-Oct-2016.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rexcomf 3360* | Commutation of restricted existential quantifiers. (Contributed by Mario Carneiro, 14-Oct-2016.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) | ||
Theorem | ralcom13 3361* | Swap first and third restricted universal quantifiers. (Contributed by AV, 3-Dec-2021.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 ↔ ∀𝑧 ∈ 𝐶 ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rexcom13 3362* | Swap first and third restricted existential quantifiers. (Contributed by NM, 8-Apr-2015.) |
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝜑 ↔ ∃𝑧 ∈ 𝐶 ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) | ||
Theorem | ralrot3 3363* | Rotate three restricted universal quantifiers. (Contributed by AV, 3-Dec-2021.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 ↔ ∀𝑧 ∈ 𝐶 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑) | ||
Theorem | rexrot4 3364* | Rotate four restricted existential quantifiers twice. (Contributed by NM, 8-Apr-2015.) |
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 ∃𝑤 ∈ 𝐷 𝜑 ↔ ∃𝑧 ∈ 𝐶 ∃𝑤 ∈ 𝐷 ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) | ||
Theorem | ralcom2 3365* | 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 2795 and it should no longer be used. Usage of ralcom 3356 is highly encouraged. (Contributed by NM, 24-Nov-1994.) (Proof shortened by Mario Carneiro, 17-Oct-2016.) (New usage is discouraged.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝜑 → ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | ralcom3 3366 | A commutation law for restricted universal quantifiers that swaps the domains of the restriction. (Contributed by NM, 22-Feb-2004.) |
⊢ (∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝐵 → 𝜑) ↔ ∀𝑥 ∈ 𝐵 (𝑥 ∈ 𝐴 → 𝜑)) | ||
Theorem | reeanlem 3367* | Lemma factoring out common proof steps of reeanv 3369 and reean 3368. (Contributed by Wolf Lammen, 20-Aug-2023.) |
⊢ (∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝑦 ∈ 𝐵 ∧ 𝜓)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜓))) ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | reean 3368* | Rearrange restricted existential quantifiers. (Contributed by NM, 27-Oct-2010.) (Proof shortened by Andrew Salmon, 30-May-2011.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | reeanv 3369* | Rearrange restricted existential quantifiers. (Contributed by NM, 9-May-1999.) |
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | 3reeanv 3370* | Rearrange three restricted existential quantifiers. (Contributed by Jeff Madsen, 11-Jun-2010.) |
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓 ∧ ∃𝑧 ∈ 𝐶 𝜒)) | ||
Theorem | 2ralor 3371* | Distribute restricted universal quantification over "or". (Contributed by Jeff Madsen, 19-Jun-2010.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∨ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∨ ∀𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | nfreu1 3372 | The setvar 𝑥 is not free in ∃!𝑥 ∈ 𝐴𝜑. (Contributed by NM, 19-Mar-1997.) |
⊢ Ⅎ𝑥∃!𝑥 ∈ 𝐴 𝜑 | ||
Theorem | nfrmo1 3373 | The setvar 𝑥 is not free in ∃*𝑥 ∈ 𝐴𝜑. (Contributed by NM, 16-Jun-2017.) |
⊢ Ⅎ𝑥∃*𝑥 ∈ 𝐴 𝜑 | ||
Theorem | nfreud 3374 | Deduction version of nfreu 3378. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 15-Feb-2013.) (Revised by Mario Carneiro, 8-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∃!𝑦 ∈ 𝐴 𝜓) | ||
Theorem | nfrmod 3375 | Deduction version of nfrmo 3379. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 17-Jun-2017.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∃*𝑦 ∈ 𝐴 𝜓) | ||
Theorem | nfreuw 3376* | Bound-variable hypothesis builder for restricted unique existence. Version of nfreu 3378 with a disjoint variable condition, which does not require ax-13 2390. (Contributed by NM, 30-Oct-2010.) (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∃!𝑦 ∈ 𝐴 𝜑 | ||
Theorem | nfrmow 3377* | Bound-variable hypothesis builder for restricted uniqueness. Version of nfrmo 3379 with a disjoint variable condition, which does not require ax-13 2390. (Contributed by NM, 16-Jun-2017.) (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∃*𝑦 ∈ 𝐴 𝜑 | ||
Theorem | nfreu 3378 | Bound-variable hypothesis builder for restricted unique existence. Usage of this theorem is discouraged because it depends on ax-13 2390. Use the weaker nfreuw 3376 when possible. (Contributed by NM, 30-Oct-2010.) (Revised by Mario Carneiro, 8-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∃!𝑦 ∈ 𝐴 𝜑 | ||
Theorem | nfrmo 3379 | Bound-variable hypothesis builder for restricted uniqueness. Usage of this theorem is discouraged because it depends on ax-13 2390. Use the weaker nfrmow 3377 when possible. (Contributed by NM, 16-Jun-2017.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∃*𝑦 ∈ 𝐴 𝜑 | ||
Theorem | rabid 3380 | 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 3381 | Abstract builder restricted to another restricted abstract builder. (Contributed by Thierry Arnoux, 30-Aug-2017.) |
⊢ {𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)} | ||
Theorem | rabidim1 3382 | Membership in a restricted abstraction, implication. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} → 𝑥 ∈ 𝐴) | ||
Theorem | rabid2 3383* | An "identity" law for restricted class abstraction. (Contributed by NM, 9-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) |
⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rabid2f 3384 | 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 3385 | Equivalent wff's correspond to equal restricted class abstractions. Closed theorem form of rabbidva 3480. (Contributed by NM, 25-Nov-2013.) |
⊢ (∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝜒) ↔ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒}) | ||
Theorem | nfrab1 3386 | The abstraction variable in a restricted class abstraction isn't free. (Contributed by NM, 19-Mar-1997.) |
⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 𝜑} | ||
Theorem | nfrabw 3387* | A variable not free in a wff remains so in a restricted class abstraction. Version of nfrab 3388 with a disjoint variable condition, which does not require ax-13 2390. (Contributed by NM, 13-Oct-2003.) (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝜑} | ||
Theorem | nfrab 3388 | A variable not free in a wff remains so in a restricted class abstraction. Usage of this theorem is discouraged because it depends on ax-13 2390. Use the weaker nfrabw 3387 when possible. (Contributed by NM, 13-Oct-2003.) (Revised by Mario Carneiro, 9-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝜑} | ||
Theorem | reubida 3389 | Formula-building rule for restricted existential quantifier (deduction form). (Contributed by Mario Carneiro, 19-Nov-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | reubidva 3390* | 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 | reubidv 3391* | Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 17-Oct-1996.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | reubiia 3392 | Formula-building rule for restricted existential quantifier (inference form). (Contributed by NM, 14-Nov-2004.) |
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜓) | ||
Theorem | reubii 3393 | Formula-building rule for restricted existential quantifier (inference form). (Contributed by NM, 22-Oct-1999.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜓) | ||
Theorem | rmobida 3394 | Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 16-Jun-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | rmobidva 3395* | Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 16-Jun-2017.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | rmobidv 3396* | Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 16-Jun-2017.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | rmobiia 3397 | Formula-building rule for restricted existential quantifier (inference form). (Contributed by NM, 16-Jun-2017.) |
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐴 𝜓) | ||
Theorem | rmobii 3398 | Formula-building rule for restricted existential quantifier (inference form). (Contributed by NM, 16-Jun-2017.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥 ∈ 𝐴 𝜓) | ||
Theorem | raleqf 3399 | 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 3400 | 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.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |