 Home Intuitionistic Logic ExplorerTheorem List (p. 35 of 95) < 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 - 3401-3500   *Has distinct variable group(s)
TypeLabelDescription
Statement

TheoremrexsnsOLD 3401* Restricted existential quantification over a singleton. (Contributed by Mario Carneiro, 23-Apr-2015.) Obsolete as of 22-Aug-2018. Use rexsns 3400 instead. (New usage is discouraged.) (Proof modification is discouraged.)
(A 𝑉 → (x {A}φ[A / x]φ))

Theoremralsng 3402* Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.)
(x = A → (φψ))       (A 𝑉 → (x {A}φψ))

Theoremrexsng 3403* Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012.)
(x = A → (φψ))       (A 𝑉 → (x {A}φψ))

Theoremexsnrex 3404 There is a set being the element of a singleton if and only if there is an element of the singleton. (Contributed by Alexander van der Vekens, 1-Jan-2018.)
(x 𝑀 = {x} ↔ x 𝑀 𝑀 = {x})

Theoremralsn 3405* Convert a quantification over a singleton to a substitution. (Contributed by NM, 27-Apr-2009.)
A V    &   (x = A → (φψ))       (x {A}φψ)

Theoremrexsn 3406* Restricted existential quantification over a singleton. (Contributed by Jeff Madsen, 5-Jan-2011.)
A V    &   (x = A → (φψ))       (x {A}φψ)

Theoremeltpg 3407 Members of an unordered triple of classes. (Contributed by FL, 2-Feb-2014.) (Proof shortened by Mario Carneiro, 11-Feb-2015.)
(A 𝑉 → (A {B, 𝐶, 𝐷} ↔ (A = B A = 𝐶 A = 𝐷)))

Theoremeltpi 3408 A member of an unordered triple of classes is one of them. (Contributed by Mario Carneiro, 11-Feb-2015.)
(A {B, 𝐶, 𝐷} → (A = B A = 𝐶 A = 𝐷))

Theoremeltp 3409 A member of an unordered triple of classes is one of them. Special case of Exercise 1 of [TakeutiZaring] p. 17. (Contributed by NM, 8-Apr-1994.) (Revised by Mario Carneiro, 11-Feb-2015.)
A V       (A {B, 𝐶, 𝐷} ↔ (A = B A = 𝐶 A = 𝐷))

Theoremdftp2 3410* Alternate definition of unordered triple of classes. Special case of Definition 5.3 of [TakeutiZaring] p. 16. (Contributed by NM, 8-Apr-1994.)
{A, B, 𝐶} = {x ∣ (x = A x = B x = 𝐶)}

Theoremnfpr 3411 Bound-variable hypothesis builder for unordered pairs. (Contributed by NM, 14-Nov-1995.)
xA    &   xB       x{A, B}

Theoremralprg 3412* Convert a quantification over a pair to a conjunction. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
(x = A → (φψ))    &   (x = B → (φχ))       ((A 𝑉 B 𝑊) → (x {A, B}φ ↔ (ψ χ)))

Theoremrexprg 3413* Convert a quantification over a pair to a disjunction. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
(x = A → (φψ))    &   (x = B → (φχ))       ((A 𝑉 B 𝑊) → (x {A, B}φ ↔ (ψ χ)))

Theoremraltpg 3414* Convert a quantification over a triple to a conjunction. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
(x = A → (φψ))    &   (x = B → (φχ))    &   (x = 𝐶 → (φθ))       ((A 𝑉 B 𝑊 𝐶 𝑋) → (x {A, B, 𝐶}φ ↔ (ψ χ θ)))

Theoremrextpg 3415* Convert a quantification over a triple to a disjunction. (Contributed by Mario Carneiro, 23-Apr-2015.)
(x = A → (φψ))    &   (x = B → (φχ))    &   (x = 𝐶 → (φθ))       ((A 𝑉 B 𝑊 𝐶 𝑋) → (x {A, B, 𝐶}φ ↔ (ψ χ θ)))

Theoremralpr 3416* Convert a quantification over a pair to a conjunction. (Contributed by NM, 3-Jun-2007.) (Revised by Mario Carneiro, 23-Apr-2015.)
A V    &   B V    &   (x = A → (φψ))    &   (x = B → (φχ))       (x {A, B}φ ↔ (ψ χ))

Theoremrexpr 3417* Convert an existential quantification over a pair to a disjunction. (Contributed by NM, 3-Jun-2007.) (Revised by Mario Carneiro, 23-Apr-2015.)
A V    &   B V    &   (x = A → (φψ))    &   (x = B → (φχ))       (x {A, B}φ ↔ (ψ χ))

Theoremraltp 3418* Convert a quantification over a triple to a conjunction. (Contributed by NM, 13-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
A V    &   B V    &   𝐶 V    &   (x = A → (φψ))    &   (x = B → (φχ))    &   (x = 𝐶 → (φθ))       (x {A, B, 𝐶}φ ↔ (ψ χ θ))

Theoremrextp 3419* Convert a quantification over a triple to a disjunction. (Contributed by Mario Carneiro, 23-Apr-2015.)
A V    &   B V    &   𝐶 V    &   (x = A → (φψ))    &   (x = B → (φχ))    &   (x = 𝐶 → (φθ))       (x {A, B, 𝐶}φ ↔ (ψ χ θ))

Theoremsbcsng 3420* Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.)
(A 𝑉 → ([A / x]φx {A}φ))

Theoremnfsn 3421 Bound-variable hypothesis builder for singletons. (Contributed by NM, 14-Nov-1995.)
xA       x{A}

Theoremcsbsng 3422 Distribute proper substitution through the singleton of a class. (Contributed by Alan Sare, 10-Nov-2012.)
(A 𝑉A / x{B} = {A / xB})

Theoremdisjsn 3423 Intersection with the singleton of a non-member is disjoint. (Contributed by NM, 22-May-1998.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) (Proof shortened by Wolf Lammen, 30-Sep-2014.)
((A ∩ {B}) = ∅ ↔ ¬ B A)

Theoremdisjsn2 3424 Intersection of distinct singletons is disjoint. (Contributed by NM, 25-May-1998.)
(AB → ({A} ∩ {B}) = ∅)

Theoremdisjpr2 3425 The intersection of distinct unordered pairs is disjoint. (Contributed by Alexander van der Vekens, 11-Nov-2017.)
(((A𝐶 B𝐶) (A𝐷 B𝐷)) → ({A, B} ∩ {𝐶, 𝐷}) = ∅)

Theoremsnprc 3426 The singleton of a proper class (one that doesn't exist) is the empty set. Theorem 7.2 of [Quine] p. 48. (Contributed by NM, 5-Aug-1993.)
A V ↔ {A} = ∅)

Theoremr19.12sn 3427* Special case of r19.12 2416 where its converse holds. (Contributed by NM, 19-May-2008.) (Revised by Mario Carneiro, 23-Apr-2015.)
A V       (x {A}y B φy B x {A}φ)

Theoremrabsn 3428* Condition where a restricted class abstraction is a singleton. (Contributed by NM, 28-May-2006.)
(B A → {x Ax = B} = {B})

Theoremrabrsndc 3429* A class abstraction over a decidable proposition restricted to a singleton is either the empty set or the singleton itself. (Contributed by Jim Kingdon, 8-Aug-2018.)
A V    &   DECID φ       (𝑀 = {x {A} ∣ φ} → (𝑀 = ∅ 𝑀 = {A}))

Theoremeuabsn2 3430* Another way to express existential uniqueness of a wff: its class abstraction is a singleton. (Contributed by Mario Carneiro, 14-Nov-2016.)
(∃!xφy{xφ} = {y})

Theoremeuabsn 3431 Another way to express existential uniqueness of a wff: its class abstraction is a singleton. (Contributed by NM, 22-Feb-2004.)
(∃!xφx{xφ} = {x})

Theoremreusn 3432* A way to express restricted existential uniqueness of a wff: its restricted class abstraction is a singleton. (Contributed by NM, 30-May-2006.) (Proof shortened by Mario Carneiro, 14-Nov-2016.)
(∃!x A φy{x Aφ} = {y})

Theoremabsneu 3433 Restricted existential uniqueness determined by a singleton. (Contributed by NM, 29-May-2006.)
((A 𝑉 {xφ} = {A}) → ∃!xφ)

Theoremrabsneu 3434 Restricted existential uniqueness determined by a singleton. (Contributed by NM, 29-May-2006.) (Revised by Mario Carneiro, 23-Dec-2016.)
((A 𝑉 {x Bφ} = {A}) → ∃!x B φ)

Theoremeusn 3435* Two ways to express "A is a singleton." (Contributed by NM, 30-Oct-2010.)
(∃!x x Ax A = {x})

Theoremrabsnt 3436* Truth implied by equality of a restricted class abstraction and a singleton. (Contributed by NM, 29-May-2006.) (Proof shortened by Mario Carneiro, 23-Dec-2016.)
B V    &   (x = B → (φψ))       ({x Aφ} = {B} → ψ)

Theoremprcom 3437 Commutative law for unordered pairs. (Contributed by NM, 5-Aug-1993.)
{A, B} = {B, A}

Theorempreq1 3438 Equality theorem for unordered pairs. (Contributed by NM, 29-Mar-1998.)
(A = B → {A, 𝐶} = {B, 𝐶})

Theorempreq2 3439 Equality theorem for unordered pairs. (Contributed by NM, 5-Aug-1993.)
(A = B → {𝐶, A} = {𝐶, B})

Theorempreq12 3440 Equality theorem for unordered pairs. (Contributed by NM, 19-Oct-2012.)
((A = 𝐶 B = 𝐷) → {A, B} = {𝐶, 𝐷})

Theorempreq1i 3441 Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
A = B       {A, 𝐶} = {B, 𝐶}

Theorempreq2i 3442 Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
A = B       {𝐶, A} = {𝐶, B}

Theorempreq12i 3443 Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
A = B    &   𝐶 = 𝐷       {A, 𝐶} = {B, 𝐷}

Theorempreq1d 3444 Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
(φA = B)       (φ → {A, 𝐶} = {B, 𝐶})

Theorempreq2d 3445 Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
(φA = B)       (φ → {𝐶, A} = {𝐶, B})

Theorempreq12d 3446 Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
(φA = B)    &   (φ𝐶 = 𝐷)       (φ → {A, 𝐶} = {B, 𝐷})

Theoremtpeq1 3447 Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
(A = B → {A, 𝐶, 𝐷} = {B, 𝐶, 𝐷})

Theoremtpeq2 3448 Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
(A = B → {𝐶, A, 𝐷} = {𝐶, B, 𝐷})

Theoremtpeq3 3449 Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
(A = B → {𝐶, 𝐷, A} = {𝐶, 𝐷, B})

Theoremtpeq1d 3450 Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
(φA = B)       (φ → {A, 𝐶, 𝐷} = {B, 𝐶, 𝐷})

Theoremtpeq2d 3451 Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
(φA = B)       (φ → {𝐶, A, 𝐷} = {𝐶, B, 𝐷})

Theoremtpeq3d 3452 Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
(φA = B)       (φ → {𝐶, 𝐷, A} = {𝐶, 𝐷, B})

Theoremtpeq123d 3453 Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
(φA = B)    &   (φ𝐶 = 𝐷)    &   (φ𝐸 = 𝐹)       (φ → {A, 𝐶, 𝐸} = {B, 𝐷, 𝐹})

Theoremtprot 3454 Rotation of the elements of an unordered triple. (Contributed by Alan Sare, 24-Oct-2011.)
{A, B, 𝐶} = {B, 𝐶, A}

Theoremtpcoma 3455 Swap 1st and 2nd members of an undordered triple. (Contributed by NM, 22-May-2015.)
{A, B, 𝐶} = {B, A, 𝐶}

