![]() |
Metamath
Proof Explorer Theorem List (p. 33 of 480) | < 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-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ralrimivvva 3201* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with triple quantification.) (Contributed by Mario Carneiro, 9-Jul-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶)) → 𝜓) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓) | ||
Theorem | ralimdvva 3202* | Deduction doubly quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90 (alim 1810). (Contributed by AV, 27-Nov-2019.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) | ||
Theorem | reximdvva 3203* | Deduction doubly quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by AV, 5-Jan-2022.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)) | ||
Theorem | ralimdvv 3204* | Deduction doubly quantifying both antecedent and consequent. (Contributed by Scott Fenton, 2-Mar-2025.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) | ||
Theorem | ralimd4v 3205* | Deduction quadrupally quantifying both antecedent and consequent. (Contributed by Scott Fenton, 2-Mar-2025.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 𝜓 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 𝜒)) | ||
Theorem | ralimd6v 3206* | Deduction sextupally quantifying both antecedent and consequent. (Contributed by Scott Fenton, 5-Mar-2025.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 ∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 𝜓 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 ∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 𝜒)) | ||
Theorem | ralrimdvva 3207* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by NM, 2-Feb-2008.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) | ||
Theorem | rexlimdvv 3208* | Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Jul-2004.) |
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒)) | ||
Theorem | rexlimdvva 3209* | Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒)) | ||
Theorem | reximddv2 3210* | Double deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) → 𝜒) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒) | ||
Theorem | r19.29vva 3211* | A commonly used pattern based on r19.29 3112, version with two restricted quantifiers. (Contributed by Thierry Arnoux, 26-Nov-2017.) (Proof shortened by Wolf Lammen, 4-Nov-2024.) |
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) → 𝜒) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | r19.29vvaOLD 3212* | Obsolete version of r19.29vva 3211 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 | 2rexbiia 3213* | Inference adding two restricted existential quantifiers to both sides of an equivalence. (Contributed by NM, 1-Aug-2004.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) | ||
Theorem | 2ralbidva 3214* | Formula-building rule for restricted universal quantifiers (deduction form). (Contributed by NM, 4-Mar-1997.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 9-Dec-2019.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) | ||
Theorem | 2rexbidva 3215* | Formula-building rule for restricted existential quantifiers (deduction form). (Contributed by NM, 15-Dec-2004.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)) | ||
Theorem | 2ralbidv 3216* | Formula-building rule for restricted universal quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.) (Revised by Szymon Jaroszewicz, 16-Mar-2007.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) | ||
Theorem | 2rexbidv 3217* | Formula-building rule for restricted existential quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)) | ||
Theorem | rexralbidv 3218* | Formula-building rule for restricted quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) | ||
Theorem | 3ralbidv 3219* | Formula-building rule for restricted universal quantifiers (deduction form.) (Contributed by Scott Fenton, 20-Feb-2025.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜒)) | ||
Theorem | 4ralbidv 3220* | Formula-building rule for restricted universal quantifiers (deduction form.) (Contributed by Scott Fenton, 20-Feb-2025.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 𝜒)) | ||
Theorem | 6ralbidv 3221* | Formula-building rule for restricted universal quantifiers (deduction form.) (Contributed by Scott Fenton, 5-Mar-2025.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 ∀𝑡 ∈ 𝐸 ∀𝑢 ∈ 𝐹 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 ∀𝑡 ∈ 𝐸 ∀𝑢 ∈ 𝐹 𝜒)) | ||
Theorem | r19.41vv 3222* | Version of r19.41v 3186 with two quantifiers. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ 𝜓)) | ||
Theorem | reeanlem 3223* | Lemma factoring out common proof steps of reeanv 3224 and reean 3311. (Contributed by Wolf Lammen, 20-Aug-2023.) |
⊢ (∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝑦 ∈ 𝐵 ∧ 𝜓)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜓))) ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | reeanv 3224* | Rearrange restricted existential quantifiers. (Contributed by NM, 9-May-1999.) |
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | 3reeanv 3225* | Rearrange three restricted existential quantifiers. (Contributed by Jeff Madsen, 11-Jun-2010.) |
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓 ∧ ∃𝑧 ∈ 𝐶 𝜒)) | ||
Theorem | 2ralor 3226* | Distribute restricted universal quantification over "or". (Contributed by Jeff Madsen, 19-Jun-2010.) (Proof shortened by Wolf Lammen, 20-Nov-2024.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∨ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∨ ∀𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | 2ralorOLD 3227* | Obsolete version of 2ralor 3226 as of 20-Nov-2024. (Contributed by Jeff Madsen, 19-Jun-2010.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∨ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∨ ∀𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | risset 3228* | Two ways to say "𝐴 belongs to 𝐵". (Contributed by NM, 22-Nov-1994.) |
⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝑥 = 𝐴) | ||
Theorem | nelb 3229* | A definition of ¬ 𝐴 ∈ 𝐵. (Contributed by Thierry Arnoux, 20-Nov-2023.) (Proof shortened by SN, 23-Jan-2024.) (Proof shortened by Wolf Lammen, 3-Nov-2024.) |
⊢ (¬ 𝐴 ∈ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝑥 ≠ 𝐴) | ||
Theorem | nelbOLD 3230* | Obsolete version of nelb 3229 as of 3-Nov-2024. (Contributed by Thierry Arnoux, 20-Nov-2023.) (Proof shortened by SN, 23-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ 𝐴 ∈ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝑥 ≠ 𝐴) | ||
Theorem | rspw 3231* | Restricted specialization. Weak version of rsp 3242, requiring ax-8 2106, but not ax-12 2169. (Contributed by Gino Giotto, 3-Oct-2024.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝑥 ∈ 𝐴 → 𝜑)) | ||
Theorem | cbvralvw 3232* | Change the bound variable of a restricted universal quantifier using implicit substitution. Version of cbvralv 3358 with a disjoint variable condition, which does not require ax-10 2135, ax-11 2152, ax-12 2169, ax-13 2369. (Contributed by NM, 28-Jan-1997.) Avoid ax-13 2369. (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvrexvw 3233* | Change the bound variable of a restricted existential quantifier using implicit substitution. Version of cbvrexv 3359 with a disjoint variable condition, which does not require ax-10 2135, ax-11 2152, ax-12 2169, ax-13 2369. (Contributed by NM, 2-Jun-1998.) Avoid ax-13 2369. (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvraldva 3234* | Rule used to change the bound variable in a restricted universal quantifier with implicit substitution. Deduction form. (Contributed by David Moews, 1-May-2017.) Avoid ax-9 2114, ax-ext 2701. (Revised by Wolf Lammen, 9-Mar-2025.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑦 ∈ 𝐴 𝜒)) | ||
Theorem | cbvrexdva 3235* | Rule used to change the bound variable in a restricted existential quantifier with implicit substitution. Deduction form. (Contributed by David Moews, 1-May-2017.) Avoid ax-9 2114, ax-ext 2701. (Revised by Wolf Lammen, 9-Mar-2025.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑦 ∈ 𝐴 𝜒)) | ||
Theorem | cbvral2vw 3236* | Change bound variables of double restricted universal quantification, using implicit substitution. Version of cbvral2v 3362 with a disjoint variable condition, which does not require ax-13 2369. (Contributed by NM, 10-Aug-2004.) Avoid ax-13 2369. (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 𝜓) | ||
Theorem | cbvrex2vw 3237* | Change bound variables of double restricted universal quantification, using implicit substitution. Version of cbvrex2v 3363 with a disjoint variable condition, which does not require ax-13 2369. (Contributed by FL, 2-Jul-2012.) Avoid ax-13 2369. (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝑤 → (𝜒 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝜓) | ||
Theorem | cbvral3vw 3238* | Change bound variables of triple restricted universal quantification, using implicit substitution. Version of cbvral3v 3364 with a disjoint variable condition, which does not require ax-13 2369. (Contributed by NM, 10-May-2005.) Avoid ax-13 2369. (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ (𝑥 = 𝑤 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝑣 → (𝜒 ↔ 𝜃)) & ⊢ (𝑧 = 𝑢 → (𝜃 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 ↔ ∀𝑤 ∈ 𝐴 ∀𝑣 ∈ 𝐵 ∀𝑢 ∈ 𝐶 𝜓) | ||
Theorem | cbvral4vw 3239* | Change bound variables of quadruple restricted universal quantification, using implicit substitution. (Contributed by Scott Fenton, 2-Mar-2025.) |
⊢ (𝑥 = 𝑎 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝑏 → (𝜒 ↔ 𝜃)) & ⊢ (𝑧 = 𝑐 → (𝜃 ↔ 𝜏)) & ⊢ (𝑤 = 𝑑 → (𝜏 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 𝜑 ↔ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐶 ∀𝑑 ∈ 𝐷 𝜓) | ||
Theorem | cbvral6vw 3240* | Change bound variables of sextuple restricted universal quantification, using implicit substitution. (Contributed by Scott Fenton, 5-Mar-2025.) |
⊢ (𝑥 = 𝑎 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝑏 → (𝜒 ↔ 𝜃)) & ⊢ (𝑧 = 𝑐 → (𝜃 ↔ 𝜏)) & ⊢ (𝑤 = 𝑑 → (𝜏 ↔ 𝜂)) & ⊢ (𝑝 = 𝑒 → (𝜂 ↔ 𝜁)) & ⊢ (𝑞 = 𝑓 → (𝜁 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 ∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 𝜑 ↔ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐶 ∀𝑑 ∈ 𝐷 ∀𝑒 ∈ 𝐸 ∀𝑓 ∈ 𝐹 𝜓) | ||
Theorem | cbvral8vw 3241* | Change bound variables of octuple restricted universal quantification, using implicit substitution. (Contributed by Scott Fenton, 2-Mar-2025.) |
⊢ (𝑥 = 𝑎 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = 𝑏 → (𝜒 ↔ 𝜃)) & ⊢ (𝑧 = 𝑐 → (𝜃 ↔ 𝜏)) & ⊢ (𝑤 = 𝑑 → (𝜏 ↔ 𝜂)) & ⊢ (𝑝 = 𝑒 → (𝜂 ↔ 𝜁)) & ⊢ (𝑞 = 𝑓 → (𝜁 ↔ 𝜎)) & ⊢ (𝑟 = 𝑔 → (𝜎 ↔ 𝜌)) & ⊢ (𝑠 = ℎ → (𝜌 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 ∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 ∀𝑟 ∈ 𝐺 ∀𝑠 ∈ 𝐻 𝜑 ↔ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐶 ∀𝑑 ∈ 𝐷 ∀𝑒 ∈ 𝐸 ∀𝑓 ∈ 𝐹 ∀𝑔 ∈ 𝐺 ∀ℎ ∈ 𝐻 𝜓) | ||
Theorem | rsp 3242 | Restricted specialization. (Contributed by NM, 17-Oct-1996.) |
⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝑥 ∈ 𝐴 → 𝜑)) | ||
Theorem | rspa 3243 | Restricted specialization. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜑) | ||
Theorem | rspe 3244 | Restricted specialization. (Contributed by NM, 12-Oct-1999.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rspec 3245 | Specialization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.) |
⊢ ∀𝑥 ∈ 𝐴 𝜑 ⇒ ⊢ (𝑥 ∈ 𝐴 → 𝜑) | ||
Theorem | r19.21bi 3246 | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.) (Proof shortened by Wolf Lammen, 11-Jun-2023.) |
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓) | ||
Theorem | r19.21be 3247 | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 21-Nov-1994.) |
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) | ||
Theorem | r19.21t 3248 | Restricted quantifier version of 19.21t 2197; closed form of r19.21 3249. (Contributed by NM, 1-Mar-2008.) (Proof shortened by Wolf Lammen, 2-Jan-2020.) |
⊢ (Ⅎ𝑥𝜑 → (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))) | ||
Theorem | r19.21 3249 | Restricted quantifier version of 19.21 2198. (Contributed by Scott Fenton, 30-Mar-2011.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | r19.23t 3250 | Closed theorem form of r19.23 3251. (Contributed by NM, 4-Mar-2013.) (Revised by Mario Carneiro, 8-Oct-2016.) |
⊢ (Ⅎ𝑥𝜓 → (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓))) | ||
Theorem | r19.23 3251 | Restricted quantifier version of 19.23 2202. See r19.23v 3180 for a version requiring fewer axioms. (Contributed by NM, 22-Oct-2010.) (Proof shortened by Mario Carneiro, 8-Oct-2016.) |
⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)) | ||
Theorem | ralrimi 3252 | Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). For a version based on fewer axioms see ralrimiv 3143. (Contributed by NM, 10-Oct-1999.) Shortened after introduction of hbralrimi 3142. (Revised by Wolf Lammen, 4-Dec-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓)) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) | ||
Theorem | ralrimia 3253 | Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) | ||
Theorem | rexlimi 3254 | Restricted quantifier version of exlimi 2208. For a version based on fewer axioms see rexlimiv 3146. (Contributed by NM, 30-Nov-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) | ||
Theorem | ralimdaa 3255 | Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 22-Sep-2003.) (Proof shortened by Wolf Lammen, 29-Dec-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | reximdai 3256 | Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 31-Aug-1999.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | r19.37 3257 | Restricted quantifier version of one direction of 19.37 2223. (The other direction does not hold when 𝐴 is empty.) (Contributed by FL, 13-May-2012.) (Revised by Mario Carneiro, 11-Dec-2016.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∃𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | r19.41 3258 | Restricted quantifier version of 19.41 2226. See r19.41v 3186 for a version with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 1-Nov-2010.) |
⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓)) | ||
Theorem | ralrimd 3259 | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) For a version based on fewer axioms see ralrimdv 3150. (Contributed by NM, 16-Feb-2004.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝜑 → (𝜓 → (𝑥 ∈ 𝐴 → 𝜒))) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | rexlimd2 3260 | Version of rexlimd 3261 with deduction version of second hypothesis. (Contributed by NM, 21-Jul-2013.) (Revised by Mario Carneiro, 8-Oct-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) | ||
Theorem | rexlimd 3261 | Deduction form of rexlimd 3261. For a version based on fewer axioms see rexlimdv 3151. (Contributed by NM, 27-May-1998.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Proof shortened by Wolf Lammen, 14-Jan-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜒 & ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) | ||
Theorem | r19.29af2 3262 | A commonly used pattern based on r19.29 3112. (Contributed by Thierry Arnoux, 17-Dec-2017.) (Proof shortened by OpenAI, 25-Mar-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜒 & ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | r19.29af 3263* | A commonly used pattern based on r19.29 3112. See r19.29a 3160, r19.29an 3156 for a variant when 𝑥 is disjoint from 𝜑. (Contributed by Thierry Arnoux, 29-Nov-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | reximd2a 3264 | Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by Thierry Arnoux, 27-Jan-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝑥 ∈ 𝐵) & ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜒) | ||
Theorem | ralbida 3265 | Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 6-Oct-2003.) (Proof shortened by Wolf Lammen, 31-Oct-2024.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | ralbidaOLD 3266 | Obsolete version of ralbida 3265 as of 31-Oct-2024. (Contributed by NM, 6-Oct-2003.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | rexbida 3267 | Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 6-Oct-2003.) |
⊢ Ⅎ𝑥𝜑 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | ralbid 3268 | Formula-building rule for restricted universal quantifier (deduction form). For a version based on fewer axioms see ralbidv 3175. (Contributed by NM, 27-Jun-1998.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | rexbid 3269 | Formula-building rule for restricted existential quantifier (deduction form). For a version based on fewer axioms see rexbidv 3176. (Contributed by NM, 27-Jun-1998.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | rexbidvALT 3270* | Alternate proof of rexbidv 3176, shorter but requires more axioms. (Contributed by NM, 20-Nov-1994.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | rexbidvaALT 3271* | Alternate proof of rexbidva 3174, shorter but requires more axioms. (Contributed by NM, 9-Mar-1997.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | rsp2 3272 | Restricted specialization, with two quantifiers. (Contributed by NM, 11-Feb-1997.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑)) | ||
Theorem | rsp2e 3273 | Restricted specialization. (Contributed by FL, 4-Jun-2012.) (Proof shortened by Wolf Lammen, 7-Jan-2020.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) | ||
Theorem | rspec2 3274 | Specialization rule for restricted quantification, with two quantifiers. (Contributed by NM, 20-Nov-1994.) |
⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ⇒ ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑) | ||
Theorem | rspec3 3275 | Specialization rule for restricted quantification, with three quantifiers. (Contributed by NM, 20-Nov-1994.) |
⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 ⇒ ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜑) | ||
Theorem | r2alf 3276* | Double restricted universal quantification. For a version based on fewer axioms see r2al 3192. (Contributed by Mario Carneiro, 14-Oct-2016.) Use r2allem 3140. (Revised by Wolf Lammen, 9-Jan-2020.) |
⊢ Ⅎ𝑦𝐴 ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑)) | ||
Theorem | r2exf 3277* | Double restricted existential quantification. For a version based on fewer axioms see r2ex 3193. (Contributed by Mario Carneiro, 14-Oct-2016.) Use r2exlem 3141. (Revised by Wolf Lammen, 10-Jan-2020.) |
⊢ Ⅎ𝑦𝐴 ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)) | ||
Theorem | 2ralbida 3278* | Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 24-Feb-2004.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) | ||
Theorem | nfra1 3279 | The setvar 𝑥 is not free in ∀𝑥 ∈ 𝐴𝜑. (Contributed by NM, 18-Oct-1996.) (Revised by Mario Carneiro, 7-Oct-2016.) |
⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝜑 | ||
Theorem | nfre1 3280 | The setvar 𝑥 is not free in ∃𝑥 ∈ 𝐴𝜑. (Contributed by NM, 19-Mar-1997.) (Revised by Mario Carneiro, 7-Oct-2016.) |
⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝜑 | ||
Theorem | ralcom4 3281* | Commutation of restricted and unrestricted universal quantifiers. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) Reduce axiom dependencies. (Revised by BJ, 13-Jun-2019.) (Proof shortened by Wolf Lammen, 31-Oct-2024.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑦∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | ralcom4OLD 3282* | Obsolete version of ralcom4 3281 as of 31-Oct-2024. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) Reduce axiom dependencies. (Revised by BJ, 13-Jun-2019.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑦∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rexcom4 3283* | Commutation of restricted and unrestricted existential quantifiers. (Contributed by NM, 12-Apr-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) Reduce axiom dependencies. (Revised by BJ, 13-Jun-2019.) |
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑) | ||
Theorem | ralcom 3284* | Commutation of restricted universal quantifiers. See ralcom2 3371 for a version without disjoint variable condition on 𝑥, 𝑦. This theorem should be used in place of ralcom2 3371 since it depends on a smaller set of axioms. (Contributed by NM, 13-Oct-1999.) (Revised by Mario Carneiro, 14-Oct-2016.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rexcom 3285* | 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.) (Proof shortened by Wolf Lammen, 8-Dec-2024.) |
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rexcomOLD 3286* | Obsolete version of rexcom 3285 as of 8-Dec-2024. (Contributed by NM, 19-Nov-1995.) (Revised by Mario Carneiro, 14-Oct-2016.) (Proof shortened by BJ, 26-Aug-2023.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rexcom4a 3287* | Specialized existential commutation lemma. (Contributed by Jeff Madsen, 1-Jun-2011.) |
⊢ (∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑦 ∈ 𝐴 (𝜑 ∧ ∃𝑥𝜓)) | ||
Theorem | ralrot3 3288* | Rotate three restricted universal quantifiers. (Contributed by AV, 3-Dec-2021.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 ↔ ∀𝑧 ∈ 𝐶 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑) | ||
Theorem | ralcom13 3289* | Swap first and third restricted universal quantifiers. (Contributed by AV, 3-Dec-2021.) (Proof shortened by Wolf Lammen, 2-Jan-2025.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 ↔ ∀𝑧 ∈ 𝐶 ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | ralcom13OLD 3290* | Obsolete version of ralcom13 3289 as of 2-Jan-2025. (Contributed by AV, 3-Dec-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 ↔ ∀𝑧 ∈ 𝐶 ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rexcom13 3291* | Swap first and third restricted existential quantifiers. (Contributed by NM, 8-Apr-2015.) |
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝜑 ↔ ∃𝑧 ∈ 𝐶 ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rexrot4 3292* | Rotate four restricted existential quantifiers twice. (Contributed by NM, 8-Apr-2015.) |
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 ∃𝑤 ∈ 𝐷 𝜑 ↔ ∃𝑧 ∈ 𝐶 ∃𝑤 ∈ 𝐷 ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) | ||
Theorem | 2ex2rexrot 3293* | Rotate two existential quantifiers and two restricted existential quantifiers. (Contributed by AV, 9-Nov-2023.) |
⊢ (∃𝑥∃𝑦∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∃𝑥∃𝑦𝜑) | ||
Theorem | nfra2w 3294* | Similar to Lemma 24 of [Monk2] p. 114, except that quantification is restricted. Once derived from hbra2VD 43923. Version of nfra2 3370 with a disjoint variable condition not requiring ax-13 2369. (Contributed by Alan Sare, 31-Dec-2011.) Reduce axiom usage. (Revised by Gino Giotto, 24-Sep-2024.) (Proof shortened by Wolf Lammen, 3-Jan-2025.) |
⊢ Ⅎ𝑦∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 | ||
Theorem | nfra2wOLD 3295* | Obsolete version of nfra2w 3294 as of 31-Oct-2024. (Contributed by Alan Sare, 31-Dec-2011.) (Revised by Gino Giotto, 24-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑦∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 | ||
Theorem | hbra1 3296 | The setvar 𝑥 is not free in ∀𝑥 ∈ 𝐴𝜑. (Contributed by NM, 18-Oct-1996.) (Proof shortened by Wolf Lammen, 7-Dec-2019.) |
⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | ralcomf 3297* | Commutation of restricted universal quantifiers. For a version based on fewer axioms see ralcom 3284. (Contributed by Mario Carneiro, 14-Oct-2016.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | rexcomf 3298* | Commutation of restricted existential quantifiers. For a version based on fewer axioms see rexcom 3285. (Contributed by Mario Carneiro, 14-Oct-2016.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) | ||
Theorem | cbvralfw 3299* | Rule used to change bound variables, using implicit substitution. Version of cbvralf 3354 with a disjoint variable condition, which does not require ax-10 2135, ax-13 2369. For a version not dependent on ax-11 2152 and ax-12, see cbvralvw 3232. (Contributed by NM, 7-Mar-2004.) Avoid ax-10 2135, ax-13 2369. (Revised by Gino Giotto, 23-May-2024.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvrexfw 3300* | Rule used to change bound variables, using implicit substitution. Version of cbvrexf 3355 with a disjoint variable condition, which does not require ax-13 2369. For a version not dependent on ax-11 2152 and ax-12, see cbvrexvw 3233. (Contributed by FL, 27-Apr-2008.) Avoid ax-10 2135, ax-13 2369. (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |