HomeHome Intuitionistic Logic Explorer
Theorem List (p. 25 of 153)
< 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 - 2401-2500   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremnecon3bid 2401 Deduction from equality to inequality. (Contributed by NM, 23-Feb-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.)
(𝜑 → (𝐴 = 𝐵𝐶 = 𝐷))       (𝜑 → (𝐴𝐵𝐶𝐷))
 
Theoremnecon3ad 2402 Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
(𝜑 → (𝜓𝐴 = 𝐵))       (𝜑 → (𝐴𝐵 → ¬ 𝜓))
 
Theoremnecon3bd 2403 Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
(𝜑 → (𝐴 = 𝐵𝜓))       (𝜑 → (¬ 𝜓𝐴𝐵))
 
Theoremnecon3d 2404 Contrapositive law deduction for inequality. (Contributed by NM, 10-Jun-2006.)
(𝜑 → (𝐴 = 𝐵𝐶 = 𝐷))       (𝜑 → (𝐶𝐷𝐴𝐵))
 
Theoremnesym 2405 Characterization of inequality in terms of reversed equality (see bicom 140). (Contributed by BJ, 7-Jul-2018.)
(𝐴𝐵 ↔ ¬ 𝐵 = 𝐴)
 
Theoremnesymi 2406 Inference associated with nesym 2405. (Contributed by BJ, 7-Jul-2018.)
𝐴𝐵        ¬ 𝐵 = 𝐴
 
Theoremnesymir 2407 Inference associated with nesym 2405. (Contributed by BJ, 7-Jul-2018.)
¬ 𝐴 = 𝐵       𝐵𝐴
 
Theoremnecon3i 2408 Contrapositive inference for inequality. (Contributed by NM, 9-Aug-2006.)
(𝐴 = 𝐵𝐶 = 𝐷)       (𝐶𝐷𝐴𝐵)
 
Theoremnecon3ai 2409 Contrapositive inference for inequality. (Contributed by NM, 23-May-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
(𝜑𝐴 = 𝐵)       (𝐴𝐵 → ¬ 𝜑)
 
Theoremnecon3bi 2410 Contrapositive inference for inequality. (Contributed by NM, 1-Jun-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
(𝐴 = 𝐵𝜑)       𝜑𝐴𝐵)
 
Theoremnecon1aidc 2411 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 15-May-2018.)
(DECID 𝜑 → (¬ 𝜑𝐴 = 𝐵))       (DECID 𝜑 → (𝐴𝐵𝜑))
 
Theoremnecon1bidc 2412 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 15-May-2018.)
(DECID 𝐴 = 𝐵 → (𝐴𝐵𝜑))       (DECID 𝐴 = 𝐵 → (¬ 𝜑𝐴 = 𝐵))
 
Theoremnecon1idc 2413 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
(𝐴𝐵𝐶 = 𝐷)       (DECID 𝐴 = 𝐵 → (𝐶𝐷𝐴 = 𝐵))
 
Theoremnecon2ai 2414 Contrapositive inference for inequality. (Contributed by NM, 16-Jan-2007.) (Proof rewritten by Jim Kingdon, 16-May-2018.)
(𝐴 = 𝐵 → ¬ 𝜑)       (𝜑𝐴𝐵)
 
Theoremnecon2bi 2415 Contrapositive inference for inequality. (Contributed by NM, 1-Apr-2007.)
(𝜑𝐴𝐵)       (𝐴 = 𝐵 → ¬ 𝜑)
 
Theoremnecon2i 2416 Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007.)
(𝐴 = 𝐵𝐶𝐷)       (𝐶 = 𝐷𝐴𝐵)
 
Theoremnecon2ad 2417 Contrapositive inference for inequality. (Contributed by NM, 19-Apr-2007.) (Proof rewritten by Jim Kingdon, 16-May-2018.)
(𝜑 → (𝐴 = 𝐵 → ¬ 𝜓))       (𝜑 → (𝜓𝐴𝐵))
 
Theoremnecon2bd 2418 Contrapositive inference for inequality. (Contributed by NM, 13-Apr-2007.)
(𝜑 → (𝜓𝐴𝐵))       (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓))
 
Theoremnecon2d 2419 Contrapositive inference for inequality. (Contributed by NM, 28-Dec-2008.)
(𝜑 → (𝐴 = 𝐵𝐶𝐷))       (𝜑 → (𝐶 = 𝐷𝐴𝐵))
 
Theoremnecon1abiidc 2420 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
(DECID 𝜑 → (¬ 𝜑𝐴 = 𝐵))       (DECID 𝜑 → (𝐴𝐵𝜑))
 
Theoremnecon1bbiidc 2421 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
(DECID 𝐴 = 𝐵 → (𝐴𝐵𝜑))       (DECID 𝐴 = 𝐵 → (¬ 𝜑𝐴 = 𝐵))
 
Theoremnecon1abiddc 2422 Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
(𝜑 → (DECID 𝜓 → (¬ 𝜓𝐴 = 𝐵)))       (𝜑 → (DECID 𝜓 → (𝐴𝐵𝜓)))
 
Theoremnecon1bbiddc 2423 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
(𝜑 → (DECID 𝐴 = 𝐵 → (𝐴𝐵𝜓)))       (𝜑 → (DECID 𝐴 = 𝐵 → (¬ 𝜓𝐴 = 𝐵)))
 
Theoremnecon2abiidc 2424 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
(DECID 𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜑))       (DECID 𝜑 → (𝜑𝐴𝐵))
 
Theoremnecon2bbiidc 2425 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
(DECID 𝐴 = 𝐵 → (𝜑𝐴𝐵))       (DECID 𝐴 = 𝐵 → (𝐴 = 𝐵 ↔ ¬ 𝜑))
 
Theoremnecon2abiddc 2426 Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
(𝜑 → (DECID 𝜓 → (𝐴 = 𝐵 ↔ ¬ 𝜓)))       (𝜑 → (DECID 𝜓 → (𝜓𝐴𝐵)))
 
Theoremnecon2bbiddc 2427 Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
(𝜑 → (DECID 𝐴 = 𝐵 → (𝜓𝐴𝐵)))       (𝜑 → (DECID 𝐴 = 𝐵 → (𝐴 = 𝐵 ↔ ¬ 𝜓)))
 
Theoremnecon4aidc 2428 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
(DECID 𝐴 = 𝐵 → (𝐴𝐵 → ¬ 𝜑))       (DECID 𝐴 = 𝐵 → (𝜑𝐴 = 𝐵))
 
Theoremnecon4idc 2429 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
(DECID 𝐴 = 𝐵 → (𝐴𝐵𝐶𝐷))       (DECID 𝐴 = 𝐵 → (𝐶 = 𝐷𝐴 = 𝐵))
 
Theoremnecon4addc 2430 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 17-May-2018.)
(𝜑 → (DECID 𝐴 = 𝐵 → (𝐴𝐵 → ¬ 𝜓)))       (𝜑 → (DECID 𝐴 = 𝐵 → (𝜓𝐴 = 𝐵)))
 
Theoremnecon4bddc 2431 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 17-May-2018.)
(𝜑 → (DECID 𝜓 → (¬ 𝜓𝐴𝐵)))       (𝜑 → (DECID 𝜓 → (𝐴 = 𝐵𝜓)))
 
Theoremnecon4ddc 2432 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 17-May-2018.)
(𝜑 → (DECID 𝐴 = 𝐵 → (𝐴𝐵𝐶𝐷)))       (𝜑 → (DECID 𝐴 = 𝐵 → (𝐶 = 𝐷𝐴 = 𝐵)))
 
Theoremnecon4abiddc 2433 Contrapositive law deduction for inequality. (Contributed by Jim Kingdon, 18-May-2018.)
(𝜑 → (DECID 𝐴 = 𝐵 → (DECID 𝜓 → (𝐴𝐵 ↔ ¬ 𝜓))))       (𝜑 → (DECID 𝐴 = 𝐵 → (DECID 𝜓 → (𝐴 = 𝐵𝜓))))
 
Theoremnecon4bbiddc 2434 Contrapositive law deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
(𝜑 → (DECID 𝜓 → (DECID 𝐴 = 𝐵 → (¬ 𝜓𝐴𝐵))))       (𝜑 → (DECID 𝜓 → (DECID 𝐴 = 𝐵 → (𝜓𝐴 = 𝐵))))
 
Theoremnecon4biddc 2435 Contrapositive law deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
(𝜑 → (DECID 𝐴 = 𝐵 → (DECID 𝐶 = 𝐷 → (𝐴𝐵𝐶𝐷))))       (𝜑 → (DECID 𝐴 = 𝐵 → (DECID 𝐶 = 𝐷 → (𝐴 = 𝐵𝐶 = 𝐷))))
 
Theoremnecon1addc 2436 Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
(𝜑 → (DECID 𝜓 → (¬ 𝜓𝐴 = 𝐵)))       (𝜑 → (DECID 𝜓 → (𝐴𝐵𝜓)))
 
Theoremnecon1bddc 2437 Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
(𝜑 → (DECID 𝐴 = 𝐵 → (𝐴𝐵𝜓)))       (𝜑 → (DECID 𝐴 = 𝐵 → (¬ 𝜓𝐴 = 𝐵)))
 
Theoremnecon1ddc 2438 Contrapositive law deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
(𝜑 → (DECID 𝐴 = 𝐵 → (𝐴𝐵𝐶 = 𝐷)))       (𝜑 → (DECID 𝐴 = 𝐵 → (𝐶𝐷𝐴 = 𝐵)))
 
Theoremneneqad 2439 If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2381. One-way deduction form of df-ne 2361. (Contributed by David Moews, 28-Feb-2017.)
(𝜑 → ¬ 𝐴 = 𝐵)       (𝜑𝐴𝐵)
 
Theoremnebidc 2440 Contraposition law for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
(DECID 𝐴 = 𝐵 → (DECID 𝐶 = 𝐷 → ((𝐴 = 𝐵𝐶 = 𝐷) ↔ (𝐴𝐵𝐶𝐷))))
 
Theorempm13.18 2441 Theorem *13.18 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.)
((𝐴 = 𝐵𝐴𝐶) → 𝐵𝐶)
 
Theorempm13.181 2442 Theorem *13.181 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.)
((𝐴 = 𝐵𝐵𝐶) → 𝐴𝐶)
 
Theorempm2.21ddne 2443 A contradiction implies anything. Equality/inequality deduction form. (Contributed by David Moews, 28-Feb-2017.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐴𝐵)       (𝜑𝜓)
 
Theoremnecom 2444 Commutation of inequality. (Contributed by NM, 14-May-1999.)
(𝐴𝐵𝐵𝐴)
 
Theoremnecomi 2445 Inference from commutative law for inequality. (Contributed by NM, 17-Oct-2012.)
𝐴𝐵       𝐵𝐴
 
Theoremnecomd 2446 Deduction from commutative law for inequality. (Contributed by NM, 12-Feb-2008.)
(𝜑𝐴𝐵)       (𝜑𝐵𝐴)
 
Theoremneanior 2447 A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.)
((𝐴𝐵𝐶𝐷) ↔ ¬ (𝐴 = 𝐵𝐶 = 𝐷))
 
Theoremne3anior 2448 A De Morgan's law for inequality. (Contributed by NM, 30-Sep-2013.) (Proof rewritten by Jim Kingdon, 19-May-2018.)
((𝐴𝐵𝐶𝐷𝐸𝐹) ↔ ¬ (𝐴 = 𝐵𝐶 = 𝐷𝐸 = 𝐹))
 
Theoremnemtbir 2449 An inference from an inequality, related to modus tollens. (Contributed by NM, 13-Apr-2007.)
𝐴𝐵    &   (𝜑𝐴 = 𝐵)        ¬ 𝜑
 
Theoremnelne1 2450 Two classes are different if they don't contain the same element. (Contributed by NM, 3-Feb-2012.)
((𝐴𝐵 ∧ ¬ 𝐴𝐶) → 𝐵𝐶)
 
Theoremnelne2 2451 Two classes are different if they don't belong to the same class. (Contributed by NM, 25-Jun-2012.)
((𝐴𝐶 ∧ ¬ 𝐵𝐶) → 𝐴𝐵)
 
Theoremnelelne 2452 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 2453 Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.)
𝑥𝐴    &   𝑥𝐵       𝑥 𝐴𝐵
 
Theoremnfned 2454 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 2455 Extend wff notation to include negated membership.
wff 𝐴𝐵
 
Definitiondf-nel 2456 Define negated membership. (Contributed by NM, 7-Aug-1994.)
(𝐴𝐵 ↔ ¬ 𝐴𝐵)
 
Theoremneli 2457 Inference associated with df-nel 2456. (Contributed by BJ, 7-Jul-2018.)
𝐴𝐵        ¬ 𝐴𝐵
 
Theoremnelir 2458 Inference associated with df-nel 2456. (Contributed by BJ, 7-Jul-2018.)
¬ 𝐴𝐵       𝐴𝐵
 
Theoremneleq1 2459 Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.)
(𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
 
Theoremneleq2 2460 Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.)
(𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
 
Theoremneleq12d 2461 Equality theorem for negated membership. (Contributed by FL, 10-Aug-2016.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐶 = 𝐷)       (𝜑 → (𝐴𝐶𝐵𝐷))
 
Theoremnfnel 2462 Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.)
𝑥𝐴    &   𝑥𝐵       𝑥 𝐴𝐵
 
Theoremnfneld 2463 Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.)
(𝜑𝑥𝐴)    &   (𝜑𝑥𝐵)       (𝜑 → Ⅎ𝑥 𝐴𝐵)
 
Theoremelnelne1 2464 Two classes are different if they don't contain the same element. (Contributed by AV, 28-Jan-2020.)
((𝐴𝐵𝐴𝐶) → 𝐵𝐶)
 
Theoremelnelne2 2465 Two classes are different if they don't belong to the same class. (Contributed by AV, 28-Jan-2020.)
((𝐴𝐶𝐵𝐶) → 𝐴𝐵)
 
Theoremnelcon3d 2466 Contrapositive law deduction for negated membership. (Contributed by AV, 28-Jan-2020.)
(𝜑 → (𝐴𝐵𝐶𝐷))       (𝜑 → (𝐶𝐷𝐴𝐵))
 
Theoremelnelall 2467 A contradiction concerning membership implies anything. (Contributed by Alexander van der Vekens, 25-Jan-2018.)
(𝐴𝐵 → (𝐴𝐵𝜑))
 
2.1.5  Restricted quantification
 
Syntaxwral 2468 Extend wff notation to include restricted universal quantification.
wff 𝑥𝐴 𝜑
 
Syntaxwrex 2469 Extend wff notation to include restricted existential quantification.
wff 𝑥𝐴 𝜑
 
Syntaxwreu 2470 Extend wff notation to include restricted existential uniqueness.
wff ∃!𝑥𝐴 𝜑
 
Syntaxwrmo 2471 Extend wff notation to include restricted "at most one".
wff ∃*𝑥𝐴 𝜑
 
Syntaxcrab 2472 Extend class notation to include the restricted class abstraction (class builder).
class {𝑥𝐴𝜑}
 
Definitiondf-ral 2473 Define restricted universal quantification. Special case of Definition 4.15(3) of [TakeutiZaring] p. 22. (Contributed by NM, 19-Aug-1993.)
(∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
 
Definitiondf-rex 2474 Define restricted existential quantification. Special case of Definition 4.15(4) of [TakeutiZaring] p. 22. (Contributed by NM, 30-Aug-1993.)
(∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
 
Definitiondf-reu 2475 Define restricted existential uniqueness. (Contributed by NM, 22-Nov-1994.)
(∃!𝑥𝐴 𝜑 ↔ ∃!𝑥(𝑥𝐴𝜑))
 
Definitiondf-rmo 2476 Define restricted "at most one". (Contributed by NM, 16-Jun-2017.)
(∃*𝑥𝐴 𝜑 ↔ ∃*𝑥(𝑥𝐴𝜑))
 
Definitiondf-rab 2477 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 2478 Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.)
(∀𝑥𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥𝐴 𝜑)
 
Theoremrexnalim 2479 Relationship between restricted universal and existential quantifiers. In classical logic this would be a biconditional. (Contributed by Jim Kingdon, 17-Aug-2018.)
(∃𝑥𝐴 ¬ 𝜑 → ¬ ∀𝑥𝐴 𝜑)
 
Theoremnnral 2480 The double negation of a universal quantification implies the universal quantification of the double negation. Restricted quantifier version of nnal 1660. (Contributed by Jim Kingdon, 1-Aug-2024.)
(¬ ¬ ∀𝑥𝐴 𝜑 → ∀𝑥𝐴 ¬ ¬ 𝜑)
 
Theoremdfrex2dc 2481 Relationship between restricted universal and existential quantifiers. (Contributed by Jim Kingdon, 29-Jun-2022.)
(DECID𝑥𝐴 𝜑 → (∃𝑥𝐴 𝜑 ↔ ¬ ∀𝑥𝐴 ¬ 𝜑))
 
Theoremralexim 2482 Relationship between restricted universal and existential quantifiers. (Contributed by Jim Kingdon, 17-Aug-2018.)
(∀𝑥𝐴 𝜑 → ¬ ∃𝑥𝐴 ¬ 𝜑)
 
Theoremrexalim 2483 Relationship between restricted universal and existential quantifiers. (Contributed by Jim Kingdon, 17-Aug-2018.)
(∃𝑥𝐴 𝜑 → ¬ ∀𝑥𝐴 ¬ 𝜑)
 
Theoremralbida 2484 Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 6-Oct-2003.)
𝑥𝜑    &   ((𝜑𝑥𝐴) → (𝜓𝜒))       (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))
 