Theoremtpcomb 3456 Swap 2nd and 3rd members of an undordered triple. (Contributed by NM, 22-May-2015.)
{A, B, 𝐶} = {A, 𝐶, B}

Theoremtpass 3457 Split off the first element of an unordered triple. (Contributed by Mario Carneiro, 5-Jan-2016.)
{A, B, 𝐶} = ({A} ∪ {B, 𝐶})

Theoremqdass 3458 Two ways to write an unordered quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.)
({A, B} ∪ {𝐶, 𝐷}) = ({A, B, 𝐶} ∪ {𝐷})

Theoremqdassr 3459 Two ways to write an unordered quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.)
({A, B} ∪ {𝐶, 𝐷}) = ({A} ∪ {B, 𝐶, 𝐷})

Theoremtpidm12 3460 Unordered triple {A, A, B} is just an overlong way to write {A, B}. (Contributed by David A. Wheeler, 10-May-2015.)
{A, A, B} = {A, B}

Theoremtpidm13 3461 Unordered triple {A, B, A} is just an overlong way to write {A, B}. (Contributed by David A. Wheeler, 10-May-2015.)
{A, B, A} = {A, B}

Theoremtpidm23 3462 Unordered triple {A, B, B} is just an overlong way to write {A, B}. (Contributed by David A. Wheeler, 10-May-2015.)
{A, B, B} = {A, B}

Theoremtpidm 3463 Unordered triple {A, A, A} is just an overlong way to write {A}. (Contributed by David A. Wheeler, 10-May-2015.)
{A, A, A} = {A}

Theoremtppreq3 3464 An unordered triple is an unordered pair if one of its elements is identical with another element. (Contributed by Alexander van der Vekens, 6-Oct-2017.)
(B = 𝐶 → {A, B, 𝐶} = {A, B})

Theoremprid1g 3465 An unordered pair contains its first member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by Stefan Allan, 8-Nov-2008.)
(A 𝑉A {A, B})

Theoremprid2g 3466 An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by Stefan Allan, 8-Nov-2008.)
(B 𝑉B {A, B})

Theoremprid1 3467 An unordered pair contains its first member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 5-Aug-1993.)
A V       A {A, B}

Theoremprid2 3468 An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 5-Aug-1993.)
B V       B {A, B}

Theoremprprc1 3469 A proper class vanishes in an unordered pair. (Contributed by NM, 5-Aug-1993.)
A V → {A, B} = {B})

Theoremprprc2 3470 A proper class vanishes in an unordered pair. (Contributed by NM, 22-Mar-2006.)
B V → {A, B} = {A})

Theoremprprc 3471 An unordered pair containing two proper classes is the empty set. (Contributed by NM, 22-Mar-2006.)
((¬ A V ¬ B V) → {A, B} = ∅)

