Home | Metamath
Proof Explorer Theorem List (p. 33 of 465) | < 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-29276) |
Hilbert Space Explorer
(29277-30799) |
Users' Mathboxes
(30800-46482) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | reximdv2 3201* | Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 17-Sep-2003.) |
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) → (𝑥 ∈ 𝐵 ∧ 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐵 𝜒)) | ||
Theorem | reximdvai 3202* | Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 14-Nov-2002.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 8-Jan-2020.) (Proof shortened by Wolf Lammen, 4-Nov-2024.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | reximdvaiOLD 3203* | Obsolete version of reximdvai 3202 as of 3-Nov-2024. (Contributed by NM, 14-Nov-2002.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 8-Jan-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | reximdv 3204* | Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version with strong hypothesis.) (Contributed by NM, 24-Jun-1998.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | reximdva 3205* | Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | reximddv 3206* | Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Thierry Arnoux, 7-Dec-2016.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝜒) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒) | ||
Theorem | reximssdv 3207* | Derivation of a restricted existential quantification over a subset (the second hypothesis implies 𝐴 ⊆ 𝐵), deduction form. (Contributed by AV, 21-Aug-2022.) |
⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝜓)) → 𝑥 ∈ 𝐴) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝜓)) → 𝜒) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒) | ||
Theorem | reximdvva 3208* | Deduction doubly quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by AV, 5-Jan-2022.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)) | ||
Theorem | reximddv2 3209* | Double deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) → 𝜒) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒) | ||
Theorem | r19.23v 3210* | Restricted quantifier version of 19.23v 1949. Version of r19.23 3245 with a disjoint variable condition. (Contributed by NM, 31-Aug-1999.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2020.) |
⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)) | ||
Theorem | rexlimiv 3211* | Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2020.) |
⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) | ||
Theorem | rexlimiva 3212* | Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 18-Dec-2006.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) | ||
Theorem | rexlimivw 3213* | Weaker version of rexlimiv 3211. (Contributed by FL, 19-Sep-2011.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) | ||
Theorem | rexlimdv 3214* | Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 14-Nov-2002.) (Proof shortened by Eric Schmidt, 22-Dec-2006.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2020.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) | ||
Theorem | rexlimdva 3215* | Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 20-Jan-2007.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) | ||
Theorem | rexlimdvaa 3216* | Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by Mario Carneiro, 15-Jun-2016.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝜒) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) | ||
Theorem | rexlimdv3a 3217* | Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). Frequently-used variant of rexlimdv 3214. (Contributed by NM, 7-Jun-2015.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝜓) → 𝜒) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) | ||
Theorem | rexlimdva2 3218* | Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) | ||
Theorem | r19.29an 3219* | A commonly used pattern in the spirit of r19.29 3186. (Contributed by Thierry Arnoux, 29-Dec-2019.) (Proof shortened by Wolf Lammen, 17-Jun-2023.) |
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → 𝜒) | ||
Theorem | r19.29a 3220* | A commonly used pattern in the spirit of r19.29 3186. (Contributed by Thierry Arnoux, 22-Nov-2017.) Reduce axiom usage. (Revised by Wolf Lammen, 17-Jun-2023.) |
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | rexlimdvw 3221* | Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 18-Jun-2014.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) | ||
Theorem | rexlimddv 3222* | Restricted existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 15-Jun-2016.) |
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝜒) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | rexlimivv 3223* | Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 17-Feb-2004.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜑 → 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → 𝜓) | ||
Theorem | rexlimdvv 3224* | Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Jul-2004.) |
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒)) | ||
Theorem | rexlimdvva 3225* | Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒)) | ||
Theorem | rexbidv2 3226* | Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 22-May-1999.) |
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒)) | ||
Theorem | rexbidva 3227* | Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 9-Mar-1997.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 6-Dec-2019.) (Proof shortened by Wolf Lammen, 10-Dec-2019.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | rexbidv 3228* | Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 20-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 6-Dec-2019.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | 2rexbiia 3229* | Inference adding two restricted existential quantifiers to both sides of an equivalence. (Contributed by NM, 1-Aug-2004.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) | ||
Theorem | 2rexbidva 3230* | Formula-building rule for restricted existential quantifiers (deduction form). (Contributed by NM, 15-Dec-2004.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)) | ||
Theorem | 2rexbidv 3231* | Formula-building rule for restricted existential quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)) | ||
Theorem | rexralbidv 3232* | Formula-building rule for restricted quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) | ||
Theorem | r2exlem 3233 | Lemma factoring out common proof steps in r2exf 3257 an r2ex 3234. Introduced to reduce dependencies on axioms. (Contributed by Wolf Lammen, 10-Jan-2020.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ¬ 𝜑)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)) | ||
Theorem | r2ex 3234* | Double restricted existential quantification. (Contributed by NM, 11-Nov-1995.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 10-Jan-2020.) |
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)) | ||
Theorem | rspe 3235 | Restricted specialization. (Contributed by NM, 12-Oct-1999.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rsp2e 3236 | Restricted specialization. (Contributed by FL, 4-Jun-2012.) (Proof shortened by Wolf Lammen, 7-Jan-2020.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) | ||
Theorem | nfre1 3237 | The setvar 𝑥 is not free in ∃𝑥 ∈ 𝐴𝜑. (Contributed by NM, 19-Mar-1997.) (Revised by Mario Carneiro, 7-Oct-2016.) |
⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝜑 | ||
Theorem | nfrexd 3238* | Deduction version of nfrex 3240. (Contributed by Mario Carneiro, 14-Oct-2016.) Add disjoint variable condition to avoid ax-13 2374. See nfrexdg 3239 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜓) | ||
Theorem | nfrexdg 3239 | Deduction version of nfrexg 3241. Usage of this theorem is discouraged because it depends on ax-13 2374. See nfrexd 3238 for a version with a disjoint variable condition, but not requiring ax-13 2374. (Contributed by Mario Carneiro, 14-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜓) | ||
Theorem | nfrex 3240* | 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 2374. See nfrexg 3241 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑 | ||
Theorem | nfrexg 3241 | Bound-variable hypothesis builder for restricted quantification. Usage of this theorem is discouraged because it depends on ax-13 2374. See nfrex 3240 for a version with a disjoint variable condition, but not requiring ax-13 2374. (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 3242 | Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 31-Aug-1999.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | reximd2a 3243 | 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 3244 | Closed theorem form of r19.23 3245. (Contributed by NM, 4-Mar-2013.) (Revised by Mario Carneiro, 8-Oct-2016.) |
⊢ (Ⅎ𝑥𝜓 → (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓))) | ||
Theorem | r19.23 3245 | Restricted quantifier version of 19.23 2208. See r19.23v 3210 for a version requiring fewer axioms. (Contributed by NM, 22-Oct-2010.) (Proof shortened by Mario Carneiro, 8-Oct-2016.) |
⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)) | ||
Theorem | rexlimi 3246 | Restricted quantifier version of exlimi 2214. (Contributed by NM, 30-Nov-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) | ||
Theorem | rexlimd2 3247 | Version of rexlimd 3248 with deduction version of second hypothesis. (Contributed by NM, 21-Jul-2013.) (Revised by Mario Carneiro, 8-Oct-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) | ||
Theorem | rexlimd 3248 | Deduction form of rexlimd 3248. (Contributed by NM, 27-May-1998.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Proof shortened by Wolf Lammen, 14-Jan-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜒 & ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) | ||
Theorem | rexbida 3249 | Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 6-Oct-2003.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | rexbidvaALT 3250* | Alternate proof of rexbidva 3227, shorter but requires more axioms. (Contributed by NM, 9-Mar-1997.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | rexbid 3251 | Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 27-Jun-1998.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | rexbidvALT 3252* | Alternate proof of rexbidv 3228, shorter but requires more axioms. (Contributed by NM, 20-Nov-1994.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | ralrexbid 3253 | 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.) (Proof shortened by Wolf Lammen, 4-Nov-2024.) |
⊢ (𝜑 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜃)) | ||
Theorem | ralrexbidOLD 3254 | Obsolete version of ralrexbid 3253 as of 4-Nov-2024. (Contributed by AV, 21-Oct-2023.) Reduce axiom usage. (Revised by SN, 13-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜃)) | ||
Theorem | r19.12 3255* | Restricted quantifier version of 19.12 2325. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) Avoid ax-13 2374, ax-ext 2711. (Revised by Wolf Lammen, 17-Jun-2023.) (Proof shortened by Wolf Lammen, 4-Nov-2024.) |
⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) | ||
Theorem | r19.12OLD 3256* | Obsolete version of 19.12 2325 as of 4-Nov-2024. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) Avoid ax-13 2374, ax-ext 2711. (Revised by Wolf Lammen, 17-Jun-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) | ||
Theorem | r2exf 3257* | Double restricted existential quantification. (Contributed by Mario Carneiro, 14-Oct-2016.) Use r2exlem 3233. (Revised by Wolf Lammen, 10-Jan-2020.) |
⊢ Ⅎ𝑦𝐴 ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)) | ||
Theorem | rexeqbii 3258 | Equality deduction for restricted existential quantifier, changing both formula and quantifier domain. Inference form. (Contributed by David Moews, 1-May-2017.) |
⊢ 𝐴 = 𝐵 & ⊢ (𝜓 ↔ 𝜒) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒) | ||
Theorem | reuanid 3259 | Cancellation law for restricted unique existential quantification. (Contributed by Peter Mazsa, 12-Feb-2018.) |
⊢ (∃!𝑥 ∈ 𝐴 (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃!𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rmoanid 3260 | Cancellation law for restricted at-most-one quantification. (Contributed by Peter Mazsa, 24-May-2018.) |
⊢ (∃*𝑥 ∈ 𝐴 (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃*𝑥 ∈ 𝐴 𝜑) | ||
Theorem | r19.29af2 3261 | A commonly used pattern based on r19.29 3186. (Contributed by Thierry Arnoux, 17-Dec-2017.) (Proof shortened by OpenAI, 25-Mar-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜒 & ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | r19.29af 3262* | A commonly used pattern based on r19.29 3186. See r19.29a 3220, r19.29an 3219 for a variant when 𝑥 is disjoint from 𝜑. (Contributed by Thierry Arnoux, 29-Nov-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | 2r19.29 3263 | Theorem r19.29 3186 with two quantifiers. (Contributed by Rodolfo Medina, 25-Sep-2010.) |
⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓)) | ||
Theorem | r19.29d2r 3264 | Theorem 19.29 of [Margaris] p. 90 with two restricted quantifiers, deduction version. (Contributed by Thierry Arnoux, 30-Jan-2017.) (Proof shortened by Wolf Lammen, 4-Nov-2024.) |
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜓 ∧ 𝜒)) | ||
Theorem | r19.29d2rOLD 3265 | Obsolete version of r19.29d2r 3264 as of 4-Nov-2024. (Contributed by Thierry Arnoux, 30-Jan-2017.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜓 ∧ 𝜒)) | ||
Theorem | r19.29vva 3266* | A commonly used pattern based on r19.29 3186, version with two restricted quantifiers. (Contributed by Thierry Arnoux, 26-Nov-2017.) (Proof shortened by Wolf Lammen, 4-Nov-2024.) |
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) → 𝜒) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | r19.29vvaOLD 3267* | Obsolete version of r19.29vva 3266 as of 4-Nov-2024. (Contributed by Thierry Arnoux, 26-Nov-2017.) (Proof shortened by Wolf Lammen, 29-Jun-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) → 𝜒) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | r19.30 3268 | Restricted quantifier version of 19.30 1888. (Contributed by Scott Fenton, 25-Feb-2011.) (Proof shortened by Wolf Lammen, 5-Nov-2024.) |
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | r19.30OLD 3269 | Obsolete version of 19.30 1888 as of 5-Nov-2024. (Contributed by Scott Fenton, 25-Feb-2011.) (Proof shortened by Wolf Lammen, 18-Jun-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | r19.32v 3270* | Restricted quantifier version of 19.32v 1947. (Contributed by NM, 25-Nov-2003.) |
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∀𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | r19.35 3271 | Restricted quantifier version of 19.35 1884. (Contributed by NM, 20-Sep-2003.) |
⊢ (∃𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | r19.36v 3272* | Restricted quantifier version of one direction of 19.36 2227. (The other direction holds iff 𝐴 is nonempty, see r19.36zv 4443.) (Contributed by NM, 22-Oct-2003.) |
⊢ (∃𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 → 𝜓)) | ||
Theorem | r19.37 3273 | Restricted quantifier version of one direction of 19.37 2229. (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 3274* | Restricted quantifier version of one direction of 19.37v 1999. (The other direction holds iff 𝐴 is nonempty, see r19.37zv 4438.) (Contributed by NM, 2-Apr-2004.) Reduce axiom usage. (Revised by Wolf Lammen, 18-Jun-2023.) |
⊢ (∃𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | r19.40 3275 | Restricted quantifier version of Theorem 19.40 of [Margaris] p. 90. (Contributed by NM, 2-Apr-2004.) |
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | r19.41v 3276* | Restricted quantifier version 19.41v 1957. Version of r19.41 3277 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 3277 | Restricted quantifier version of 19.41 2232. See r19.41v 3276 for a version with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 1-Nov-2010.) |
⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓)) | ||
Theorem | r19.41vv 3278* | Version of r19.41v 3276 with two quantifiers. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ 𝜓)) | ||
Theorem | r19.42v 3279* | Restricted quantifier version of 19.42v 1961 (see also 19.42 2233). (Contributed by NM, 27-May-1998.) |
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | r19.43 3280 | Restricted quantifier version of 19.43 1889. (Contributed by NM, 27-May-1998.) (Proof shortened by Andrew Salmon, 30-May-2011.) |
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | r19.44v 3281* | One direction of a restricted quantifier version of 19.44 2234. The other direction holds when 𝐴 is nonempty, see r19.44zv 4440. (Contributed by NM, 2-Apr-2004.) |
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) → (∃𝑥 ∈ 𝐴 𝜑 ∨ 𝜓)) | ||
Theorem | r19.45v 3282* | Restricted quantifier version of one direction of 19.45 2235. The other direction holds when 𝐴 is nonempty, see r19.45zv 4439. (Contributed by NM, 2-Apr-2004.) |
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) → (𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | ralcom 3283* | Commutation of restricted universal quantifiers. See ralcom2 3291 for a version without disjoint variable condition on 𝑥, 𝑦. This theorem should be used in place of ralcom2 3291 since it depends on a smaller set of axioms. (Contributed by NM, 13-Oct-1999.) (Revised by Mario Carneiro, 14-Oct-2016.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rexcom 3284* | 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 | ralcomf 3285* | Commutation of restricted universal quantifiers. (Contributed by Mario Carneiro, 14-Oct-2016.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rexcomf 3286* | Commutation of restricted existential quantifiers. (Contributed by Mario Carneiro, 14-Oct-2016.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) | ||
Theorem | ralcom13 3287* | Swap first and third restricted universal quantifiers. (Contributed by AV, 3-Dec-2021.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 ↔ ∀𝑧 ∈ 𝐶 ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rexcom13 3288* | Swap first and third restricted existential quantifiers. (Contributed by NM, 8-Apr-2015.) |
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝜑 ↔ ∃𝑧 ∈ 𝐶 ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) | ||
Theorem | ralrot3 3289* | Rotate three restricted universal quantifiers. (Contributed by AV, 3-Dec-2021.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 ↔ ∀𝑧 ∈ 𝐶 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑) | ||
Theorem | rexrot4 3290* | Rotate four restricted existential quantifiers twice. (Contributed by NM, 8-Apr-2015.) |
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 ∃𝑤 ∈ 𝐷 𝜑 ↔ ∃𝑧 ∈ 𝐶 ∃𝑤 ∈ 𝐷 ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) | ||
Theorem | ralcom2 3291* | 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 2711 and it should no longer be used. Usage of ralcom 3283 is highly encouraged. (Contributed by NM, 24-Nov-1994.) (Proof shortened by Mario Carneiro, 17-Oct-2016.) (New usage is discouraged.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝜑 → ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | ralcom3 3292 | A commutation law for restricted universal quantifiers that swaps the domains of the restriction. (Contributed by NM, 22-Feb-2004.) |
⊢ (∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝐵 → 𝜑) ↔ ∀𝑥 ∈ 𝐵 (𝑥 ∈ 𝐴 → 𝜑)) | ||
Theorem | reeanlem 3293* | Lemma factoring out common proof steps of reeanv 3295 and reean 3294. (Contributed by Wolf Lammen, 20-Aug-2023.) |
⊢ (∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝑦 ∈ 𝐵 ∧ 𝜓)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜓))) ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | reean 3294* | Rearrange restricted existential quantifiers. (Contributed by NM, 27-Oct-2010.) (Proof shortened by Andrew Salmon, 30-May-2011.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | reeanv 3295* | Rearrange restricted existential quantifiers. (Contributed by NM, 9-May-1999.) |
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | 3reeanv 3296* | Rearrange three restricted existential quantifiers. (Contributed by Jeff Madsen, 11-Jun-2010.) |
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓 ∧ ∃𝑧 ∈ 𝐶 𝜒)) | ||
Theorem | 2ralor 3297* | Distribute restricted universal quantification over "or". (Contributed by Jeff Madsen, 19-Jun-2010.) (Proof shortened by Wolf Lammen, 20-Nov-2024.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∨ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∨ ∀𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | 2ralorOLD 3298* | Obsolete version of 2ralor 3297 as of 20-Nov-2024. (Contributed by Jeff Madsen, 19-Jun-2010.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∨ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∨ ∀𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | nfreu1 3299 | The setvar 𝑥 is not free in ∃!𝑥 ∈ 𝐴𝜑. (Contributed by NM, 19-Mar-1997.) |
⊢ Ⅎ𝑥∃!𝑥 ∈ 𝐴 𝜑 | ||
Theorem | nfrmo1 3300 | The setvar 𝑥 is not free in ∃*𝑥 ∈ 𝐴𝜑. (Contributed by NM, 16-Jun-2017.) |
⊢ Ⅎ𝑥∃*𝑥 ∈ 𝐴 𝜑 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |