P. 23 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 2201-2300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	neeq12i 2201	Inference for inequality. (Contributed by NM, 24-Jul-2012.)
⊢ A = B    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (A ≠ 𝐶 ↔ B ≠ 𝐷)
Theorem	neeq1d 2202	Deduction for inequality. (Contributed by NM, 25-Oct-1999.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (A ≠ 𝐶 ↔ B ≠ 𝐶))
Theorem	neeq2d 2203	Deduction for inequality. (Contributed by NM, 25-Oct-1999.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (𝐶 ≠ A ↔ 𝐶 ≠ B))
Theorem	neeq12d 2204	Deduction for inequality. (Contributed by NM, 24-Jul-2012.)
⊢ (φ → A = B)    &   ⊢ (φ → 𝐶 = 𝐷)    ⇒   ⊢ (φ → (A ≠ 𝐶 ↔ B ≠ 𝐷))
Theorem	neneqd 2205	Deduction eliminating inequality definition. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (φ → A ≠ B)    ⇒   ⊢ (φ → ¬ A = B)
Theorem	eqnetri 2206	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ A = B    &   ⊢ B ≠ 𝐶    ⇒   ⊢ A ≠ 𝐶
Theorem	eqnetrd 2207	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ (φ → A = B)    &   ⊢ (φ → B ≠ 𝐶)    ⇒   ⊢ (φ → A ≠ 𝐶)
Theorem	eqnetrri 2208	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ A = B    &   ⊢ A ≠ 𝐶    ⇒   ⊢ B ≠ 𝐶
Theorem	eqnetrrd 2209	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ (φ → A = B)    &   ⊢ (φ → A ≠ 𝐶)    ⇒   ⊢ (φ → B ≠ 𝐶)
Theorem	neeqtri 2210	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ A ≠ B    &   ⊢ B = 𝐶    ⇒   ⊢ A ≠ 𝐶
Theorem	neeqtrd 2211	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ (φ → A ≠ B)    &   ⊢ (φ → B = 𝐶)    ⇒   ⊢ (φ → A ≠ 𝐶)
Theorem	neeqtrri 2212	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ A ≠ B    &   ⊢ 𝐶 = B    ⇒   ⊢ A ≠ 𝐶
Theorem	neeqtrrd 2213	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
⊢ (φ → A ≠ B)    &   ⊢ (φ → 𝐶 = B)    ⇒   ⊢ (φ → A ≠ 𝐶)
Theorem	syl5eqner 2214	B chained equality inference for inequality. (Contributed by NM, 6-Jun-2012.)
⊢ B = A    &   ⊢ (φ → B ≠ 𝐶)    ⇒   ⊢ (φ → A ≠ 𝐶)
Theorem	3netr3d 2215	Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.)
⊢ (φ → A ≠ B)    &   ⊢ (φ → A = 𝐶)    &   ⊢ (φ → B = 𝐷)    ⇒   ⊢ (φ → 𝐶 ≠ 𝐷)
Theorem	3netr4d 2216	Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.)
⊢ (φ → A ≠ B)    &   ⊢ (φ → 𝐶 = A)    &   ⊢ (φ → 𝐷 = B)    ⇒   ⊢ (φ → 𝐶 ≠ 𝐷)
Theorem	3netr3g 2217	Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.)
⊢ (φ → A ≠ B)    &   ⊢ A = 𝐶    &   ⊢ B = 𝐷    ⇒   ⊢ (φ → 𝐶 ≠ 𝐷)
Theorem	3netr4g 2218	Substitution of equality into both sides of an inequality. (Contributed by NM, 14-Jun-2012.)
⊢ (φ → A ≠ B)    &   ⊢ 𝐶 = A    &   ⊢ 𝐷 = B    ⇒   ⊢ (φ → 𝐶 ≠ 𝐷)
Theorem	necon3abii 2219	Deduction from equality to inequality. (Contributed by NM, 9-Nov-2007.)
⊢ (A = B ↔ φ)    ⇒   ⊢ (A ≠ B ↔ ¬ φ)
Theorem	necon3bbii 2220	Deduction from equality to inequality. (Contributed by NM, 13-Apr-2007.)
⊢ (φ ↔ A = B)    ⇒   ⊢ (¬ φ ↔ A ≠ B)
Theorem	necon3bii 2221	Inference from equality to inequality. (Contributed by NM, 23-Feb-2005.)
⊢ (A = B ↔ 𝐶 = 𝐷)    ⇒   ⊢ (A ≠ B ↔ 𝐶 ≠ 𝐷)
Theorem	necon3abid 2222	Deduction from equality to inequality. (Contributed by NM, 21-Mar-2007.)
⊢ (φ → (A = B ↔ ψ))    ⇒   ⊢ (φ → (A ≠ B ↔ ¬ ψ))
Theorem	necon3bbid 2223	Deduction from equality to inequality. (Contributed by NM, 2-Jun-2007.)
⊢ (φ → (ψ ↔ A = B))    ⇒   ⊢ (φ → (¬ ψ ↔ A ≠ B))
Theorem	necon3bid 2224	Deduction from equality to inequality. (Contributed by NM, 23-Feb-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (φ → (A = B ↔ 𝐶 = 𝐷))    ⇒   ⊢ (φ → (A ≠ B ↔ 𝐶 ≠ 𝐷))
Theorem	necon3ad 2225	Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
⊢ (φ → (ψ → A = B))    ⇒   ⊢ (φ → (A ≠ B → ¬ ψ))
Theorem	necon3bd 2226	Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
⊢ (φ → (A = B → ψ))    ⇒   ⊢ (φ → (¬ ψ → A ≠ B))
Theorem	necon3d 2227	Contrapositive law deduction for inequality. (Contributed by NM, 10-Jun-2006.)
⊢ (φ → (A = B → 𝐶 = 𝐷))    ⇒   ⊢ (φ → (𝐶 ≠ 𝐷 → A ≠ B))
Theorem	nesym 2228	Characterization of inequality in terms of reversed equality (see bicom 128). (Contributed by BJ, 7-Jul-2018.)
⊢ (A ≠ B ↔ ¬ B = A)
Theorem	nesymi 2229	Inference associated with nesym 2228. (Contributed by BJ, 7-Jul-2018.)
⊢ A ≠ B    ⇒   ⊢ ¬ B = A
Theorem	nesymir 2230	Inference associated with nesym 2228. (Contributed by BJ, 7-Jul-2018.)
⊢ ¬ A = B    ⇒   ⊢ B ≠ A
Theorem	necon3i 2231	Contrapositive inference for inequality. (Contributed by NM, 9-Aug-2006.)
⊢ (A = B → 𝐶 = 𝐷)    ⇒   ⊢ (𝐶 ≠ 𝐷 → A ≠ B)
Theorem	necon3ai 2232	Contrapositive inference for inequality. (Contributed by NM, 23-May-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
⊢ (φ → A = B)    ⇒   ⊢ (A ≠ B → ¬ φ)
Theorem	necon3bi 2233	Contrapositive inference for inequality. (Contributed by NM, 1-Jun-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
⊢ (A = B → φ)    ⇒   ⊢ (¬ φ → A ≠ B)
Theorem	necon1aidc 2234	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 15-May-2018.)
⊢ (DECID φ → (¬ φ → A = B))    ⇒   ⊢ (DECID φ → (A ≠ B → φ))
Theorem	necon1bidc 2235	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 15-May-2018.)
⊢ (DECID A = B → (A ≠ B → φ))    ⇒   ⊢ (DECID A = B → (¬ φ → A = B))
Theorem	necon1idc 2236	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
⊢ (A ≠ B → 𝐶 = 𝐷)    ⇒   ⊢ (DECID A = B → (𝐶 ≠ 𝐷 → A = B))
Theorem	necon2ai 2237	Contrapositive inference for inequality. (Contributed by NM, 16-Jan-2007.) (Proof rewritten by Jim Kingdon, 16-May-2018.)
⊢ (A = B → ¬ φ)    ⇒   ⊢ (φ → A ≠ B)
Theorem	necon2bi 2238	Contrapositive inference for inequality. (Contributed by NM, 1-Apr-2007.)
⊢ (φ → A ≠ B)    ⇒   ⊢ (A = B → ¬ φ)
Theorem	necon2i 2239	Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007.)
⊢ (A = B → 𝐶 ≠ 𝐷)    ⇒   ⊢ (𝐶 = 𝐷 → A ≠ B)
Theorem	necon2ad 2240	Contrapositive inference for inequality. (Contributed by NM, 19-Apr-2007.) (Proof rewritten by Jim Kingdon, 16-May-2018.)
⊢ (φ → (A = B → ¬ ψ))    ⇒   ⊢ (φ → (ψ → A ≠ B))
Theorem	necon2bd 2241	Contrapositive inference for inequality. (Contributed by NM, 13-Apr-2007.)
⊢ (φ → (ψ → A ≠ B))    ⇒   ⊢ (φ → (A = B → ¬ ψ))
Theorem	necon2d 2242	Contrapositive inference for inequality. (Contributed by NM, 28-Dec-2008.)
⊢ (φ → (A = B → 𝐶 ≠ 𝐷))    ⇒   ⊢ (φ → (𝐶 = 𝐷 → A ≠ B))
Theorem	necon1abiidc 2243	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
⊢ (DECID φ → (¬ φ ↔ A = B))    ⇒   ⊢ (DECID φ → (A ≠ B ↔ φ))
Theorem	necon1bbiidc 2244	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
⊢ (DECID A = B → (A ≠ B ↔ φ))    ⇒   ⊢ (DECID A = B → (¬ φ ↔ A = B))
Theorem	necon1abiddc 2245	Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
⊢ (φ → (DECID ψ → (¬ ψ ↔ A = B)))    ⇒   ⊢ (φ → (DECID ψ → (A ≠ B ↔ ψ)))
Theorem	necon1bbiddc 2246	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
⊢ (φ → (DECID A = B → (A ≠ B ↔ ψ)))    ⇒   ⊢ (φ → (DECID A = B → (¬ ψ ↔ A = B)))
Theorem	necon2abiidc 2247	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
⊢ (DECID φ → (A = B ↔ ¬ φ))    ⇒   ⊢ (DECID φ → (φ ↔ A ≠ B))
Theorem	necon2bbii 2248	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
⊢ (DECID A = B → (φ ↔ A ≠ B))    ⇒   ⊢ (DECID A = B → (A = B ↔ ¬ φ))
Theorem	necon2abiddc 2249	Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
⊢ (φ → (DECID ψ → (A = B ↔ ¬ ψ)))    ⇒   ⊢ (φ → (DECID ψ → (ψ ↔ A ≠ B)))
Theorem	necon2bbiddc 2250	Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
⊢ (φ → (DECID A = B → (ψ ↔ A ≠ B)))    ⇒   ⊢ (φ → (DECID A = B → (A = B ↔ ¬ ψ)))
Theorem	necon4aidc 2251	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
⊢ (DECID A = B → (A ≠ B → ¬ φ))    ⇒   ⊢ (DECID A = B → (φ → A = B))
Theorem	necon4idc 2252	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
⊢ (DECID A = B → (A ≠ B → 𝐶 ≠ 𝐷))    ⇒   ⊢ (DECID A = B → (𝐶 = 𝐷 → A = B))
Theorem	necon4addc 2253	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 17-May-2018.)
⊢ (φ → (DECID A = B → (A ≠ B → ¬ ψ)))    ⇒   ⊢ (φ → (DECID A = B → (ψ → A = B)))
Theorem	necon4bddc 2254	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 17-May-2018.)
⊢ (φ → (DECID ψ → (¬ ψ → A ≠ B)))    ⇒   ⊢ (φ → (DECID ψ → (A = B → ψ)))
Theorem	necon4ddc 2255	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 17-May-2018.)
⊢ (φ → (DECID A = B → (A ≠ B → 𝐶 ≠ 𝐷)))    ⇒   ⊢ (φ → (DECID A = B → (𝐶 = 𝐷 → A = B)))
Theorem	necon4abiddc 2256	Contrapositive law deduction for inequality. (Contributed by Jim Kingdon, 18-May-2018.)
⊢ (φ → (DECID A = B → (DECID ψ → (A ≠ B ↔ ¬ ψ))))    ⇒   ⊢ (φ → (DECID A = B → (DECID ψ → (A = B ↔ ψ))))
Theorem	necon4bbiddc 2257	Contrapositive law deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
⊢ (φ → (DECID ψ → (DECID A = B → (¬ ψ ↔ A ≠ B))))    ⇒   ⊢ (φ → (DECID ψ → (DECID A = B → (ψ ↔ A = B))))
Theorem	necon4biddc 2258	Contrapositive law deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
⊢ (φ → (DECID A = B → (DECID 𝐶 = 𝐷 → (A ≠ B ↔ 𝐶 ≠ 𝐷))))    ⇒   ⊢ (φ → (DECID A = B → (DECID 𝐶 = 𝐷 → (A = B ↔ 𝐶 = 𝐷))))
Theorem	necon1addc 2259	Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
⊢ (φ → (DECID ψ → (¬ ψ → A = B)))    ⇒   ⊢ (φ → (DECID ψ → (A ≠ B → ψ)))
Theorem	necon1bddc 2260	Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
⊢ (φ → (DECID A = B → (A ≠ B → ψ)))    ⇒   ⊢ (φ → (DECID A = B → (¬ ψ → A = B)))
Theorem	necon1ddc 2261	Contrapositive law deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
⊢ (φ → (DECID A = B → (A ≠ B → 𝐶 = 𝐷)))    ⇒   ⊢ (φ → (DECID A = B → (𝐶 ≠ 𝐷 → A = B)))
Theorem	neneqad 2262	If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2205. One-way deduction form of df-ne 2188. (Contributed by David Moews, 28-Feb-2017.)
⊢ (φ → ¬ A = B)    ⇒   ⊢ (φ → A ≠ B)
Theorem	nebidc 2263	Contraposition law for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
⊢ (DECID A = B → (DECID 𝐶 = 𝐷 → ((A = B ↔ 𝐶 = 𝐷) ↔ (A ≠ B ↔ 𝐶 ≠ 𝐷))))
Theorem	pm13.18 2264	Theorem *13.18 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.)
⊢ ((A = B ∧ A ≠ 𝐶) → B ≠ 𝐶)
Theorem	pm13.181 2265	Theorem *13.181 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.)
⊢ ((A = B ∧ B ≠ 𝐶) → A ≠ 𝐶)
Theorem	pm2.21ddne 2266	A contradiction implies anything. Equality/inequality deduction form. (Contributed by David Moews, 28-Feb-2017.)
⊢ (φ → A = B)    &   ⊢ (φ → A ≠ B)    ⇒   ⊢ (φ → ψ)
Theorem	necom 2267	Commutation of inequality. (Contributed by NM, 14-May-1999.)
⊢ (A ≠ B ↔ B ≠ A)
Theorem	necomi 2268	Inference from commutative law for inequality. (Contributed by NM, 17-Oct-2012.)
⊢ A ≠ B    ⇒   ⊢ B ≠ A
Theorem	necomd 2269	Deduction from commutative law for inequality. (Contributed by NM, 12-Feb-2008.)
⊢ (φ → A ≠ B)    ⇒   ⊢ (φ → B ≠ A)
Theorem	neanior 2270	A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.)
⊢ ((A ≠ B ∧ 𝐶 ≠ 𝐷) ↔ ¬ (A = B ∨ 𝐶 = 𝐷))
Theorem	ne3anior 2271	A De Morgan's law for inequality. (Contributed by NM, 30-Sep-2013.) (Proof rewritten by Jim Kingdon, 19-May-2018.)
⊢ ((A ≠ B ∧ 𝐶 ≠ 𝐷 ∧ 𝐸 ≠ 𝐹) ↔ ¬ (A = B ∨ 𝐶 = 𝐷 ∨ 𝐸 = 𝐹))
Theorem	nemtbir 2272	An inference from an inequality, related to modus tollens. (Contributed by NM, 13-Apr-2007.)
⊢ A ≠ B    &   ⊢ (φ ↔ A = B)    ⇒   ⊢ ¬ φ
Theorem	nelne1 2273	Two classes are different if they don't contain the same element. (Contributed by NM, 3-Feb-2012.)
⊢ ((A ∈ B ∧ ¬ A ∈ 𝐶) → B ≠ 𝐶)
Theorem	nelne2 2274	Two classes are different if they don't belong to the same class. (Contributed by NM, 25-Jun-2012.)
⊢ ((A ∈ 𝐶 ∧ ¬ B ∈ 𝐶) → A ≠ B)
Theorem	nfne 2275	Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ ℲxA    &   ⊢ ℲxB    ⇒   ⊢ Ⅎx A ≠ B
Theorem	nfned 2276	Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ (φ → ℲxA)    &   ⊢ (φ → ℲxB)    ⇒   ⊢ (φ → Ⅎx A ≠ B)
2.1.4.2  Negated membership
Theorem	neli 2277	Inference associated with df-nel 2189. (Contributed by BJ, 7-Jul-2018.)
⊢ A ∉ B    ⇒   ⊢ ¬ A ∈ B
Theorem	nelir 2278	Inference associated with df-nel 2189. (Contributed by BJ, 7-Jul-2018.)
⊢ ¬ A ∈ B    ⇒   ⊢ A ∉ B
Theorem	neleq1 2279	Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.)
⊢ (A = B → (A ∉ 𝐶 ↔ B ∉ 𝐶))
Theorem	neleq2 2280	Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.)
⊢ (A = B → (𝐶 ∉ A ↔ 𝐶 ∉ B))
Theorem	neleq12d 2281	Equality theorem for negated membership. (Contributed by FL, 10-Aug-2016.)
⊢ (φ → A = B)    &   ⊢ (φ → 𝐶 = 𝐷)    ⇒   ⊢ (φ → (A ∉ 𝐶 ↔ B ∉ 𝐷))
Theorem	nfnel 2282	Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ ℲxA    &   ⊢ ℲxB    ⇒   ⊢ Ⅎx A ∉ B
Theorem	nfneld 2283	Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ (φ → ℲxA)    &   ⊢ (φ → ℲxB)    ⇒   ⊢ (φ → Ⅎx A ∉ B)
2.1.5  Restricted quantification
Syntax	wral 2284	Extend wff notation to include restricted universal quantification.
wff ∀x ∈ A φ
Syntax	wrex 2285	Extend wff notation to include restricted existential quantification.
wff ∃x ∈ A φ
Syntax	wreu 2286	Extend wff notation to include restricted existential uniqueness.
wff ∃!x ∈ A φ
Syntax	wrmo 2287	Extend wff notation to include restricted "at most one."
wff ∃*x ∈ A φ
Syntax	crab 2288	Extend class notation to include the restricted class abstraction (class builder).
class {x ∈ A ∣ φ}
Definition	df-ral 2289	Define restricted universal quantification. Special case of Definition 4.15(3) of [TakeutiZaring] p. 22. (Contributed by NM, 19-Aug-1993.)
⊢ (∀x ∈ A φ ↔ ∀x(x ∈ A → φ))
Definition	df-rex 2290	Define restricted existential quantification. Special case of Definition 4.15(4) of [TakeutiZaring] p. 22. (Contributed by NM, 30-Aug-1993.)
⊢ (∃x ∈ A φ ↔ ∃x(x ∈ A ∧ φ))
Definition	df-reu 2291	Define restricted existential uniqueness. (Contributed by NM, 22-Nov-1994.)
⊢ (∃!x ∈ A φ ↔ ∃!x(x ∈ A ∧ φ))
Definition	df-rmo 2292	Define restricted "at most one". (Contributed by NM, 16-Jun-2017.)
⊢ (∃*x ∈ A φ ↔ ∃*x(x ∈ A ∧ φ))
Definition	df-rab 2293	Define a restricted class abstraction (class builder), which is the class of all x in A such that φ is true. Definition of [TakeutiZaring] p. 20. (Contributed by NM, 22-Nov-1994.)
⊢ {x ∈ A ∣ φ} = {x ∣ (x ∈ A ∧ φ)}
Theorem	ralnex 2294	Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.)
⊢ (∀x ∈ A ¬ φ ↔ ¬ ∃x ∈ A φ)
Theorem	rexnalim 2295	Relationship between restricted universal and existential quantifiers. In classical logic this would be a biconditional. (Contributed by Jim Kingdon, 17-Aug-2018.)
⊢ (∃x ∈ A ¬ φ → ¬ ∀x ∈ A φ)
Theorem	ralexim 2296	Relationship between restricted universal and existential quantifiers. (Contributed by Jim Kingdon, 17-Aug-2018.)
⊢ (∀x ∈ A φ → ¬ ∃x ∈ A ¬ φ)
Theorem	rexalim 2297	Relationship between restricted universal and existential quantifiers. (Contributed by Jim Kingdon, 17-Aug-2018.)
⊢ (∃x ∈ A φ → ¬ ∀x ∈ A ¬ φ)
Theorem	ralbida 2298	Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 6-Oct-2003.)
⊢ Ⅎxφ    &   ⊢ ((φ ∧ x ∈ A) → (ψ ↔ χ))    ⇒   ⊢ (φ → (∀x ∈ A ψ ↔ ∀x ∈ A χ))
Theorem	rexbida 2299	Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 6-Oct-2003.)
⊢ Ⅎxφ    &   ⊢ ((φ ∧ x ∈ A) → (ψ ↔ χ))    ⇒   ⊢ (φ → (∃x ∈ A ψ ↔ ∃x ∈ A χ))
Theorem	ralbidva 2300*	Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 4-Mar-1997.)
⊢ ((φ ∧ x ∈ A) → (ψ ↔ χ))    ⇒   ⊢ (φ → (∀x ∈ A ψ ↔ ∀x ∈ A χ))