Home | Metamath
Proof Explorer Theorem List (p. 32 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 | pm13.181 3101 | Theorem *13.181 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐵 ≠ 𝐶) → 𝐴 ≠ 𝐶) | ||
Theorem | pm2.61ine 3102 | Inference eliminating an inequality in an antecedent. (Contributed by NM, 16-Jan-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ (𝐴 = 𝐵 → 𝜑) & ⊢ (𝐴 ≠ 𝐵 → 𝜑) ⇒ ⊢ 𝜑 | ||
Theorem | pm2.21ddne 3103 | A contradiction implies anything. Equality/inequality deduction form. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | pm2.61ne 3104 | 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 3105 | Deduction eliminating an inequality in an antecedent. (Contributed by NM, 1-Jun-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓)) & ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | pm2.61dane 3106 | Deduction eliminating an inequality in an antecedent. (Contributed by NM, 30-Nov-2011.) |
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝜓) & ⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | pm2.61da2ne 3107 | Deduction eliminating two inequalities in an antecedent. (Contributed by NM, 29-May-2013.) |
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝜓) & ⊢ ((𝜑 ∧ 𝐶 = 𝐷) → 𝜓) & ⊢ ((𝜑 ∧ (𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷)) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | pm2.61da3ne 3108 | Deduction eliminating three inequalities in an antecedent. (Contributed by NM, 15-Jun-2013.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝜓) & ⊢ ((𝜑 ∧ 𝐶 = 𝐷) → 𝜓) & ⊢ ((𝜑 ∧ 𝐸 = 𝐹) → 𝜓) & ⊢ ((𝜑 ∧ (𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷 ∧ 𝐸 ≠ 𝐹)) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | pm2.61iine 3109 | Equality version of pm2.61ii 185. (Contributed by Scott Fenton, 13-Jun-2013.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) → 𝜑) & ⊢ (𝐴 = 𝐶 → 𝜑) & ⊢ (𝐵 = 𝐷 → 𝜑) ⇒ ⊢ 𝜑 | ||
Theorem | neor 3110 | Logical OR with an equality. (Contributed by NM, 29-Apr-2007.) |
⊢ ((𝐴 = 𝐵 ∨ 𝜓) ↔ (𝐴 ≠ 𝐵 → 𝜓)) | ||
Theorem | neanior 3111 | A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.) |
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷)) | ||
Theorem | ne3anior 3112 | A De Morgan's law for inequality. (Contributed by NM, 30-Sep-2013.) |
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷 ∧ 𝐸 ≠ 𝐹) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷 ∨ 𝐸 = 𝐹)) | ||
Theorem | neorian 3113 | A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.) |
⊢ ((𝐴 ≠ 𝐵 ∨ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∧ 𝐶 = 𝐷)) | ||
Theorem | nemtbir 3114 | An inference from an inequality, related to modus tollens. (Contributed by NM, 13-Apr-2007.) |
⊢ 𝐴 ≠ 𝐵 & ⊢ (𝜑 ↔ 𝐴 = 𝐵) ⇒ ⊢ ¬ 𝜑 | ||
Theorem | nelne1 3115 | 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 3116 | Obsolete version of nelne1 3115 asw of 14-May-2023. (Contributed by NM, 3-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐵 ≠ 𝐶) | ||
Theorem | nelne2 3117 | 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 3118 | Obsolete version of nelne2 3117 asw of 14-May-2023. (Contributed by NM, 25-Jun-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → 𝐴 ≠ 𝐵) | ||
Theorem | nelelne 3119 | 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 3120 | 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 3121 | Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐴 ≠ 𝐵 | ||
Theorem | nfned 3122 | Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥 𝐴 ≠ 𝐵) | ||
Theorem | nabbi 3123 | 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 3124 | A modus tollens deduction for inequality. (Contributed by Steven Nguyen, 1-Jun-2023.) |
⊢ (𝜑 → 𝐶 ≠ 𝐷) & ⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) | ||
Syntax | wnel 3125 | Extend wff notation to include negated membership. |
wff 𝐴 ∉ 𝐵 | ||
Definition | df-nel 3126 | Define negated membership. (Contributed by NM, 7-Aug-1994.) |
⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵) | ||
Theorem | neli 3127 | Inference associated with df-nel 3126. (Contributed by BJ, 7-Jul-2018.) |
⊢ 𝐴 ∉ 𝐵 ⇒ ⊢ ¬ 𝐴 ∈ 𝐵 | ||
Theorem | nelir 3128 | Inference associated with df-nel 3126. (Contributed by BJ, 7-Jul-2018.) |
⊢ ¬ 𝐴 ∈ 𝐵 ⇒ ⊢ 𝐴 ∉ 𝐵 | ||
Theorem | neleq12d 3129 | Equality theorem for negated membership. (Contributed by FL, 10-Aug-2016.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ∉ 𝐶 ↔ 𝐵 ∉ 𝐷)) | ||
Theorem | neleq1 3130 | Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ (𝐴 = 𝐵 → (𝐴 ∉ 𝐶 ↔ 𝐵 ∉ 𝐶)) | ||
Theorem | neleq2 3131 | Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ (𝐴 = 𝐵 → (𝐶 ∉ 𝐴 ↔ 𝐶 ∉ 𝐵)) | ||
Theorem | nfnel 3132 | Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐴 ∉ 𝐵 | ||
Theorem | nfneld 3133 | Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥 𝐴 ∉ 𝐵) | ||
Theorem | nnel 3134 | Negation of negated membership, analogous to nne 3022. (Contributed by Alexander van der Vekens, 18-Jan-2018.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
⊢ (¬ 𝐴 ∉ 𝐵 ↔ 𝐴 ∈ 𝐵) | ||
Theorem | elnelne1 3135 | Two classes are different if they don't contain the same element. (Contributed by AV, 28-Jan-2020.) |
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∉ 𝐶) → 𝐵 ≠ 𝐶) | ||
Theorem | elnelne2 3136 | Two classes are different if they don't belong to the same class. (Contributed by AV, 28-Jan-2020.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∉ 𝐶) → 𝐴 ≠ 𝐵) | ||
Theorem | nelcon3d 3137 | Contrapositive law deduction for negated membership. (Contributed by AV, 28-Jan-2020.) |
⊢ (𝜑 → (𝐴 ∈ 𝐵 → 𝐶 ∈ 𝐷)) ⇒ ⊢ (𝜑 → (𝐶 ∉ 𝐷 → 𝐴 ∉ 𝐵)) | ||
Theorem | elnelall 3138 | A contradiction concerning membership implies anything. (Contributed by Alexander van der Vekens, 25-Jan-2018.) |
⊢ (𝐴 ∈ 𝐵 → (𝐴 ∉ 𝐵 → 𝜑)) | ||
Theorem | pm2.61danel 3139 | Deduction eliminating an elementhood in an antecedent. (Contributed by AV, 5-Dec-2021.) |
⊢ ((𝜑 ∧ 𝐴 ∈ 𝐵) → 𝜓) & ⊢ ((𝜑 ∧ 𝐴 ∉ 𝐵) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Syntax | wral 3140 | Extend wff notation to include restricted universal quantification. |
wff ∀𝑥 ∈ 𝐴 𝜑 | ||
Syntax | wrex 3141 | Extend wff notation to include restricted existential quantification. |
wff ∃𝑥 ∈ 𝐴 𝜑 | ||
Syntax | wreu 3142 | Extend wff notation to include restricted existential uniqueness. |
wff ∃!𝑥 ∈ 𝐴 𝜑 | ||
Syntax | wrmo 3143 | Extend wff notation to include restricted "at most one." |
wff ∃*𝑥 ∈ 𝐴 𝜑 | ||
Syntax | crab 3144 | Extend class notation to include the restricted class abstraction (class builder). |
class {𝑥 ∈ 𝐴 ∣ 𝜑} | ||
Definition | df-ral 3145 |
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 43311 or ralndv2 43312, 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 3146 |
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 3145). (Contributed by NM, 30-Aug-1993.) |
⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | ||
Definition | df-reu 3147 |
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 3145). (Contributed by NM, 22-Nov-1994.) |
⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | ||
Definition | df-rmo 3148 |
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 3145). (Contributed by NM, 16-Jun-2017.) |
⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | ||
Definition | df-rab 3149 |
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 3145). (Contributed by NM, 22-Nov-1994.) |
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} | ||
Theorem | rgen 3150 | Generalization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.) |
⊢ (𝑥 ∈ 𝐴 → 𝜑) ⇒ ⊢ ∀𝑥 ∈ 𝐴 𝜑 | ||
Theorem | ralel 3151 | All elements of a class are elements of the class. (Contributed by AV, 30-Oct-2020.) |
⊢ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐴 | ||
Theorem | rgenw 3152 | Generalization rule for restricted quantification. (Contributed by NM, 18-Jun-2014.) |
⊢ 𝜑 ⇒ ⊢ ∀𝑥 ∈ 𝐴 𝜑 | ||
Theorem | rgen2w 3153 | Generalization rule for restricted quantification. Note that 𝑥 and 𝑦 needn't be distinct. (Contributed by NM, 18-Jun-2014.) |
⊢ 𝜑 ⇒ ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 | ||
Theorem | mprg 3154 | Modus ponens combined with restricted generalization. (Contributed by NM, 10-Aug-2004.) |
⊢ (∀𝑥 ∈ 𝐴 𝜑 → 𝜓) & ⊢ (𝑥 ∈ 𝐴 → 𝜑) ⇒ ⊢ 𝜓 | ||
Theorem | mprgbir 3155 | Modus ponens on biconditional combined with restricted generalization. (Contributed by NM, 21-Mar-2004.) |
⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓) & ⊢ (𝑥 ∈ 𝐴 → 𝜓) ⇒ ⊢ 𝜑 | ||
Theorem | alral 3156 | Universal quantification implies restricted quantification. (Contributed by NM, 20-Oct-2006.) |
⊢ (∀𝑥𝜑 → ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | raln 3157 | Restricted universally quantified negation expressed as a universally quantified negation. (Contributed by BJ, 16-Jul-2021.) |
⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑)) | ||
Theorem | ral2imi 3158 | Inference quantifying antecedent, nested antecedent, and consequent, with a strong hypothesis. (Contributed by NM, 19-Dec-2006.) Allow shortening of ralim 3164. (Revised by Wolf Lammen, 1-Dec-2019.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | ralimi2 3159 | Inference quantifying both antecedent and consequent. (Contributed by NM, 22-Feb-2004.) |
⊢ ((𝑥 ∈ 𝐴 → 𝜑) → (𝑥 ∈ 𝐵 → 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐵 𝜓) | ||
Theorem | ralimia 3160 | Inference quantifying both antecedent and consequent. (Contributed by NM, 19-Jul-1996.) |
⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓) | ||
Theorem | ralimiaa 3161 | Inference quantifying both antecedent and consequent. (Contributed by NM, 4-Aug-2007.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓) | ||
Theorem | ralimi 3162 | Inference quantifying both antecedent and consequent, with strong hypothesis. (Contributed by NM, 4-Mar-1997.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓) | ||
Theorem | 2ralimi 3163 | Inference quantifying both antecedent and consequent two times, with strong hypothesis. (Contributed by AV, 3-Dec-2021.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) | ||
Theorem | ralim 3164 | Distribution of restricted quantification over implication. (Contributed by NM, 9-Feb-1997.) (Proof shortened by Wolf Lammen, 1-Dec-2019.) |
⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | ralbii2 3165 | Inference adding different restricted universal quantifiers to each side of an equivalence. (Contributed by NM, 15-Aug-2005.) |
⊢ ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐵 → 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓) | ||
Theorem | ralbiia 3166 | Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 26-Nov-2000.) |
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓) | ||
Theorem | ralbii 3167 | 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 3168 | Inference adding two restricted universal quantifiers to both sides of an equivalence. (Contributed by NM, 1-Aug-2004.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) | ||
Theorem | ralbi 3169 | Distribute a restricted universal quantifier over a biconditional. Restricted quantification version of albi 1819. (Contributed by NM, 6-Oct-2003.) Reduce axiom usage. (Revised by Wolf Lammen, 17-Jun-2023.) |
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | ralanid 3170 | Cancellation law for restricted universal quantification. (Contributed by Peter Mazsa, 30-Dec-2018.) (Proof shortened by Wolf Lammen, 29-Jun-2023.) |
⊢ (∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | ralanidOLD 3171 | Obsolete version of ralanid 3170 as of 29-Jun-2023. (Contributed by Peter Mazsa, 30-Dec-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∀𝑥 ∈ 𝐴 𝜑) | ||
Theorem | r19.26 3172 | Restricted quantifier version of 19.26 1871. (Contributed by NM, 28-Jan-1997.) (Proof shortened by Andrew Salmon, 30-May-2011.) |
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | r19.26-2 3173 | Restricted quantifier version of 19.26-2 1872. Version of r19.26 3172 with two quantifiers. (Contributed by NM, 10-Aug-2004.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | r19.26-3 3174 | Version of r19.26 3172 with three quantifiers. (Contributed by FL, 22-Nov-2010.) |
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓 ∧ ∀𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | r19.26m 3175 | Version of 19.26 1871 and r19.26 3172 with restricted quantifiers ranging over different classes. (Contributed by NM, 22-Feb-2004.) |
⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜓)) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | ralbiim 3176 | Split a biconditional and distribute quantifier. Restricted quantifier version of albiim 1890. (Contributed by NM, 3-Jun-2012.) |
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) ↔ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑))) | ||
Theorem | r19.21v 3177* | Restricted quantifier version of 19.21v 1940. (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 3178* | Inference quantifying both antecedent and consequent. (Contributed by NM, 1-Feb-2005.) |
⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) → (𝑥 ∈ 𝐵 → 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐵 𝜒)) | ||
Theorem | ralimdva 3179* | 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 3180* | Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90 (alim 1811). (Contributed by NM, 8-Oct-2003.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | ralimdvva 3181* | Deduction doubly quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90 (alim 1811). (Contributed by AV, 27-Nov-2019.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) | ||
Theorem | hbralrimi 3182 | Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). This theorem contains the common proof steps for ralrimi 3218 and ralrimiv 3183. 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 3183* | 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 3184* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Jan-2006.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) | ||
Theorem | ralrimivw 3185* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) | ||
Theorem | r19.27v 3186* | Restricted quantitifer version of one direction of 19.27 2229. (The other direction holds when 𝐴 is nonempty, see r19.27zv 4453.) (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 3187* | Obsolete version of r19.27v 3186 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 3188* | Restricted quantifier version of one direction of 19.28 2230. (The other direction holds when 𝐴 is nonempty, see r19.28zv 4448.) (Contributed by NM, 2-Apr-2004.) (Proof shortened by Wolf Lammen, 17-Jun-2023.) |
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) | ||
Theorem | r19.28vOLD 3189* | Obsolete version of r19.28v 3188 as of 17-Jun-2023. (Contributed by NM, 2-Apr-2004.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) | ||
Theorem | ralrimdv 3190* | 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 3191* | 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 3192* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by NM, 24-Jul-2004.) |
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜓)) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) | ||
Theorem | ralrimivva 3193* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by Jeff Madsen, 19-Jun-2011.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝜓) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) | ||
Theorem | ralrimivvva 3194* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with triple quantification.) (Contributed by Mario Carneiro, 9-Jul-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶)) → 𝜓) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓) | ||
Theorem | ralrimdvv 3195* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by NM, 1-Jun-2005.) |
⊢ (𝜑 → (𝜓 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜒))) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) | ||
Theorem | ralrimdvva 3196* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by NM, 2-Feb-2008.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) | ||
Theorem | ralbidv2 3197* | Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 6-Apr-1997.) |
⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) ↔ (𝑥 ∈ 𝐵 → 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) | ||
Theorem | ralbidva 3198* | 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 3199* | 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 3200* | 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.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |