P. 37 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 3601-3700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	prneli 3601	If an element doesn't match the items in an unordered pair, it is not in the unordered pair, using e/. (Contributed by David A. Wheeler, 10-May-2015.)
|- A =/= B   &    |- A =/= C   =>    |- A e/ { B , C }
Theorem	nelprd 3602	If an element doesn't match the items in an unordered pair, it is not in the unordered pair, deduction version. (Contributed by Alexander van der Vekens, 25-Jan-2018.)
|- ( ph -> A =/= B )   &    |- ( ph -> A =/= C )   =>    |- ( ph -> -. A e. { B , C } )
Theorem	eldifpr 3603	Membership in a set with two elements removed. Similar to eldifsn 3703 and eldiftp 3622. (Contributed by Mario Carneiro, 18-Jul-2017.)
|- ( A e. ( B \ { C , D } ) <-> ( A e. B /\ A =/= C /\ A =/= D ) )
Theorem	rexdifpr 3604	Restricted existential quantification over a set with two elements removed. (Contributed by Alexander van der Vekens, 7-Feb-2018.)
|- ( E. x e. ( A \ { B , C } ) ph <-> E. x e. A ( x =/= B /\ x =/= C /\ ph ) )
Theorem	snidg 3605	A set is a member of its singleton. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 28-Oct-2003.)
|- ( A e. V -> A e. { A } )
Theorem	snidb 3606	A class is a set iff it is a member of its singleton. (Contributed by NM, 5-Apr-2004.)
|- ( A e. _V <-> A e. { A } )
Theorem	snid 3607	A set is a member of its singleton. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 31-Dec-1993.)
|- A e. _V   =>    |- A e. { A }
Theorem	vsnid 3608	A setvar variable is a member of its singleton (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- x e. { x }
Theorem	elsn2g 3609	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, 28-Oct-2003.)
|- ( B e. V -> ( A e. { B } <-> A = B ) )
Theorem	elsn2 3610	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 3611	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 3612*	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 3694 and snprc 3641. (Contributed by Jim Kingdon, 30-Aug-2018.)
|- E* x x e. { A }
Theorem	ralsnsg 3613*	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 3614*	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 3615*	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 3616*	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 3617*	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 3618	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 3619*	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 3620*	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 3621	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 3622	Membership in a set with three elements removed. Similar to eldifsn 3703 and eldifpr 3603. (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 3623	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 3624	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 3625*	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 3626	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 3627*	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 3628*	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 3629*	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 3630*	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 3631*	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 3632*	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 3633*	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 3634*	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 3635*	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 3636	Bound-variable hypothesis builder for singletons. (Contributed by NM, 14-Nov-1995.)
|- F/_ x A   =>    |- F/_ x { A }
Theorem	csbsng 3637	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 3638	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 3639	Intersection of distinct singletons is disjoint. (Contributed by NM, 25-May-1998.)
|- ( A =/= B -> ( { A } i^i { B } ) = (/) )
Theorem	disjpr2 3640	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 3641	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 3642*	Special case of r19.12 2572 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 3643*	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	rabrsndc 3644*	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 3645*	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 3646	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 3647*	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 3648	Restricted existential uniqueness determined by a singleton. (Contributed by NM, 29-May-2006.)
|- ( ( A e. V /\ { x | ph } = { A } ) -> E! x ph )
Theorem	rabsneu 3649	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 3650*	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 3651*	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 3652	Commutative law for unordered pairs. (Contributed by NM, 5-Aug-1993.)
|- { A , B } = { B , A }
Theorem	preq1 3653	Equality theorem for unordered pairs. (Contributed by NM, 29-Mar-1998.)
|- ( A = B -> { A , C } = { B , C } )
Theorem	preq2 3654	Equality theorem for unordered pairs. (Contributed by NM, 5-Aug-1993.)
|- ( A = B -> { C , A } = { C , B } )
Theorem	preq12 3655	Equality theorem for unordered pairs. (Contributed by NM, 19-Oct-2012.)
|- ( ( A = C /\ B = D ) -> { A , B } = { C , D } )
Theorem	preq1i 3656	Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
|- A = B   =>    |- { A , C } = { B , C }
Theorem	preq2i 3657	Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
|- A = B   =>    |- { C , A } = { C , B }
Theorem	preq12i 3658	Equality inference for unordered pairs. (Contributed by NM, 19-Oct-2012.)
|- A = B   &    |- C = D   =>    |- { A , C } = { B , D }
Theorem	preq1d 3659	Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
|- ( ph -> A = B )   =>    |- ( ph -> { A , C } = { B , C } )
Theorem	preq2d 3660	Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
|- ( ph -> A = B )   =>    |- ( ph -> { C , A } = { C , B } )
Theorem	preq12d 3661	Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> { A , C } = { B , D } )
Theorem	tpeq1 3662	Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
|- ( A = B -> { A , C , D } = { B , C , D } )
Theorem	tpeq2 3663	Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
|- ( A = B -> { C , A , D } = { C , B , D } )
Theorem	tpeq3 3664	Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011.)
|- ( A = B -> { C , D , A } = { C , D , B } )
Theorem	tpeq1d 3665	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
|- ( ph -> A = B )   =>    |- ( ph -> { A , C , D } = { B , C , D } )
Theorem	tpeq2d 3666	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
|- ( ph -> A = B )   =>    |- ( ph -> { C , A , D } = { C , B , D } )
Theorem	tpeq3d 3667	Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014.)
|- ( ph -> A = B )   =>    |- ( ph -> { C , D , A } = { C , D , B } )
Theorem	tpeq123d 3668	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 3669	Rotation of the elements of an unordered triple. (Contributed by Alan Sare, 24-Oct-2011.)
|- { A , B , C } = { B , C , A }
Theorem	tpcoma 3670	Swap 1st and 2nd members of an undordered triple. (Contributed by NM, 22-May-2015.)
|- { A , B , C } = { B , A , C }
Theorem	tpcomb 3671	Swap 2nd and 3rd members of an undordered triple. (Contributed by NM, 22-May-2015.)
|- { A , B , C } = { A , C , B }
Theorem	tpass 3672	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 3673	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 3674	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 3675	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 3676	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 3677	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 3678	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 3679	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 3680	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 3681	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 3682	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 3683	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	prprc1 3684	A proper class vanishes in an unordered pair. (Contributed by NM, 5-Aug-1993.)
|- ( -. A e. _V -> { A , B } = { B } )
Theorem	prprc2 3685	A proper class vanishes in an unordered pair. (Contributed by NM, 22-Mar-2006.)
|- ( -. B e. _V -> { A , B } = { A } )
Theorem	prprc 3686	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 3687	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 3688	Closed theorem form of tpid1 3687. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( A e. B -> A e. { A , C , D } )
Theorem	tpid2 3689	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 3690	Closed theorem form of tpid2 3689. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( A e. B -> A e. { C , A , D } )
Theorem	tpid3g 3691	Closed theorem form of tpid3 3692. (Contributed by Alan Sare, 24-Oct-2011.)
|- ( A e. B -> A e. { C , D , A } )
Theorem	tpid3 3692	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 3693	The singleton of a set is not empty. (Contributed by NM, 14-Dec-2008.)
|- ( A e. V -> { A } =/= (/) )
Theorem	snmg 3694*	The singleton of a set is inhabited. (Contributed by Jim Kingdon, 11-Aug-2018.)
|- ( A e. V -> E. x x e. { A } )
Theorem	snnz 3695	The singleton of a set is not empty. (Contributed by NM, 10-Apr-1994.)
|- A e. _V   =>    |- { A } =/= (/)
Theorem	snm 3696*	The singleton of a set is inhabited. (Contributed by Jim Kingdon, 11-Aug-2018.)
|- A e. _V   =>    |- E. x x e. { A }
Theorem	prmg 3697*	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 3698	A pair containing a set is not empty. (Contributed by NM, 9-Apr-1994.)
|- A e. _V   =>    |- { A , B } =/= (/)
Theorem	prm 3699*	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 3700	A pair containing a set is not empty. (Contributed by FL, 19-Sep-2011.)
|- ( A e. V -> { A , B } =/= (/) )