Home | Metamath
Proof Explorer Theorem List (p. 32 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pm2.21ddne 3101 | A contradiction implies anything. Equality/inequality deduction form. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | pm2.61ne 3102 | Deduction eliminating an inequality in an antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ (𝐴 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝜓) & ⊢ (𝜑 → 𝜒) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | pm2.61dne 3103 | Deduction eliminating an inequality in an antecedent. (Contributed by NM, 1-Jun-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓)) & ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | pm2.61dane 3104 | Deduction eliminating an inequality in an antecedent. (Contributed by NM, 30-Nov-2011.) |
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝜓) & ⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | pm2.61da2ne 3105 | Deduction eliminating two inequalities in an antecedent. (Contributed by NM, 29-May-2013.) |
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝜓) & ⊢ ((𝜑 ∧ 𝐶 = 𝐷) → 𝜓) & ⊢ ((𝜑 ∧ (𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷)) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | pm2.61da3ne 3106 | Deduction eliminating three inequalities in an antecedent. (Contributed by NM, 15-Jun-2013.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝜓) & ⊢ ((𝜑 ∧ 𝐶 = 𝐷) → 𝜓) & ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝜓) & ⊢ ((𝜑 ∧ (𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷 ∧ 𝐸 ≠ 𝐹)) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | pm2.61iine 3107 | Equality version of pm2.61ii 184. (Contributed by Scott Fenton, 13-Jun-2013.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) → 𝜑) & ⊢ (𝐴 = 𝐶 → 𝜑) & ⊢ (𝐵 = 𝐷 → 𝜑) ⇒ ⊢ 𝜑 | ||
Theorem | neor 3108 | Logical OR with an equality. (Contributed by NM, 29-Apr-2007.) |
⊢ ((𝐴 = 𝐵 ∨ 𝜓) ↔ (𝐴 ≠ 𝐵 → 𝜓)) | ||
Theorem | neanior 3109 | A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.) |
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷)) | ||
Theorem | ne3anior 3110 | A De Morgan's law for inequality. (Contributed by NM, 30-Sep-2013.) |
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷 ∧ 𝐸 ≠ 𝐹) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷 ∨ 𝐸 = 𝐹)) | ||
Theorem | neorian 3111 | A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.) |
⊢ ((𝐴 ≠ 𝐵 ∨ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∧ 𝐶 = 𝐷)) | ||
Theorem | nemtbir 3112 | An inference from an inequality, related to modus tollens. (Contributed by NM, 13-Apr-2007.) |
⊢ 𝐴 ≠ 𝐵 & ⊢ (𝜑 ↔ 𝐴 = 𝐵) ⇒ ⊢ ¬ 𝜑 | ||
Theorem | nelne1 3113 | Two classes are different if they don't contain the same element. (Contributed by NM, 3-Feb-2012.) (Proof shortened by Wolf Lammen, 14-May-2023.) |
⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐵 ≠ 𝐶) | ||
Theorem | nelne1OLD 3114 | Obsolete version of nelne1 3113 asw of 14-May-2023. (Contributed by NM, 3-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐵 ≠ 𝐶) | ||
Theorem | nelne2 3115 | Two classes are different if they don't belong to the same class. (Contributed by NM, 25-Jun-2012.) (Proof shortened by Wolf Lammen, 14-May-2023.) |
⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → 𝐴 ≠ 𝐵) | ||
Theorem | nelne2OLD 3116 | Obsolete version of nelne2 3115 asw of 14-May-2023. (Contributed by NM, 25-Jun-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → 𝐴 ≠ 𝐵) | ||
Theorem | nelelne 3117 | Two classes are different if they don't belong to the same class. (Contributed by Rodolfo Medina, 17-Oct-2010.) (Proof shortened by AV, 10-May-2020.) |
⊢ (¬ 𝐴 ∈ 𝐵 → (𝐶 ∈ 𝐵 → 𝐶 ≠ 𝐴)) | ||
Theorem | neneor 3118 | If two classes are different, a third class must be different of at least one of them. (Contributed by Thierry Arnoux, 8-Aug-2020.) |
⊢ (𝐴 ≠ 𝐵 → (𝐴 ≠ 𝐶 ∨ 𝐵 ≠ 𝐶)) | ||
Theorem | nfne 3119 | Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐴 ≠ 𝐵 | ||
Theorem | nfned 3120 | Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥 𝐴 ≠ 𝐵) | ||
Theorem | nabbi 3121 | Not equivalent wff's correspond to not equal class abstractions. (Contributed by AV, 7-Apr-2019.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ (∃𝑥(𝜑 ↔ ¬ 𝜓) ↔ {𝑥 ∣ 𝜑} ≠ {𝑥 ∣ 𝜓}) | ||
Theorem | mteqand 3122 | A modus tollens deduction for inequality. (Contributed by Steven Nguyen, 1-Jun-2023.) |
⊢ (𝜑 → 𝐶 ≠ 𝐷) & ⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) | ||
Syntax | wnel 3123 | Extend wff notation to include negated membership. |
wff 𝐴 ∉ 𝐵 | ||
Definition | df-nel 3124 | Define negated membership. (Contributed by NM, 7-Aug-1994.) |
⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵) | ||
Theorem | neli 3125 | Inference associated with df-nel 3124. (Contributed by BJ, 7-Jul-2018.) |
⊢ 𝐴 ∉ 𝐵 ⇒ ⊢ ¬ 𝐴 ∈ 𝐵 | ||
Theorem | nelir 3126 | Inference associated with df-nel 3124. (Contributed by BJ, 7-Jul-2018.) |
⊢ ¬ 𝐴 ∈ 𝐵 ⇒ ⊢ 𝐴 ∉ 𝐵 | ||
Theorem | neleq12d 3127 | Equality theorem for negated membership. (Contributed by FL, 10-Aug-2016.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ∉ 𝐶 ↔ 𝐵 ∉ 𝐷)) | ||
Theorem | neleq1 3128 | Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ (𝐴 = 𝐵 → (𝐴 ∉ 𝐶 ↔ 𝐵 ∉ 𝐶)) | ||
Theorem | neleq2 3129 | Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ (𝐴 = 𝐵 → (𝐶 ∉ 𝐴 ↔ 𝐶 ∉ 𝐵)) | ||
Theorem | nfnel 3130 | Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐴 ∉ 𝐵 | ||
Theorem | nfneld 3131 | Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥 𝐴 ∉ 𝐵) | ||
Theorem | nnel 3132 | Negation of negated membership, analogous to nne 3020. (Contributed by Alexander van der Vekens, 18-Jan-2018.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ (¬ 𝐴 ∉ 𝐵 ↔ 𝐴 ∈ 𝐵) | ||
Theorem | elnelne1 3133 | Two classes are different if they don't contain the same element. (Contributed by AV, 28-Jan-2020.) |
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∉ 𝐶) → 𝐵 ≠ 𝐶) | ||
Theorem | elnelne2 3134 | Two classes are different if they don't belong to the same class. (Contributed by AV, 28-Jan-2020.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∉ 𝐶) → 𝐴 ≠ 𝐵) | ||
Theorem | nelcon3d 3135 | Contrapositive law deduction for negated membership. (Contributed by AV, 28-Jan-2020.) |
⊢ (𝜑 → (𝐴 ∈ 𝐵 → 𝐶 ∈ 𝐷)) ⇒ ⊢ (𝜑 → (𝐶 ∉ 𝐷 → 𝐴 ∉ 𝐵)) | ||
Theorem | elnelall 3136 | A contradiction concerning membership implies anything. (Contributed by Alexander van der Vekens, 25-Jan-2018.) |
⊢ (𝐴 ∈ 𝐵 → (𝐴 ∉ 𝐵 → 𝜑)) | ||
Theorem | pm2.61danel 3137 | Deduction eliminating an elementhood in an antecedent. (Contributed by AV, 5-Dec-2021.) |
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐵) → 𝜓) & ⊢ ((𝜑 ∧ 𝐴 ∉ 𝐵) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Syntax | wral 3138 | Extend wff notation to include restricted universal quantification. |
wff ∀𝑥 ∈ 𝐴 𝜑 | ||
Syntax | wrex 3139 | Extend wff notation to include restricted existential quantification. |
wff ∃𝑥 ∈ 𝐴 𝜑 | ||
Syntax | wreu 3140 | Extend wff notation to include restricted existential uniqueness. |
wff ∃!𝑥 ∈ 𝐴 𝜑 | ||
Syntax | wrmo 3141 | Extend wff notation to include restricted "at most one." |
wff ∃*𝑥 ∈ 𝐴 𝜑 | ||
Syntax | crab 3142 | Extend class notation to include the restricted class abstraction (class builder). |
class {𝑥 ∈ 𝐴 ∣ 𝜑} | ||
Definition | df-ral 3143 |
Define restricted universal quantification. Special case of Definition
4.15(3) of [TakeutiZaring] p. 22.
Note: This notation is most often used to express that 𝜑 holds for all elements of a given class 𝐴. For this reading Ⅎ𝑥𝐴 is required, though, for example, asserted when 𝑥 and 𝐴 are disjoint. Should instead 𝐴 depend on 𝑥, you rather focus on those 𝑥 that happen to be contained in the corresponding 𝐴(𝑥). This hardly used interpretation could still occur naturally. For some examples, look at ralndv1 43185 or ralndv2 43186, courtesy of AV. So be careful to either keep 𝐴 independent of 𝑥, or adjust your comments to include such exotic cases. (Contributed by NM, 19-Aug-1993.) |
⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | ||
Definition | df-rex 3144 |
Define restricted existential quantification. Special case of Definition
4.15(4) of [TakeutiZaring] p. 22.
Note: This notation is most often used to express that 𝜑 holds for at least one element of a given class 𝐴. For this reading Ⅎ𝑥𝐴 is required, though, for example, asserted when 𝑥 and 𝐴 are disjoint. Should instead 𝐴 depend on 𝑥, you rather assert at least one 𝑥 fulfilling 𝜑 happens to be contained in the corresponding 𝐴(𝑥). This interpretation is rarely needed (see also df-ral 3143). (Contributed by NM, 30-Aug-1993.) |
⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | ||
Definition | df-reu 3145 |
Define restricted existential uniqueness.
Note: This notation is most often used to express that 𝜑 holds for exactly one element of a given class 𝐴. For this reading Ⅎ𝑥𝐴 is required, though, for example, asserted when 𝑥 and 𝐴 are disjoint. Should instead 𝐴 depend on 𝑥, you rather assert exactly one 𝑥 fulfilling 𝜑 happens to be contained in the corresponding 𝐴(𝑥). This interpretation is rarely needed (see also df-ral 3143). (Contributed by NM, 22-Nov-1994.) |
⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | ||
Definition | df-rmo 3146 |
Define restricted "at most one".
Note: This notation is most often used to express that 𝜑 holds for at most one element of a given class 𝐴. For this reading Ⅎ𝑥𝐴 is required, though, for example, asserted when 𝑥 and 𝐴 are disjoint. Should instead 𝐴 depend on 𝑥, you rather assert at most one 𝑥 fulfilling 𝜑 happens to be contained in the corresponding 𝐴(𝑥). This interpretation is rarely needed (see also df-ral 3143). (Contributed by NM, 16-Jun-2017.) |
⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | ||
Definition | df-rab 3147 |
Define a restricted class abstraction (class builder), which is the class
of all 𝑥 in 𝐴 such that 𝜑 is true. Definition of
[TakeutiZaring] p. 20.
Note: For the reading given above Ⅎ𝑥𝐴 is required, though, for example, asserted when 𝑥 and 𝐴 are disjoint. Should instead 𝐴 depend on 𝑥, you rather get a class of all those 𝑥 fulfilling 𝜑 that happen to be contained in the corresponding 𝐴(𝑥). This need not be a subset of any of the 𝐴(𝑥) at all. Such interpretation is rarely needed (see also df-ral 3143). (Contributed by NM, 22-Nov-1994.) |
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} | ||
Theorem | rgen 3148 | Generalization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.) |
⊢ (𝑥 ∈ 𝐴 → 𝜑) ⇒ ⊢ ∀𝑥 ∈ 𝐴 𝜑 | ||
Theorem | ralel 3149 | All elements of a class are elements of the class. (Contributed by AV, 30-Oct-2020.) |
⊢ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐴 | ||
Theorem | rgenw 3150 | Generalization rule for restricted quantification. (Contributed by NM, 18-Jun-2014.) |
⊢ 𝜑 ⇒ ⊢ ∀𝑥 ∈ 𝐴 𝜑 | ||
Theorem | rgen2w 3151 | Generalization rule for restricted quantification. Note that 𝑥 and 𝑦 needn't be distinct. (Contributed by NM, 18-Jun-2014.) |
⊢ 𝜑 ⇒ ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 | ||
Theorem | mprg 3152 | Modus ponens combined with restricted generalization. (Contributed by NM, 10-Aug-2004.) |
⊢ (∀𝑥 ∈ 𝐴 𝜑 → 𝜓) & ⊢ (𝑥 ∈ 𝐴 → 𝜑) ⇒ ⊢ 𝜓 | ||
Theorem | mprgbir 3153 | Modus ponens on biconditional combined with restricted generalization. (Contributed by NM, 21-Mar-2004.) |
⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓) & ⊢ (𝑥 ∈ 𝐴 → 𝜓) ⇒ ⊢ 𝜑 | ||
Theorem | alral 3154 | Universal quantification implies restricted quantification. (Contributed by NM, 20-Oct-2006.) |
⊢ (∀𝑥𝜑 → ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | raln 3155 | Restricted universally quantified negation expressed as a universally quantified negation. (Contributed by BJ, 16-Jul-2021.) |
⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑)) | ||
Theorem | ral2imi 3156 | Inference quantifying antecedent, nested antecedent, and consequent, with a strong hypothesis. (Contributed by NM, 19-Dec-2006.) Allow shortening of ralim 3162. (Revised by Wolf Lammen, 1-Dec-2019.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | ralimi2 3157 | Inference quantifying both antecedent and consequent. (Contributed by NM, 22-Feb-2004.) |
⊢ ((𝑥 ∈ 𝐴 → 𝜑) → (𝑥 ∈ 𝐵 → 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐵 𝜓) | ||
Theorem | ralimia 3158 | Inference quantifying both antecedent and consequent. (Contributed by NM, 19-Jul-1996.) |
⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓) | ||
Theorem | ralimiaa 3159 | Inference quantifying both antecedent and consequent. (Contributed by NM, 4-Aug-2007.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓) | ||
Theorem | ralimi 3160 | Inference quantifying both antecedent and consequent, with strong hypothesis. (Contributed by NM, 4-Mar-1997.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓) | ||
Theorem | 2ralimi 3161 | Inference quantifying both antecedent and consequent two times, with strong hypothesis. (Contributed by AV, 3-Dec-2021.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) | ||
Theorem | ralim 3162 | Distribution of restricted quantification over implication. (Contributed by NM, 9-Feb-1997.) (Proof shortened by Wolf Lammen, 1-Dec-2019.) |
⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | ralbii2 3163 | Inference adding different restricted universal quantifiers to each side of an equivalence. (Contributed by NM, 15-Aug-2005.) |
⊢ ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐵 → 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓) | ||
Theorem | ralbiia 3164 | Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 26-Nov-2000.) |
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓) | ||
Theorem | ralbii 3165 | Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 23-Nov-1994.) (Revised by Mario Carneiro, 17-Oct-2016.) (Proof shortened by Wolf Lammen, 4-Dec-2019.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓) | ||
Theorem | 2ralbii 3166 | Inference adding two restricted universal quantifiers to both sides of an equivalence. (Contributed by NM, 1-Aug-2004.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) | ||
Theorem | ralbi 3167 | Distribute a restricted universal quantifier over a biconditional. Restricted quantification version of albi 1810. (Contributed by NM, 6-Oct-2003.) Reduce axiom usage. (Revised by Wolf Lammen, 17-Jun-2023.) |
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | ralanid 3168 | Cancellation law for restricted universal quantification. (Contributed by Peter Mazsa, 30-Dec-2018.) (Proof shortened by Wolf Lammen, 29-Jun-2023.) |
⊢ (∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | ralanidOLD 3169 | Obsolete version of ralanid 3168 as of 29-Jun-2023. (Contributed by Peter Mazsa, 30-Dec-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | r19.26 3170 | Restricted quantifier version of 19.26 1862. (Contributed by NM, 28-Jan-1997.) (Proof shortened by Andrew Salmon, 30-May-2011.) |
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | r19.26-2 3171 | Restricted quantifier version of 19.26-2 1863. Version of r19.26 3170 with two quantifiers. (Contributed by NM, 10-Aug-2004.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | r19.26-3 3172 | Version of r19.26 3170 with three quantifiers. (Contributed by FL, 22-Nov-2010.) |
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓 ∧ ∀𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | r19.26m 3173 | Version of 19.26 1862 and r19.26 3170 with restricted quantifiers ranging over different classes. (Contributed by NM, 22-Feb-2004.) |
⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜓)) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | ralbiim 3174 | Split a biconditional and distribute quantifier. Restricted quantifier version of albiim 1881. (Contributed by NM, 3-Jun-2012.) |
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) ↔ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑))) | ||
Theorem | r19.21v 3175* | Restricted quantifier version of 19.21v 1931. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 2-Jan-2020.) |
⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | ralimdv2 3176* | Inference quantifying both antecedent and consequent. (Contributed by NM, 1-Feb-2005.) |
⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) → (𝑥 ∈ 𝐵 → 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐵 𝜒)) | ||
Theorem | ralimdva 3177* | Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 5-Dec-2019.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | ralimdv 3178* | Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90 (alim 1802). (Contributed by NM, 8-Oct-2003.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | ralimdvva 3179* | Deduction doubly quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90 (alim 1802). (Contributed by AV, 27-Nov-2019.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) | ||
Theorem | hbralrimi 3180 | Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). This theorem contains the common proof steps for ralrimi 3216 and ralrimiv 3181. Its main advantage over these two is its minimal references to axioms. The proof is extracted from NM's previous work. (Contributed by Wolf Lammen, 4-Dec-2019.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓)) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) | ||
Theorem | ralrimiv 3181* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 4-Dec-2019.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓)) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) | ||
Theorem | ralrimiva 3182* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Jan-2006.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) | ||
Theorem | ralrimivw 3183* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) | ||
Theorem | r19.27v 3184* | Restricted quantitifer version of one direction of 19.27 2220. (The other direction holds when 𝐴 is nonempty, see r19.27zv 4449.) (Contributed by NM, 3-Jun-2004.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Proof shortened by Wolf Lammen, 17-Jun-2023.) |
⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) | ||
Theorem | r19.27vOLD 3185* | Obsolete version of r19.27v 3184 as of 17-Jun-2023. (Contributed by NM, 3-Jun-2004.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) | ||
Theorem | r19.28v 3186* | Restricted quantifier version of one direction of 19.28 2221. (The other direction holds when 𝐴 is nonempty, see r19.28zv 4444.) (Contributed by NM, 2-Apr-2004.) (Proof shortened by Wolf Lammen, 17-Jun-2023.) |
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) | ||
Theorem | r19.28vOLD 3187* | Obsolete version of r19.28v 3186 as of 17-Jun-2023. (Contributed by NM, 2-Apr-2004.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) | ||
Theorem | ralrimdv 3188* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 27-May-1998.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 28-Dec-2019.) |
⊢ (𝜑 → (𝜓 → (𝑥 ∈ 𝐴 → 𝜒))) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | ralrimdva 3189* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Feb-2008.) (Proof shortened by Wolf Lammen, 28-Dec-2019.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | ralrimivv 3190* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by NM, 24-Jul-2004.) |
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜓)) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) | ||
Theorem | ralrimivva 3191* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by Jeff Madsen, 19-Jun-2011.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝜓) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) | ||
Theorem | ralrimivvva 3192* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with triple quantification.) (Contributed by Mario Carneiro, 9-Jul-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶)) → 𝜓) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓) | ||
Theorem | ralrimdvv 3193* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by NM, 1-Jun-2005.) |
⊢ (𝜑 → (𝜓 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜒))) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) | ||
Theorem | ralrimdvva 3194* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by NM, 2-Feb-2008.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) | ||
Theorem | ralbidv2 3195* | Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 6-Apr-1997.) |
⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) ↔ (𝑥 ∈ 𝐵 → 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) | ||
Theorem | ralbidva 3196* | Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 4-Mar-1997.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 29-Dec-2019.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | ralbidv 3197* | Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 20-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 5-Dec-2019.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | 2ralbidva 3198* | 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 | 2ralbidv 3199* | Formula-building rule for restricted universal quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.) (Revised by Szymon Jaroszewicz, 16-Mar-2007.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) | ||
Theorem | r2allem 3200 | Lemma factoring out common proof steps of r2alf 3222 and r2al 3201. Introduced to reduce dependencies on axioms. (Contributed by Wolf Lammen, 9-Jan-2020.) |
⊢ (∀𝑦(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝜑)) ↔ (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝐵 → 𝜑))) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |