 Home Intuitionistic Logic ExplorerTheorem List (p. 24 of 130) < Previous  Next > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 2301-2400   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremneneqd 2301 Deduction eliminating inequality definition. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
(𝜑𝐴𝐵)       (𝜑 → ¬ 𝐴 = 𝐵)

Theoremneneq 2302 From inequality to non-equality. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(𝐴𝐵 → ¬ 𝐴 = 𝐵)

Theoremeqnetri 2303 Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
𝐴 = 𝐵    &   𝐵𝐶       𝐴𝐶

Theoremeqnetrd 2304 Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐵𝐶)       (𝜑𝐴𝐶)

Theoremeqnetrri 2305 Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
𝐴 = 𝐵    &   𝐴𝐶       𝐵𝐶

Theoremeqnetrrd 2306 Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐴𝐶)       (𝜑𝐵𝐶)

Theoremneeqtri 2307 Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
𝐴𝐵    &   𝐵 = 𝐶       𝐴𝐶

Theoremneeqtrd 2308 Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
(𝜑𝐴𝐵)    &   (𝜑𝐵 = 𝐶)       (𝜑𝐴𝐶)

Theoremneeqtrri 2309 Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
𝐴𝐵    &   𝐶 = 𝐵       𝐴𝐶

Theoremneeqtrrd 2310 Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
(𝜑𝐴𝐵)    &   (𝜑𝐶 = 𝐵)       (𝜑𝐴𝐶)

Theoremsyl5eqner 2311 B chained equality inference for inequality. (Contributed by NM, 6-Jun-2012.)
𝐵 = 𝐴    &   (𝜑𝐵𝐶)       (𝜑𝐴𝐶)

Theorem3netr3d 2312 Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.)
(𝜑𝐴𝐵)    &   (𝜑𝐴 = 𝐶)    &   (𝜑𝐵 = 𝐷)       (𝜑𝐶𝐷)

Theorem3netr4d 2313 Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.)
(𝜑𝐴𝐵)    &   (𝜑𝐶 = 𝐴)    &   (𝜑𝐷 = 𝐵)       (𝜑𝐶𝐷)

Theorem3netr3g 2314 Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.)
(𝜑𝐴𝐵)    &   𝐴 = 𝐶    &   𝐵 = 𝐷       (𝜑𝐶𝐷)

Theorem3netr4g 2315 Substitution of equality into both sides of an inequality. (Contributed by NM, 14-Jun-2012.)
(𝜑𝐴𝐵)    &   𝐶 = 𝐴    &   𝐷 = 𝐵       (𝜑𝐶𝐷)

Theoremnecon3abii 2316 Deduction from equality to inequality. (Contributed by NM, 9-Nov-2007.)
(𝐴 = 𝐵𝜑)       (𝐴𝐵 ↔ ¬ 𝜑)

Theoremnecon3bbii 2317 Deduction from equality to inequality. (Contributed by NM, 13-Apr-2007.)
(𝜑𝐴 = 𝐵)       𝜑𝐴𝐵)

Theoremnecon3bii 2318 Inference from equality to inequality. (Contributed by NM, 23-Feb-2005.)
(𝐴 = 𝐵𝐶 = 𝐷)       (𝐴𝐵𝐶𝐷)

Theoremnecon3abid 2319 Deduction from equality to inequality. (Contributed by NM, 21-Mar-2007.)
(𝜑 → (𝐴 = 𝐵𝜓))       (𝜑 → (𝐴𝐵 ↔ ¬ 𝜓))

Theoremnecon3bbid 2320 Deduction from equality to inequality. (Contributed by NM, 2-Jun-2007.)
(𝜑 → (𝜓𝐴 = 𝐵))       (𝜑 → (¬ 𝜓𝐴𝐵))

Theoremnecon3bid 2321 Deduction from equality to inequality. (Contributed by NM, 23-Feb-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.)
(𝜑 → (𝐴 = 𝐵𝐶 = 𝐷))       (𝜑 → (𝐴𝐵𝐶𝐷))

Theoremnecon3ad 2322 Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
(𝜑 → (𝜓𝐴 = 𝐵))       (𝜑 → (𝐴𝐵 → ¬ 𝜓))

Theoremnecon3bd 2323 Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
(𝜑 → (𝐴 = 𝐵𝜓))       (𝜑 → (¬ 𝜓𝐴𝐵))

Theoremnecon3d 2324 Contrapositive law deduction for inequality. (Contributed by NM, 10-Jun-2006.)
(𝜑 → (𝐴 = 𝐵𝐶 = 𝐷))       (𝜑 → (𝐶𝐷𝐴𝐵))

Theoremnesym 2325 Characterization of inequality in terms of reversed equality (see bicom 139). (Contributed by BJ, 7-Jul-2018.)
(𝐴𝐵 ↔ ¬ 𝐵 = 𝐴)

Theoremnesymi 2326 Inference associated with nesym 2325. (Contributed by BJ, 7-Jul-2018.)
𝐴𝐵        ¬ 𝐵 = 𝐴

Theoremnesymir 2327 Inference associated with nesym 2325. (Contributed by BJ, 7-Jul-2018.)
¬ 𝐴 = 𝐵       𝐵𝐴

Theoremnecon3i 2328 Contrapositive inference for inequality. (Contributed by NM, 9-Aug-2006.)
(𝐴 = 𝐵𝐶 = 𝐷)       (𝐶𝐷𝐴𝐵)

Theoremnecon3ai 2329 Contrapositive inference for inequality. (Contributed by NM, 23-May-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
(𝜑𝐴 = 𝐵)       (𝐴𝐵 → ¬ 𝜑)

Theoremnecon3bi 2330 Contrapositive inference for inequality. (Contributed by NM, 1-Jun-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
(𝐴 = 𝐵𝜑)       𝜑𝐴𝐵)

Theoremnecon1aidc 2331 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 15-May-2018.)
(DECID 𝜑 → (¬ 𝜑𝐴 = 𝐵))       (DECID 𝜑 → (𝐴𝐵𝜑))

Theoremnecon1bidc 2332 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 15-May-2018.)
(DECID 𝐴 = 𝐵 → (𝐴𝐵𝜑))       (DECID 𝐴 = 𝐵 → (¬ 𝜑𝐴 = 𝐵))

Theoremnecon1idc 2333 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
(𝐴𝐵𝐶 = 𝐷)       (DECID 𝐴 = 𝐵 → (𝐶𝐷𝐴 = 𝐵))

Theoremnecon2ai 2334 Contrapositive inference for inequality. (Contributed by NM, 16-Jan-2007.) (Proof rewritten by Jim Kingdon, 16-May-2018.)
(𝐴 = 𝐵 → ¬ 𝜑)       (𝜑𝐴𝐵)

Theoremnecon2bi 2335 Contrapositive inference for inequality. (Contributed by NM, 1-Apr-2007.)
(𝜑𝐴𝐵)       (𝐴 = 𝐵 → ¬ 𝜑)

Theoremnecon2i 2336 Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007.)
(𝐴 = 𝐵𝐶𝐷)       (𝐶 = 𝐷𝐴𝐵)

Theoremnecon2ad 2337 Contrapositive inference for inequality. (Contributed by NM, 19-Apr-2007.) (Proof rewritten by Jim Kingdon, 16-May-2018.)
(𝜑 → (𝐴 = 𝐵 → ¬ 𝜓))       (𝜑 → (𝜓𝐴𝐵))

Theoremnecon2bd 2338 Contrapositive inference for inequality. (Contributed by NM, 13-Apr-2007.)
(𝜑 → (𝜓𝐴𝐵))       (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓))

Theoremnecon2d 2339 Contrapositive inference for inequality. (Contributed by NM, 28-Dec-2008.)
(𝜑 → (𝐴 = 𝐵𝐶𝐷))       (𝜑 → (𝐶 = 𝐷𝐴𝐵))

Theoremnecon1abiidc 2340 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
(DECID 𝜑 → (¬ 𝜑𝐴 = 𝐵))       (DECID 𝜑 → (𝐴𝐵𝜑))

Theoremnecon1bbiidc 2341 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
(DECID 𝐴 = 𝐵 → (𝐴𝐵𝜑))       (DECID 𝐴 = 𝐵 → (¬ 𝜑𝐴 = 𝐵))