Theoremrexbida 2485 Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 6-Oct-2003.)
𝑥𝜑    &   ((𝜑𝑥𝐴) → (𝜓𝜒))       (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐴 𝜒))
 
Theoremralbidva 2486* Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 4-Mar-1997.)
((𝜑𝑥𝐴) → (𝜓𝜒))       (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))
 
Theoremrexbidva 2487* Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 9-Mar-1997.)
((𝜑𝑥𝐴) → (𝜓𝜒))       (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐴 𝜒))
 
Theoremralbid 2488 Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 27-Jun-1998.)
𝑥𝜑    &   (𝜑 → (𝜓𝜒))       (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))
 
Theoremrexbid 2489 Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 27-Jun-1998.)
𝑥𝜑    &   (𝜑 → (𝜓𝜒))       (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐴 𝜒))
 
Theoremralbidv 2490* Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 20-Nov-1994.)
(𝜑 → (𝜓𝜒))       (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))
 
Theoremrexbidv 2491* Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 20-Nov-1994.)
(𝜑 → (𝜓𝜒))       (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐴 𝜒))
 
Theoremralbidv2 2492* Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 6-Apr-1997.)
(𝜑 → ((𝑥𝐴𝜓) ↔ (𝑥𝐵𝜒)))       (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐵 𝜒))
 
Theoremrexbidv2 2493* Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 22-May-1999.)
(𝜑 → ((𝑥𝐴𝜓) ↔ (𝑥𝐵𝜒)))       (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐵 𝜒))
 
Theoremralbid2 2494 Formula-building rule for restricted universal quantifier (deduction form). (Contributed by BJ, 14-Jul-2024.)
𝑥𝜑    &   (𝜑 → ((𝑥𝐴𝜓) ↔ (𝑥𝐵𝜒)))       (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐵 𝜒))
 
Theoremrexbid2 2495 Formula-building rule for restricted existential quantifier (deduction form). (Contributed by BJ, 14-Jul-2024.)
𝑥𝜑    &   (𝜑 → ((𝑥𝐴𝜓) ↔ (𝑥𝐵𝜒)))       (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐵 𝜒))
 
Theoremralbii 2496 Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 23-Nov-1994.) (Revised by Mario Carneiro, 17-Oct-2016.)
(𝜑𝜓)       (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 𝜓)
 
Theoremrexbii 2497 Inference adding restricted existential quantifier to both sides of an equivalence. (Contributed by NM, 23-Nov-1994.) (Revised by Mario Carneiro, 17-Oct-2016.)
(𝜑𝜓)       (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐴 𝜓)
 
Theorem2ralbii 2498 Inference adding two restricted universal quantifiers to both sides of an equivalence. (Contributed by NM, 1-Aug-2004.)
(𝜑𝜓)       (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑥𝐴𝑦𝐵 𝜓)
 
Theorem2rexbii 2499 Inference adding two restricted existential quantifiers to both sides of an equivalence. (Contributed by NM, 11-Nov-1995.)
(𝜑𝜓)       (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑥𝐴𝑦𝐵 𝜓)
 
Theoremralbii2 2500 Inference adding different restricted universal quantifiers to each side of an equivalence. (Contributed by NM, 15-Aug-2005.)
((𝑥𝐴𝜑) ↔ (𝑥𝐵𝜓))       (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐵 𝜓)
    < Previous  Next >

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-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15294
  Copyright terms: Public domain < Previous  Next >