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	prprc2 3701	A proper class vanishes in an unordered pair. (Contributed by NM, 22-Mar-2006.)
|- ( -. B e. _V -> { A , B } = { A } )
Theorem	prprc 3702	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 3703	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 3704	Closed theorem form of tpid1 3703. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( A e. B -> A e. { A , C , D } )
Theorem	tpid2 3705	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 3706	Closed theorem form of tpid2 3705. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( A e. B -> A e. { C , A , D } )
Theorem	tpid3g 3707	Closed theorem form of tpid3 3708. (Contributed by Alan Sare, 24-Oct-2011.)
|- ( A e. B -> A e. { C , D , A } )
Theorem	tpid3 3708	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 3709	The singleton of a set is not empty. (Contributed by NM, 14-Dec-2008.)
|- ( A e. V -> { A } =/= (/) )
Theorem	snmg 3710*	The singleton of a set is inhabited. (Contributed by Jim Kingdon, 11-Aug-2018.)
|- ( A e. V -> E. x x e. { A } )
Theorem	snnz 3711	The singleton of a set is not empty. (Contributed by NM, 10-Apr-1994.)
|- A e. _V   =>    |- { A } =/= (/)
Theorem	snm 3712*	The singleton of a set is inhabited. (Contributed by Jim Kingdon, 11-Aug-2018.)
|- A e. _V   =>    |- E. x x e. { A }
Theorem	prmg 3713*	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 3714	A pair containing a set is not empty. (Contributed by NM, 9-Apr-1994.)
|- A e. _V   =>    |- { A , B } =/= (/)
Theorem	prm 3715*	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 3716	A pair containing a set is not empty. (Contributed by FL, 19-Sep-2011.)
|- ( A e. V -> { A , B } =/= (/) )
Theorem	tpnz 3717	A triplet containing a set is not empty. (Contributed by NM, 10-Apr-1994.)
|- A e. _V   =>    |- { A , B , C } =/= (/)
Theorem	snssOLD 3718	Obsolete version of snss 3727 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 3719	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 3720	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 3721	Membership in a set with an element removed. (Contributed by NM, 10-Mar-2015.)
|- ( A e. ( B \ { C } ) -> A =/= C )
Theorem	neldifsn 3722	A is not in ( B \ { A } ). (Contributed by David Moews, 1-May-2017.)
|- -. A e. ( B \ { A } )
Theorem	neldifsnd 3723	A is not in ( B \ { A } ). Deduction form. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> -. A e. ( B \ { A } ) )
Theorem	rexdifsn 3724	Restricted existential quantification over a set with an element removed. (Contributed by NM, 4-Feb-2015.)
|- ( E. x e. ( A \ { B } ) ph <-> E. x e. A ( x =/= B /\ ph ) )
Theorem	snssb 3725	Characterization of the inclusion of a singleton in a class. (Contributed by BJ, 1-Jan-2025.)
|- ( { A } C_ B <-> ( A e. _V -> A e. B ) )
Theorem	snssg 3726	The singleton formed on a set is included in a class if and only if the set is an element of that class. Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 22-Jul-2001.) (Proof shortened by BJ, 1-Jan-2025.)
|- ( A e. V -> ( A e. B <-> { A } C_ B ) )
Theorem	snss 3727	The singleton of an element of a class is a subset of the class (inference form of snssg 3726). Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 21-Jun-1993.) (Proof shortened by BJ, 1-Jan-2025.)
|- A e. _V   =>    |- ( A e. B <-> { A } C_ B )
Theorem	snssgOLD 3728	Obsolete version of snssgOLD 3728 as of 1-Jan-2025. (Contributed by NM, 22-Jul-2001.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A e. V -> ( A e. B <-> { A } C_ B ) )
Theorem	difsn 3729	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 e. B -> ( B \ { A } ) = B )
Theorem	difprsnss 3730	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 } ) C_ { B }
Theorem	difprsn1 3731	Removal of a singleton from an unordered pair. (Contributed by Thierry Arnoux, 4-Feb-2017.)
|- ( A =/= B -> ( { A , B } \ { A } ) = { B } )
Theorem	difprsn2 3732	Removal of a singleton from an unordered pair. (Contributed by Alexander van der Vekens, 5-Oct-2017.)
|- ( A =/= B -> ( { A , B } \ { B } ) = { A } )
Theorem	diftpsn3 3733	Removal of a singleton from an unordered triple. (Contributed by Alexander van der Vekens, 5-Oct-2017.)
|- ( ( A =/= C /\ B =/= C ) -> ( { A , B , C } \ { C } ) = { A , B } )
Theorem	difpr 3734	Removing two elements as pair of elements corresponds to removing each of the two elements as singletons. (Contributed by Alexander van der Vekens, 13-Jul-2018.)
|- ( A \ { B , C } ) = ( ( A \ { B } ) \ { C } )
Theorem	difsnb 3735	( B \ { A } ) equals B if and only if A is not a member of B. Generalization of difsn 3729. (Contributed by David Moews, 1-May-2017.)
|- ( -. A e. B <-> ( B \ { A } ) = B )
Theorem	snssi 3736	The singleton of an element of a class is a subset of the class. (Contributed by NM, 6-Jun-1994.)
|- ( A e. B -> { A } C_ B )
Theorem	snssd 3737	The singleton of an element of a class is a subset of the class (deduction form). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ph -> A e. B )   =>    |- ( ph -> { A } C_ B )
Theorem	difsnss 3738	If we remove a single element from a class then put it back in, we end up with a subset of the original class. If equality is decidable, we can replace subset with equality as seen in nndifsnid 6503. (Contributed by Jim Kingdon, 10-Aug-2018.)
|- ( B e. A -> ( ( A \ { B } ) u. { B } ) C_ A )
Theorem	pw0 3739	Compute the power set of the empty set. Theorem 89 of [Suppes] p. 47. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|- ~P (/) = { (/) }
Theorem	snsspr1 3740	A singleton is a subset of an unordered pair containing its member. (Contributed by NM, 27-Aug-2004.)
|- { A } C_ { A , B }
Theorem	snsspr2 3741	A singleton is a subset of an unordered pair containing its member. (Contributed by NM, 2-May-2009.)
|- { B } C_ { A , B }
Theorem	snsstp1 3742	A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.)
|- { A } C_ { A , B , C }
Theorem	snsstp2 3743	A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.)
|- { B } C_ { A , B , C }
Theorem	snsstp3 3744	A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.)
|- { C } C_ { A , B , C }
Theorem	prsstp12 3745	A pair is a subset of an unordered triple containing its members. (Contributed by Jim Kingdon, 11-Aug-2018.)
|- { A , B } C_ { A , B , C }
Theorem	prsstp13 3746	A pair is a subset of an unordered triple containing its members. (Contributed by Jim Kingdon, 11-Aug-2018.)
|- { A , C } C_ { A , B , C }
Theorem	prsstp23 3747	A pair is a subset of an unordered triple containing its members. (Contributed by Jim Kingdon, 11-Aug-2018.)
|- { B , C } C_ { A , B , C }
Theorem	prss 3748	A pair of elements of a class is a subset of the class. Theorem 7.5 of [Quine] p. 49. (Contributed by NM, 30-May-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|- A e. _V   &    |- B e. _V   =>    |- ( ( A e. C /\ B e. C ) <-> { A , B } C_ C )
Theorem	prssg 3749	A pair of elements of a class is a subset of the class. Theorem 7.5 of [Quine] p. 49. (Contributed by NM, 22-Mar-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|- ( ( A e. V /\ B e. W ) -> ( ( A e. C /\ B e. C ) <-> { A , B } C_ C ) )
Theorem	prssi 3750	A pair of elements of a class is a subset of the class. (Contributed by NM, 16-Jan-2015.)
|- ( ( A e. C /\ B e. C ) -> { A , B } C_ C )
Theorem	prsspwg 3751	An unordered pair belongs to the power class of a class iff each member belongs to the class. (Contributed by Thierry Arnoux, 3-Oct-2016.) (Revised by NM, 18-Jan-2018.)
|- ( ( A e. V /\ B e. W ) -> ( { A , B } C_ ~P C <-> ( A C_ C /\ B C_ C ) ) )
Theorem	sssnr 3752	Empty set and the singleton itself are subsets of a singleton. Concerning the converse, see exmidsssn 4200. (Contributed by Jim Kingdon, 10-Aug-2018.)
|- ( ( A = (/) \/ A = { B } ) -> A C_ { B } )
Theorem	sssnm 3753*	The inhabited subset of a singleton. (Contributed by Jim Kingdon, 10-Aug-2018.)
|- ( E. x x e. A -> ( A C_ { B } <-> A = { B } ) )
Theorem	eqsnm 3754*	Two ways to express that an inhabited set equals a singleton. (Contributed by Jim Kingdon, 11-Aug-2018.)
|- ( E. x x e. A -> ( A = { B } <-> A. x e. A x = B ) )
Theorem	ssprr 3755	The subsets of a pair. (Contributed by Jim Kingdon, 11-Aug-2018.)
|- ( ( ( A = (/) \/ A = { B } ) \/ ( A = { C } \/ A = { B , C } ) ) -> A C_ { B , C } )
Theorem	sstpr 3756	The subsets of a triple. (Contributed by Jim Kingdon, 11-Aug-2018.)
|- ( ( ( ( A = (/) \/ A = { B } ) \/ ( A = { C } \/ A = { B , C } ) ) \/ ( ( A = { D } \/ A = { B , D } ) \/ ( A = { C , D } \/ A = { B , C , D } ) ) ) -> A C_ { B , C , D } )
Theorem	tpss 3757	A triplet of elements of a class is a subset of the class. (Contributed by NM, 9-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   =>    |- ( ( A e. D /\ B e. D /\ C e. D ) <-> { A , B , C } C_ D )
Theorem	tpssi 3758	A triple of elements of a class is a subset of the class. (Contributed by Alexander van der Vekens, 1-Feb-2018.)
|- ( ( A e. D /\ B e. D /\ C e. D ) -> { A , B , C } C_ D )
Theorem	sneqr 3759	If the singletons of two sets are equal, the two sets are equal. Part of Exercise 4 of [TakeutiZaring] p. 15. (Contributed by NM, 27-Aug-1993.)
|- A e. _V   =>    |- ( { A } = { B } -> A = B )
Theorem	snsssn 3760	If a singleton is a subset of another, their members are equal. (Contributed by NM, 28-May-2006.)
|- A e. _V   =>    |- ( { A } C_ { B } -> A = B )
Theorem	sneqrg 3761	Closed form of sneqr 3759. (Contributed by Scott Fenton, 1-Apr-2011.)
|- ( A e. V -> ( { A } = { B } -> A = B ) )
Theorem	sneqbg 3762	Two singletons of sets are equal iff their elements are equal. (Contributed by Scott Fenton, 16-Apr-2012.)
|- ( A e. V -> ( { A } = { B } <-> A = B ) )
Theorem	snsspw 3763	The singleton of a class is a subset of its power class. (Contributed by NM, 5-Aug-1993.)
|- { A } C_ ~P A
Theorem	prsspw 3764	An unordered pair belongs to the power class of a class iff each member belongs to the class. (Contributed by NM, 10-Dec-2003.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- A e. _V   &    |- B e. _V   =>    |- ( { A , B } C_ ~P C <-> ( A C_ C /\ B C_ C ) )
Theorem	preqr1g 3765	Reverse equality lemma for unordered pairs. If two unordered pairs have the same second element, the first elements are equal. Closed form of preqr1 3767. (Contributed by Jim Kingdon, 21-Sep-2018.)
|- ( ( A e. _V /\ B e. _V ) -> ( { A , C } = { B , C } -> A = B ) )
Theorem	preqr2g 3766	Reverse equality lemma for unordered pairs. If two unordered pairs have the same second element, the second elements are equal. Closed form of preqr2 3768. (Contributed by Jim Kingdon, 21-Sep-2018.)
|- ( ( A e. _V /\ B e. _V ) -> ( { C , A } = { C , B } -> A = B ) )
Theorem	preqr1 3767	Reverse equality lemma for unordered pairs. If two unordered pairs have the same second element, the first elements are equal. (Contributed by NM, 18-Oct-1995.)
|- A e. _V   &    |- B e. _V   =>    |- ( { A , C } = { B , C } -> A = B )
Theorem	preqr2 3768	Reverse equality lemma for unordered pairs. If two unordered pairs have the same first element, the second elements are equal. (Contributed by NM, 5-Aug-1993.)
|- A e. _V   &    |- B e. _V   =>    |- ( { C , A } = { C , B } -> A = B )
Theorem	preq12b 3769	Equality relationship for two unordered pairs. (Contributed by NM, 17-Oct-1996.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   &    |- D e. _V   =>    |- ( { A , B } = { C , D } <-> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) )
Theorem	prel12 3770	Equality of two unordered pairs. (Contributed by NM, 17-Oct-1996.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   &    |- D e. _V   =>    |- ( -. A = B -> ( { A , B } = { C , D } <-> ( A e. { C , D } /\ B e. { C , D } ) ) )
Theorem	opthpr 3771	A way to represent ordered pairs using unordered pairs with distinct members. (Contributed by NM, 27-Mar-2007.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   &    |- D e. _V   =>    |- ( A =/= D -> ( { A , B } = { C , D } <-> ( A = C /\ B = D ) ) )
Theorem	preq12bg 3772	Closed form of preq12b 3769. (Contributed by Scott Fenton, 28-Mar-2014.)
|- ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) -> ( { A , B } = { C , D } <-> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) )
Theorem	prneimg 3773	Two pairs are not equal if at least one element of the first pair is not contained in the second pair. (Contributed by Alexander van der Vekens, 13-Aug-2017.)
|- ( ( ( A e. U /\ B e. V ) /\ ( C e. X /\ D e. Y ) ) -> ( ( ( A =/= C /\ A =/= D ) \/ ( B =/= C /\ B =/= D ) ) -> { A , B } =/= { C , D } ) )
Theorem	preqsn 3774	Equivalence for a pair equal to a singleton. (Contributed by NM, 3-Jun-2008.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   =>    |- ( { A , B } = { C } <-> ( A = B /\ B = C ) )
Theorem	dfopg 3775	Value of the ordered pair when the arguments are sets. (Contributed by Mario Carneiro, 26-Apr-2015.)
|- ( ( A e. V /\ B e. W ) -> <. A , B >. = { { A } , { A , B } } )
Theorem	dfop 3776	Value of an ordered pair when the arguments are sets, with the conclusion corresponding to Kuratowski's original definition. (Contributed by NM, 25-Jun-1998.)
|- A e. _V   &    |- B e. _V   =>    |- <. A , B >. = { { A } , { A , B } }
Theorem	opeq1 3777	Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- ( A = B -> <. A , C >. = <. B , C >. )
Theorem	opeq2 3778	Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- ( A = B -> <. C , A >. = <. C , B >. )
Theorem	opeq12 3779	Equality theorem for ordered pairs. (Contributed by NM, 28-May-1995.)
|- ( ( A = C /\ B = D ) -> <. A , B >. = <. C , D >. )
Theorem	opeq1i 3780	Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.)
|- A = B   =>    |- <. A , C >. = <. B , C >.
Theorem	opeq2i 3781	Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.)
|- A = B   =>    |- <. C , A >. = <. C , B >.
Theorem	opeq12i 3782	Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.) (Proof shortened by Eric Schmidt, 4-Apr-2007.)
|- A = B   &    |- C = D   =>    |- <. A , C >. = <. B , D >.
Theorem	opeq1d 3783	Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.)
|- ( ph -> A = B )   =>    |- ( ph -> <. A , C >. = <. B , C >. )
Theorem	opeq2d 3784	Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.)
|- ( ph -> A = B )   =>    |- ( ph -> <. C , A >. = <. C , B >. )
Theorem	opeq12d 3785	Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> <. A , C >. = <. B , D >. )
Theorem	oteq1 3786	Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015.)
|- ( A = B -> <. A , C , D >. = <. B , C , D >. )
Theorem	oteq2 3787	Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015.)
|- ( A = B -> <. C , A , D >. = <. C , B , D >. )
Theorem	oteq3 3788	Equality theorem for ordered triples. (Contributed by NM, 3-Apr-2015.)
|- ( A = B -> <. C , D , A >. = <. C , D , B >. )
Theorem	oteq1d 3789	Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- ( ph -> A = B )   =>    |- ( ph -> <. A , C , D >. = <. B , C , D >. )
Theorem	oteq2d 3790	Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- ( ph -> A = B )   =>    |- ( ph -> <. C , A , D >. = <. C , B , D >. )
Theorem	oteq3d 3791	Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- ( ph -> A = B )   =>    |- ( ph -> <. C , D , A >. = <. C , D , B >. )
Theorem	oteq123d 3792	Equality deduction for ordered triples. (Contributed by Mario Carneiro, 11-Jan-2017.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   &    |- ( ph -> E = F )   =>    |- ( ph -> <. A , C , E >. = <. B , D , F >. )
Theorem	nfop 3793	Bound-variable hypothesis builder for ordered pairs. (Contributed by NM, 14-Nov-1995.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/_ x <. A , B >.
Theorem	nfopd 3794	Deduction version of bound-variable hypothesis builder nfop 3793. This shows how the deduction version of a not-free theorem such as nfop 3793 can be created from the corresponding not-free inference theorem. (Contributed by NM, 4-Feb-2008.)
|- ( ph -> F/_ x A )   &    |- ( ph -> F/_ x B )   =>    |- ( ph -> F/_ x <. A , B >. )
Theorem	opid 3795	The ordered pair <. A , A >. in Kuratowski's representation. (Contributed by FL, 28-Dec-2011.)
|- A e. _V   =>    |- <. A , A >. = { { A } }
Theorem	ralunsn 3796*	Restricted quantification over the union of a set and a singleton, using implicit substitution. (Contributed by Paul Chapman, 17-Nov-2012.) (Revised by Mario Carneiro, 23-Apr-2015.)
|- ( x = B -> ( ph <-> ps ) )   =>    |- ( B e. C -> ( A. x e. ( A u. { B } ) ph <-> ( A. x e. A ph /\ ps ) ) )
Theorem	2ralunsn 3797*	Double restricted quantification over the union of a set and a singleton, using implicit substitution. (Contributed by Paul Chapman, 17-Nov-2012.)
|- ( x = B -> ( ph <-> ch ) )   &    |- ( y = B -> ( ph <-> ps ) )   &    |- ( x = B -> ( ps <-> th ) )   =>    |- ( B e. C -> ( A. x e. ( A u. { B } ) A. y e. ( A u. { B } ) ph <-> ( ( A. x e. A A. y e. A ph /\ A. x e. A ps ) /\ ( A. y e. A ch /\ th ) ) ) )
Theorem	opprc 3798	Expansion of an ordered pair when either member is a proper class. (Contributed by Mario Carneiro, 26-Apr-2015.)
|- ( -. ( A e. _V /\ B e. _V ) -> <. A , B >. = (/) )
Theorem	opprc1 3799	Expansion of an ordered pair when the first member is a proper class. See also opprc 3798. (Contributed by NM, 10-Apr-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- ( -. A e. _V -> <. A , B >. = (/) )
Theorem	opprc2 3800	Expansion of an ordered pair when the second member is a proper class. See also opprc 3798. (Contributed by NM, 15-Nov-1994.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- ( -. B e. _V -> <. A , B >. = (/) )