Theoremnecon1abiddc 2342 Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
(𝜑 → (DECID 𝜓 → (¬ 𝜓𝐴 = 𝐵)))       (𝜑 → (DECID 𝜓 → (𝐴𝐵𝜓)))

Theoremnecon1bbiddc 2343 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
(𝜑 → (DECID 𝐴 = 𝐵 → (𝐴𝐵𝜓)))       (𝜑 → (DECID 𝐴 = 𝐵 → (¬ 𝜓𝐴 = 𝐵)))

Theoremnecon2abiidc 2344 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
(DECID 𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜑))       (DECID 𝜑 → (𝜑𝐴𝐵))

Theoremnecon2bbiidc 2345 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
(DECID 𝐴 = 𝐵 → (𝜑𝐴𝐵))       (DECID 𝐴 = 𝐵 → (𝐴 = 𝐵 ↔ ¬ 𝜑))

Theoremnecon2abiddc 2346 Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
(𝜑 → (DECID 𝜓 → (𝐴 = 𝐵 ↔ ¬ 𝜓)))       (𝜑 → (DECID 𝜓 → (𝜓𝐴𝐵)))

Theoremnecon2bbiddc 2347 Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
(𝜑 → (DECID 𝐴 = 𝐵 → (𝜓𝐴𝐵)))       (𝜑 → (DECID 𝐴 = 𝐵 → (𝐴 = 𝐵 ↔ ¬ 𝜓)))

Theoremnecon4aidc 2348 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
(DECID 𝐴 = 𝐵 → (𝐴𝐵 → ¬ 𝜑))       (DECID 𝐴 = 𝐵 → (𝜑𝐴 = 𝐵))

Theoremnecon4idc 2349 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
(DECID 𝐴 = 𝐵 → (𝐴𝐵𝐶𝐷))       (DECID 𝐴 = 𝐵 → (𝐶 = 𝐷𝐴 = 𝐵))

Theoremnecon4addc 2350 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 17-May-2018.)
(𝜑 → (DECID 𝐴 = 𝐵 → (𝐴𝐵 → ¬ 𝜓)))       (𝜑 → (DECID 𝐴 = 𝐵 → (𝜓𝐴 = 𝐵)))

Theoremnecon4bddc 2351 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 17-May-2018.)
(𝜑 → (DECID 𝜓 → (¬ 𝜓𝐴𝐵)))       (𝜑 → (DECID 𝜓 → (𝐴 = 𝐵𝜓)))

Theoremnecon4ddc 2352 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 17-May-2018.)
(𝜑 → (DECID 𝐴 = 𝐵 → (𝐴𝐵𝐶𝐷)))       (𝜑 → (DECID 𝐴 = 𝐵 → (𝐶 = 𝐷𝐴 = 𝐵)))

Theoremnecon4abiddc 2353 Contrapositive law deduction for inequality. (Contributed by Jim Kingdon, 18-May-2018.)
(𝜑 → (DECID 𝐴 = 𝐵 → (DECID 𝜓 → (𝐴𝐵 ↔ ¬ 𝜓))))       (𝜑 → (DECID 𝐴 = 𝐵 → (DECID 𝜓 → (𝐴 = 𝐵𝜓))))

Theoremnecon4bbiddc 2354 Contrapositive law deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
(𝜑 → (DECID 𝜓 → (DECID 𝐴 = 𝐵 → (¬ 𝜓𝐴𝐵))))       (𝜑 → (DECID 𝜓 → (DECID 𝐴 = 𝐵 → (𝜓𝐴 = 𝐵))))

Theoremnecon4biddc 2355 Contrapositive law deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
(𝜑 → (DECID 𝐴 = 𝐵 → (DECID 𝐶 = 𝐷 → (𝐴𝐵𝐶𝐷))))       (𝜑 → (DECID 𝐴 = 𝐵 → (DECID 𝐶 = 𝐷 → (𝐴 = 𝐵𝐶 = 𝐷))))

Theoremnecon1addc 2356 Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
(𝜑 → (DECID 𝜓 → (¬ 𝜓𝐴 = 𝐵)))       (𝜑 → (DECID 𝜓 → (𝐴𝐵𝜓)))

Theoremnecon1bddc 2357 Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
(𝜑 → (DECID 𝐴 = 𝐵 → (𝐴𝐵𝜓)))       (𝜑 → (DECID 𝐴 = 𝐵 → (¬ 𝜓𝐴 = 𝐵)))

Theoremnecon1ddc 2358 Contrapositive law deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
(𝜑 → (DECID 𝐴 = 𝐵 → (𝐴𝐵𝐶 = 𝐷)))       (𝜑 → (DECID 𝐴 = 𝐵 → (𝐶𝐷𝐴 = 𝐵)))

Theoremneneqad 2359 If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2301. One-way deduction form of df-ne 2281. (Contributed by David Moews, 28-Feb-2017.)
(𝜑 → ¬ 𝐴 = 𝐵)       (𝜑𝐴𝐵)

Theoremnebidc 2360 Contraposition law for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
(DECID 𝐴 = 𝐵 → (DECID 𝐶 = 𝐷 → ((𝐴 = 𝐵𝐶 = 𝐷) ↔ (𝐴𝐵𝐶𝐷))))

Theorempm13.18 2361 Theorem *13.18 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.)
((𝐴 = 𝐵𝐴𝐶) → 𝐵𝐶)

Theorempm13.181 2362 Theorem *13.181 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.)
((𝐴 = 𝐵𝐵𝐶) → 𝐴𝐶)

Theorempm2.21ddne 2363 A contradiction implies anything. Equality/inequality deduction form. (Contributed by David Moews, 28-Feb-2017.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐴𝐵)       (𝜑𝜓)

Theoremnecom 2364 Commutation of inequality. (Contributed by NM, 14-May-1999.)
(𝐴𝐵𝐵𝐴)

Theoremnecomi 2365 Inference from commutative law for inequality. (Contributed by NM, 17-Oct-2012.)
𝐴𝐵       𝐵𝐴

Theoremnecomd 2366 Deduction from commutative law for inequality. (Contributed by NM, 12-Feb-2008.)
(𝜑𝐴𝐵)       (𝜑𝐵𝐴)

Theoremneanior 2367 A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.)
((𝐴𝐵𝐶𝐷) ↔ ¬ (𝐴 = 𝐵𝐶 = 𝐷))

Theoremne3anior 2368 A De Morgan's law for inequality. (Contributed by NM, 30-Sep-2013.) (Proof rewritten by Jim Kingdon, 19-May-2018.)
((𝐴𝐵𝐶𝐷𝐸𝐹) ↔ ¬ (𝐴 = 𝐵𝐶 = 𝐷𝐸 = 𝐹))

Theoremnemtbir 2369 An inference from an inequality, related to modus tollens. (Contributed by NM, 13-Apr-2007.)
𝐴𝐵    &   (𝜑𝐴 = 𝐵)        ¬ 𝜑

Theoremnelne1 2370 Two classes are different if they don't contain the same element. (Contributed by NM, 3-Feb-2012.)
((𝐴𝐵 ∧ ¬ 𝐴𝐶) → 𝐵𝐶)

Theoremnelne2 2371 Two classes are different if they don't belong to the same class. (Contributed by NM, 25-Jun-2012.)
((𝐴𝐶 ∧ ¬ 𝐵𝐶) → 𝐴𝐵)

Theoremnelelne 2372 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.)
𝐴𝐵 → (𝐶𝐵𝐶𝐴))

Theoremnfne 2373 Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.)
𝑥𝐴    &   𝑥𝐵       𝑥 𝐴𝐵

Theoremnfned 2374 Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.)
(𝜑𝑥𝐴)    &   (𝜑𝑥𝐵)       (𝜑 → Ⅎ𝑥 𝐴𝐵)

2.1.4.2  Negated membership

Syntaxwnel 2375 Extend wff notation to include negated membership.
wff 𝐴𝐵

Definitiondf-nel 2376 Define negated membership. (Contributed by NM, 7-Aug-1994.)
(𝐴𝐵 ↔ ¬ 𝐴𝐵)

Theoremneli 2377 Inference associated with df-nel 2376. (Contributed by BJ, 7-Jul-2018.)
𝐴𝐵        ¬ 𝐴𝐵

Theoremnelir 2378 Inference associated with df-nel 2376. (Contributed by BJ, 7-Jul-2018.)
¬ 𝐴𝐵       𝐴𝐵

Theoremneleq1 2379 Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.)
(𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))

Theoremneleq2 2380 Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.)
(𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))

Theoremneleq12d 2381 Equality theorem for negated membership. (Contributed by FL, 10-Aug-2016.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐶 = 𝐷)       (𝜑 → (𝐴𝐶𝐵𝐷))

Theoremnfnel 2382 Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.)
𝑥𝐴    &   𝑥𝐵       𝑥 𝐴𝐵

Theoremnfneld 2383 Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.)
(𝜑𝑥𝐴)    &   (𝜑𝑥𝐵)       (𝜑 → Ⅎ𝑥 𝐴𝐵)

Theoremelnelne1 2384 Two classes are different if they don't contain the same element. (Contributed by AV, 28-Jan-2020.)
((𝐴𝐵𝐴𝐶) → 𝐵𝐶)

Theoremelnelne2 2385 Two classes are different if they don't belong to the same class. (Contributed by AV, 28-Jan-2020.)
((𝐴𝐶𝐵𝐶) → 𝐴𝐵)

Theoremnelcon3d 2386 Contrapositive law deduction for negated membership. (Contributed by AV, 28-Jan-2020.)
(𝜑 → (𝐴𝐵𝐶𝐷))       (𝜑 → (𝐶𝐷𝐴𝐵))

Theoremelnelall 2387 A contradiction concerning membership implies anything. (Contributed by Alexander van der Vekens, 25-Jan-2018.)
(𝐴𝐵 → (𝐴𝐵𝜑))

2.1.5  Restricted quantification

Syntaxwral 2388 Extend wff notation to include restricted universal quantification.
wff 𝑥𝐴 𝜑

Syntaxwrex 2389 Extend wff notation to include restricted existential quantification.
wff 𝑥𝐴 𝜑

Syntaxwreu 2390 Extend wff notation to include restricted existential uniqueness.
wff ∃!𝑥𝐴 𝜑

Syntaxwrmo 2391 Extend wff notation to include restricted "at most one."
wff ∃*𝑥𝐴 𝜑

Syntaxcrab 2392 Extend class notation to include the restricted class abstraction (class builder).
class {𝑥𝐴𝜑}

Definitiondf-ral 2393 Define restricted universal quantification. Special case of Definition 4.15(3) of [TakeutiZaring] p. 22. (Contributed by NM, 19-Aug-1993.)
(∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))

Definitiondf-rex 2394 Define restricted existential quantification. Special case of Definition 4.15(4) of [TakeutiZaring] p. 22. (Contributed by NM, 30-Aug-1993.)
(∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))

Definitiondf-reu 2395 Define restricted existential uniqueness. (Contributed by NM, 22-Nov-1994.)
(∃!𝑥𝐴 𝜑 ↔ ∃!𝑥(𝑥𝐴𝜑))

Definitiondf-rmo 2396 Define restricted "at most one". (Contributed by NM, 16-Jun-2017.)
(∃*𝑥𝐴 𝜑 ↔ ∃*𝑥(𝑥𝐴𝜑))

Definitiondf-rab 2397 Define a restricted class abstraction (class builder), which is the class of all 𝑥 in 𝐴 such that 𝜑 is true. Definition of [TakeutiZaring] p. 20. (Contributed by NM, 22-Nov-1994.)
{𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}

Theoremralnex 2398 Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.)
(∀𝑥𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥𝐴 𝜑)

Theoremrexnalim 2399 Relationship between restricted universal and existential quantifiers. In classical logic this would be a biconditional. (Contributed by Jim Kingdon, 17-Aug-2018.)
(∃𝑥𝐴 ¬ 𝜑 → ¬ ∀𝑥𝐴 𝜑)

Theoremdfrex2dc 2400 Relationship between restricted universal and existential quantifiers. (Contributed by Jim Kingdon, 29-Jun-2022.)
(DECID𝑥𝐴 𝜑 → (∃𝑥𝐴 𝜑 ↔ ¬ ∀𝑥𝐴 ¬ 𝜑))

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-12930
 Copyright terms: Public domain < Previous  Next >