Theoremtpid1 3472 One of the three elements of an unordered triple. (Contributed by NM, 7-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
A V       A {A, B, 𝐶}

Theoremtpid2 3473 One of the three elements of an unordered triple. (Contributed by NM, 7-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
B V       B {A, B, 𝐶}

Theoremtpid3g 3474 Closed theorem form of tpid3 3475. (Contributed by Alan Sare, 24-Oct-2011.)
(A BA {𝐶, 𝐷, A})

Theoremtpid3 3475 One of the three elements of an unordered triple. (Contributed by NM, 7-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
𝐶 V       𝐶 {A, B, 𝐶}

Theoremsnnzg 3476 The singleton of a set is not empty. (Contributed by NM, 14-Dec-2008.)
(A 𝑉 → {A} ≠ ∅)

Theoremsnmg 3477* The singleton of a set is inhabited. (Contributed by Jim Kingdon, 11-Aug-2018.)
(A 𝑉x x {A})

Theoremsnnz 3478 The singleton of a set is not empty. (Contributed by NM, 10-Apr-1994.)
A V       {A} ≠ ∅

Theoremsnm 3479* The singleton of a set is inhabited. (Contributed by Jim Kingdon, 11-Aug-2018.)
A V       x x {A}

Theoremprmg 3480* A pair containing a set is inhabited. (Contributed by Jim Kingdon, 21-Sep-2018.)
(A 𝑉x x {A, B})

Theoremprnz 3481 A pair containing a set is not empty. (Contributed by NM, 9-Apr-1994.)
A V       {A, B} ≠ ∅

Theoremprm 3482* A pair containing a set is inhabited. (Contributed by Jim Kingdon, 21-Sep-2018.)
A V       x x {A, B}

Theoremprnzg 3483 A pair containing a set is not empty. (Contributed by FL, 19-Sep-2011.)
(A 𝑉 → {A, B} ≠ ∅)

Theoremtpnz 3484 A triplet containing a set is not empty. (Contributed by NM, 10-Apr-1994.)
A V       {A, B, 𝐶} ≠ ∅

Theoremsnss 3485 The singleton of an element of a class is a subset of the class. Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 5-Aug-1993.)
A V       (A B ↔ {A} ⊆ B)

Theoremeldifsn 3486 Membership in a set with an element removed. (Contributed by NM, 10-Oct-2007.)
(A (B ∖ {𝐶}) ↔ (A B A𝐶))

Theoremeldifsni 3487 Membership in a set with an element removed. (Contributed by NM, 10-Mar-2015.)
(A (B ∖ {𝐶}) → A𝐶)

Theoremneldifsn 3488 A is not in (B ∖ {A}). (Contributed by David Moews, 1-May-2017.)
¬ A (B ∖ {A})

Theoremneldifsnd 3489 A is not in (B ∖ {A}). Deduction form. (Contributed by David Moews, 1-May-2017.)
(φ → ¬ A (B ∖ {A}))

Theoremrexdifsn 3490 Restricted existential quantification over a set with an element removed. (Contributed by NM, 4-Feb-2015.)
(x (A ∖ {B})φx A (xB φ))

Theoremsnssg 3491 The singleton of an element of a class is a subset of the class. Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 22-Jul-2001.)
(A 𝑉 → (A B ↔ {A} ⊆ B))

Theoremdifsn 3492 An element not in a set can be removed without affecting the set. (Contributed by NM, 16-Mar-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
A B → (B ∖ {A}) = B)

Theoremdifprsnss 3493 Removal of a singleton from an unordered pair. (Contributed by NM, 16-Mar-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
({A, B} ∖ {A}) ⊆ {B}

Theoremdifprsn1 3494 Removal of a singleton from an unordered pair. (Contributed by Thierry Arnoux, 4-Feb-2017.)
(AB → ({A, B} ∖ {A}) = {B})

Theoremdifprsn2 3495 Removal of a singleton from an unordered pair. (Contributed by Alexander van der Vekens, 5-Oct-2017.)
(AB → ({A, B} ∖ {B}) = {A})

Theoremdiftpsn3 3496 Removal of a singleton from an unordered triple. (Contributed by Alexander van der Vekens, 5-Oct-2017.)
((A𝐶 B𝐶) → ({A, B, 𝐶} ∖ {𝐶}) = {A, B})

Theoremdifsnb 3497 (B ∖ {A}) equals B if and only if A is not a member of B. Generalization of difsn 3492. (Contributed by David Moews, 1-May-2017.)
A B ↔ (B ∖ {A}) = B)

Theoremdifsnpssim 3498 (B ∖ {A}) is a proper subclass of B if A is a member of B. In classical logic, the converse holds as well. (Contributed by Jim Kingdon, 9-Aug-2018.)
(A B → (B ∖ {A}) ⊊ B)

Theoremsnssi 3499 The singleton of an element of a class is a subset of the class. (Contributed by NM, 6-Jun-1994.)
(A B → {A} ⊆ B)

Theoremsnssd 3500 The singleton of an element of a class is a subset of the class (deduction rule). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
(φA B)       (φ → {A} ⊆ B)

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-9427
 Copyright terms: Public domain < Previous  Next >