P. 38 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 3701-3800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	elsn2 3701	There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. This variation requires only that B, rather than A, be a set. (Contributed by NM, 12-Jun-1994.)
|- B e. _V   =>    |- ( A e. { B } <-> A = B )
Theorem	nelsn 3702	If a class is not equal to the class in a singleton, then it is not in the singleton. (Contributed by Glauco Siliprandi, 17-Aug-2020.) (Proof shortened by BJ, 4-May-2021.)
|- ( A =/= B -> -. A e. { B } )
Theorem	mosn 3703*	A singleton has at most one element. This works whether A is a proper class or not, and in that sense can be seen as encompassing both snmg 3788 and snprc 3732. (Contributed by Jim Kingdon, 30-Aug-2018.)
|- E* x x e. { A }
Theorem	ralsnsg 3704*	Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.)
|- ( A e. V -> ( A. x e. { A } ph <-> [. A / x ]. ph ) )
Theorem	ralsns 3705*	Substitution expressed in terms of quantification over a singleton. (Contributed by Mario Carneiro, 23-Apr-2015.)
|- ( A e. V -> ( A. x e. { A } ph <-> [. A / x ]. ph ) )
Theorem	rexsns 3706*	Restricted existential quantification over a singleton. (Contributed by Mario Carneiro, 23-Apr-2015.) (Revised by NM, 22-Aug-2018.)
|- ( E. x e. { A } ph <-> [. A / x ]. ph )
Theorem	ralsng 3707*	Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.)
|- ( x = A -> ( ph <-> ps ) )   =>    |- ( A e. V -> ( A. x e. { A } ph <-> ps ) )
Theorem	rexsng 3708*	Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012.)
|- ( x = A -> ( ph <-> ps ) )   =>    |- ( A e. V -> ( E. x e. { A } ph <-> ps ) )
Theorem	exsnrex 3709	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.)
|- ( E. x M = { x } <-> E. x e. M M = { x } )
Theorem	ralsn 3710*	Convert a quantification over a singleton to a substitution. (Contributed by NM, 27-Apr-2009.)
|- A e. _V   &    |- ( x = A -> ( ph <-> ps ) )   =>    |- ( A. x e. { A } ph <-> ps )
Theorem	rexsn 3711*	Restricted existential quantification over a singleton. (Contributed by Jeff Madsen, 5-Jan-2011.)
|- A e. _V   &    |- ( x = A -> ( ph <-> ps ) )   =>    |- ( E. x e. { A } ph <-> ps )
Theorem	eltpg 3712	Members of an unordered triple of classes. (Contributed by FL, 2-Feb-2014.) (Proof shortened by Mario Carneiro, 11-Feb-2015.)
|- ( A e. V -> ( A e. { B , C , D } <-> ( A = B \/ A = C \/ A = D ) ) )
Theorem	eldiftp 3713	Membership in a set with three elements removed. Similar to eldifsn 3798 and eldifpr 3694. (Contributed by David A. Wheeler, 22-Jul-2017.)
|- ( A e. ( B \ { C , D , E } ) <-> ( A e. B /\ ( A =/= C /\ A =/= D /\ A =/= E ) ) )
Theorem	eltpi 3714	A member of an unordered triple of classes is one of them. (Contributed by Mario Carneiro, 11-Feb-2015.)
|- ( A e. { B , C , D } -> ( A = B \/ A = C \/ A = D ) )
Theorem	eltp 3715	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 e. _V   =>    |- ( A e. { B , C , D } <-> ( A = B \/ A = C \/ A = D ) )
Theorem	dftp2 3716*	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 , C } = { x | ( x = A \/ x = B \/ x = C ) }
Theorem	nfpr 3717	Bound-variable hypothesis builder for unordered pairs. (Contributed by NM, 14-Nov-1995.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/_ x { A , B }
Theorem	ralprg 3718*	Convert a quantification over a pair to a conjunction. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
|- ( x = A -> ( ph <-> ps ) )   &    |- ( x = B -> ( ph <-> ch ) )   =>    |- ( ( A e. V /\ B e. W ) -> ( A. x e. { A , B } ph <-> ( ps /\ ch ) ) )
Theorem	rexprg 3719*	Convert a quantification over a pair to a disjunction. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
|- ( x = A -> ( ph <-> ps ) )   &    |- ( x = B -> ( ph <-> ch ) )   =>    |- ( ( A e. V /\ B e. W ) -> ( E. x e. { A , B } ph <-> ( ps \/ ch ) ) )
Theorem	raltpg 3720*	Convert a quantification over a triple to a conjunction. (Contributed by NM, 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
|- ( x = A -> ( ph <-> ps ) )   &    |- ( x = B -> ( ph <-> ch ) )   &    |- ( x = C -> ( ph <-> th ) )   =>    |- ( ( A e. V /\ B e. W /\ C e. X ) -> ( A. x e. { A , B , C } ph <-> ( ps /\ ch /\ th ) ) )
Theorem	rextpg 3721*	Convert a quantification over a triple to a disjunction. (Contributed by Mario Carneiro, 23-Apr-2015.)
|- ( x = A -> ( ph <-> ps ) )   &    |- ( x = B -> ( ph <-> ch ) )   &    |- ( x = C -> ( ph <-> th ) )   =>    |- ( ( A e. V /\ B e. W /\ C e. X ) -> ( E. x e. { A , B , C } ph <-> ( ps \/ ch \/ th ) ) )
Theorem	ralpr 3722*	Convert a quantification over a pair to a conjunction. (Contributed by NM, 3-Jun-2007.) (Revised by Mario Carneiro, 23-Apr-2015.)
|- A e. _V   &    |- B e. _V   &    |- ( x = A -> ( ph <-> ps ) )   &    |- ( x = B -> ( ph <-> ch ) )   =>    |- ( A. x e. { A , B } ph <-> ( ps /\ ch ) )
Theorem	rexpr 3723*	Convert an existential quantification over a pair to a disjunction. (Contributed by NM, 3-Jun-2007.) (Revised by Mario Carneiro, 23-Apr-2015.)
|- A e. _V   &    |- B e. _V   &    |- ( x = A -> ( ph <-> ps ) )   &    |- ( x = B -> ( ph <-> ch ) )   =>    |- ( E. x e. { A , B } ph <-> ( ps \/ ch ) )
Theorem	raltp 3724*	Convert a quantification over a triple to a conjunction. (Contributed by NM, 13-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   &    |- ( x = A -> ( ph <-> ps ) )   &    |- ( x = B -> ( ph <-> ch ) )   &    |- ( x = C -> ( ph <-> th ) )   =>    |- ( A. x e. { A , B , C } ph <-> ( ps /\ ch /\ th ) )
Theorem	rextp 3725*	Convert a quantification over a triple to a disjunction. (Contributed by Mario Carneiro, 23-Apr-2015.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   &    |- ( x = A -> ( ph <-> ps ) )   &    |- ( x = B -> ( ph <-> ch ) )   &    |- ( x = C -> ( ph <-> th ) )   =>    |- ( E. x e. { A , B , C } ph <-> ( ps \/ ch \/ th ) )
Theorem	sbcsng 3726*	Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.)
|- ( A e. V -> ( [. A / x ]. ph <-> A. x e. { A } ph ) )
Theorem	nfsn 3727	Bound-variable hypothesis builder for singletons. (Contributed by NM, 14-Nov-1995.)
|- F/_ x A   =>    |- F/_ x { A }
Theorem	csbsng 3728	Distribute proper substitution through the singleton of a class. (Contributed by Alan Sare, 10-Nov-2012.)
|- ( A e. V -> [_ A / x ]_ { B } = { [_ A / x ]_ B } )
Theorem	disjsn 3729	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 i^i { B } ) = (/) <-> -. B e. A )
Theorem	disjsn2 3730	Intersection of distinct singletons is disjoint. (Contributed by NM, 25-May-1998.)
|- ( A =/= B -> ( { A } i^i { B } ) = (/) )
Theorem	disjpr2 3731	The intersection of distinct unordered pairs is disjoint. (Contributed by Alexander van der Vekens, 11-Nov-2017.)
|- ( ( ( A =/= C /\ B =/= C ) /\ ( A =/= D /\ B =/= D ) ) -> ( { A , B } i^i { C , D } ) = (/) )
Theorem	snprc 3732	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 e. _V <-> { A } = (/) )
Theorem	r19.12sn 3733*	Special case of r19.12 2637 where its converse holds. (Contributed by NM, 19-May-2008.) (Revised by Mario Carneiro, 23-Apr-2015.) (Revised by BJ, 20-Dec-2021.)
|- ( A e. V -> ( E. x e. { A } A. y e. B ph <-> A. y e. B E. x e. { A } ph ) )
Theorem	rabsn 3734*	Condition where a restricted class abstraction is a singleton. (Contributed by NM, 28-May-2006.)
|- ( B e. A -> { x e. A | x = B } = { B } )
Theorem	rabsnifsb 3735*	A restricted class abstraction restricted to a singleton is either the empty set or the singleton itself. (Contributed by AV, 21-Jul-2019.)
|- { x e. { A } | ph } = if ( [. A / x ]. ph , { A } , (/) )
Theorem	rabsnif 3736*	A restricted class abstraction restricted to a singleton is either the empty set or the singleton itself. (Contributed by AV, 12-Apr-2019.) (Proof shortened by AV, 21-Jul-2019.)
|- ( x = A -> ( ph <-> ps ) )   =>    |- { x e. { A } | ph } = if ( ps , { A } , (/) )
Theorem	rabrsndc 3737*	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 e. _V   &    |- DECID ph   =>    |- ( M = { x e. { A } | ph } -> ( M = (/) \/ M = { A } ) )
Theorem	euabsn2 3738*	Another way to express existential uniqueness of a wff: its class abstraction is a singleton. (Contributed by Mario Carneiro, 14-Nov-2016.)
|- ( E! x ph <-> E. y { x | ph } = { y } )
Theorem	euabsn 3739	Another way to express existential uniqueness of a wff: its class abstraction is a singleton. (Contributed by NM, 22-Feb-2004.)
|- ( E! x ph <-> E. x { x | ph } = { x } )
Theorem	reusn 3740*	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.)
|- ( E! x e. A ph <-> E. y { x e. A | ph } = { y } )
Theorem	absneu 3741	Restricted existential uniqueness determined by a singleton. (Contributed by NM, 29-May-2006.)
|- ( ( A e. V /\ { x | ph } = { A } ) -> E! x ph )
Theorem	rabsneu 3742	Restricted existential uniqueness determined by a singleton. (Contributed by NM, 29-May-2006.) (Revised by Mario Carneiro, 23-Dec-2016.)
|- ( ( A e. V /\ { x e. B | ph } = { A } ) -> E! x e. B ph )
Theorem	eusn 3743*	Two ways to express " A is a singleton". (Contributed by NM, 30-Oct-2010.)
|- ( E! x x e. A <-> E. x A = { x } )
Theorem	rabsnt 3744*	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 e. _V   &    |- ( x = B -> ( ph <-> ps ) )   =>    |- ( { x e. A | ph } = { B } -> ps )
Theorem	prcom 3745	Commutative law for unordered pairs. (Contributed by NM, 5-Aug-1993.)
|- { A , B } = { B , A }
Theorem	preq1 3746	Equality theorem for unordered pairs. (Contributed by NM, 29-Mar-1998.)
|- ( A = B -> { A , C } = { B , C } )
Theorem	preq2 3747	Equality theorem for unordered pairs. (Contributed by NM, 5-Aug-1993.)
|- ( A = B -> { C , A } = { C , B } )
Theorem	preq12 3748	Equality theorem for unordered pairs. (Contributed by NM, 19-Oct-2012.)
|- ( ( A = C /\ B = D ) -> { A , B } = { C , D } )
Theorem	preq1i 3749	Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
|- A = B   =>    |- { A , C } = { B , C }
Theorem	preq2i 3750	Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
|- A = B   =>    |- { C , A } = { C , B }
Theorem	preq12i 3751	Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
|- A = B   &    |- C = D   =>    |- { A , C } = { B , D }
Theorem	preq1d 3752	Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
|- ( ph -> A = B )   =>    |- ( ph -> { A , C } = { B , C } )
Theorem	preq2d 3753	Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
|- ( ph -> A = B )   =>    |- ( ph -> { C , A } = { C , B } )
Theorem	preq12d 3754	Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> { A , C } = { B , D } )
Theorem	tpeq1 3755	Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
|- ( A = B -> { A , C , D } = { B , C , D } )
Theorem	tpeq2 3756	Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
|- ( A = B -> { C , A , D } = { C , B , D } )
Theorem	tpeq3 3757	Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
|- ( A = B -> { C , D , A } = { C , D , B } )
Theorem	tpeq1d 3758	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
|- ( ph -> A = B )   =>    |- ( ph -> { A , C , D } = { B , C , D } )
Theorem	tpeq2d 3759	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
|- ( ph -> A = B )   =>    |- ( ph -> { C , A , D } = { C , B , D } )
Theorem	tpeq3d 3760	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
|- ( ph -> A = B )   =>    |- ( ph -> { C , D , A } = { C , D , B } )
Theorem	tpeq123d 3761	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   &    |- ( ph -> E = F )   =>    |- ( ph -> { A , C , E } = { B , D , F } )
Theorem	tprot 3762	Rotation of the elements of an unordered triple. (Contributed by Alan Sare, 24-Oct-2011.)
|- { A , B , C } = { B , C , A }
Theorem	tpcoma 3763	Swap 1st and 2nd members of an undordered triple. (Contributed by NM, 22-May-2015.)
|- { A , B , C } = { B , A , C }
Theorem	tpcomb 3764	Swap 2nd and 3rd members of an undordered triple. (Contributed by NM, 22-May-2015.)
|- { A , B , C } = { A , C , B }
Theorem	tpass 3765	Split off the first element of an unordered triple. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- { A , B , C } = ( { A } u. { B , C } )
Theorem	qdass 3766	Two ways to write an unordered quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- ( { A , B } u. { C , D } ) = ( { A , B , C } u. { D } )
Theorem	qdassr 3767	Two ways to write an unordered quadruple. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- ( { A , B } u. { C , D } ) = ( { A } u. { B , C , D } )
Theorem	tpidm12 3768	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 }
Theorem	tpidm13 3769	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 }
Theorem	tpidm23 3770	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 }
Theorem	tpidm 3771	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 }
Theorem	tppreq3 3772	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 = C -> { A , B , C } = { A , B } )
Theorem	prid1g 3773	An unordered pair contains its first member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by Stefan Allan, 8-Nov-2008.)
|- ( A e. V -> A e. { A , B } )
Theorem	prid2g 3774	An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by Stefan Allan, 8-Nov-2008.)
|- ( B e. V -> B e. { A , B } )
Theorem	prid1 3775	An unordered pair contains its first member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 5-Aug-1993.)
|- A e. _V   =>    |- A e. { A , B }
Theorem	prid2 3776	An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 5-Aug-1993.)
|- B e. _V   =>    |- B e. { A , B }
Theorem	ifpprsnssdc 3777	An unordered pair is a singleton or a subset of itself. This theorem is helpful to convert theorems about walks in arbitrary graphs into theorems about walks in pseudographs. (Contributed by AV, 27-Feb-2021.)
|- ( ( P = { A , B } /\ DECID A = B ) -> if- ( A = B , P = { A } , { A , B } C_ P ) )
Theorem	prprc1 3778	A proper class vanishes in an unordered pair. (Contributed by NM, 5-Aug-1993.)
|- ( -. A e. _V -> { A , B } = { B } )
Theorem	prprc2 3779	A proper class vanishes in an unordered pair. (Contributed by NM, 22-Mar-2006.)
|- ( -. B e. _V -> { A , B } = { A } )
Theorem	prprc 3780	An unordered pair containing two proper classes is the empty set. (Contributed by NM, 22-Mar-2006.)
|- ( ( -. A e. _V /\ -. B e. _V ) -> { A , B } = (/) )
Theorem	tpid1 3781	One of the three elements of an unordered triple. (Contributed by NM, 7-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|- A e. _V   =>    |- A e. { A , B , C }
Theorem	tpid1g 3782	Closed theorem form of tpid1 3781. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( A e. B -> A e. { A , C , D } )
Theorem	tpid2 3783	One of the three elements of an unordered triple. (Contributed by NM, 7-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|- B e. _V   =>    |- B e. { A , B , C }
Theorem	tpid2g 3784	Closed theorem form of tpid2 3783. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( A e. B -> A e. { C , A , D } )
Theorem	tpid3g 3785	Closed theorem form of tpid3 3786. (Contributed by Alan Sare, 24-Oct-2011.)
|- ( A e. B -> A e. { C , D , A } )
Theorem	tpid3 3786	One of the three elements of an unordered triple. (Contributed by NM, 7-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|- C e. _V   =>    |- C e. { A , B , C }
Theorem	snnzg 3787	The singleton of a set is not empty. It is also inhabited as shown at snmg 3788. (Contributed by NM, 14-Dec-2008.)
|- ( A e. V -> { A } =/= (/) )
Theorem	snmg 3788*	The singleton of a set is inhabited. (Contributed by Jim Kingdon, 11-Aug-2018.)
|- ( A e. V -> E. x x e. { A } )
Theorem	snnz 3789	The singleton of a set is not empty. It is also inhabited as shown at snm 3790. (Contributed by NM, 10-Apr-1994.)
|- A e. _V   =>    |- { A } =/= (/)
Theorem	snm 3790*	The singleton of a set is inhabited. (Contributed by Jim Kingdon, 11-Aug-2018.)
|- A e. _V   =>    |- E. x x e. { A }
Theorem	snmb 3791*	A singleton is inhabited iff its argument is a set. (Contributed by Scott Fenton, 8-May-2018.) (Revised by Jim Kingdon, 29-Dec-2025.)
|- ( A e. _V <-> E. x x e. { A } )
Theorem	prmg 3792*	A pair containing a set is inhabited. (Contributed by Jim Kingdon, 21-Sep-2018.)
|- ( A e. V -> E. x x e. { A , B } )
Theorem	prnz 3793	A pair containing a set is not empty. It is also inhabited (see prm 3794). (Contributed by NM, 9-Apr-1994.)
|- A e. _V   =>    |- { A , B } =/= (/)
Theorem	prm 3794*	A pair containing a set is inhabited. (Contributed by Jim Kingdon, 21-Sep-2018.)
|- A e. _V   =>    |- E. x x e. { A , B }
Theorem	prnzg 3795	A pair containing a set is not empty. It is also inhabited (see prmg 3792). (Contributed by FL, 19-Sep-2011.)
|- ( A e. V -> { A , B } =/= (/) )
Theorem	tpnz 3796	A triplet containing a set is not empty. (Contributed by NM, 10-Apr-1994.)
|- A e. _V   =>    |- { A , B , C } =/= (/)
Theorem	snssOLD 3797	Obsolete version of snss 3806 as of 1-Jan-2025. (Contributed by NM, 5-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
|- A e. _V   =>    |- ( A e. B <-> { A } C_ B )
Theorem	eldifsn 3798	Membership in a set with an element removed. (Contributed by NM, 10-Oct-2007.)
|- ( A e. ( B \ { C } ) <-> ( A e. B /\ A =/= C ) )
Theorem	ssdifsn 3799	Subset of a set with an element removed. (Contributed by Emmett Weisz, 7-Jul-2021.) (Proof shortened by JJ, 31-May-2022.)
|- ( A C_ ( B \ { C } ) <-> ( A C_ B /\ -. C e. A ) )
Theorem	eldifsni 3800	Membership in a set with an element removed. (Contributed by NM, 10-Mar-2015.)
|- ( A e. ( B \ { C } ) -> A =/= C )