P. 44 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 4301-4400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	prprc2 4301	A proper class vanishes in an unordered pair. (Contributed by NM, 22-Mar-2006.)
|- ( -. B e. _V -> { A , B } = { A } )
Theorem	prprc 4302	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 4303	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	tpid2 4304	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	tpid3g 4305	Closed theorem form of tpid3 4307. (Contributed by Alan Sare, 24-Oct-2011.) (Proof shortened by JJ, 30-Apr-2021.)
|- ( A e. B -> A e. { C , D , A } )
Theorem	tpid3gOLD 4306	Obsolete proof of tpid3g 4305 as of 30-Apr-2021. Closed theorem form of tpid3 4307. This proof was automatically generated from the virtual deduction proof tpid3gVD 39077 using a translation program. (Contributed by Alan Sare, 24-Oct-2011.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( A e. B -> A e. { C , D , A } )
Theorem	tpid3 4307	One of the three elements of an unordered triple. (Contributed by NM, 7-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) (Proof shortened by JJ, 30-Apr-2021.)
|- C e. _V   =>    |- C e. { A , B , C }
Theorem	snnzg 4308	The singleton of a set is not empty. (Contributed by NM, 14-Dec-2008.)
|- ( A e. V -> { A } =/= (/) )
Theorem	snnz 4309	The singleton of a set is not empty. (Contributed by NM, 10-Apr-1994.)
|- A e. _V   =>    |- { A } =/= (/)
Theorem	prnz 4310	A pair containing a set is not empty. (Contributed by NM, 9-Apr-1994.)
|- A e. _V   =>    |- { A , B } =/= (/)
Theorem	prnzg 4311	A pair containing a set is not empty. (Contributed by FL, 19-Sep-2011.) (Proof shortened by JJ, 23-Jul-2021.)
|- ( A e. V -> { A , B } =/= (/) )
Theorem	prnzgOLD 4312	Obsolete proof of prnzg 4311 as of 23-Jul-2021. (Contributed by FL, 19-Sep-2011.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( A e. V -> { A , B } =/= (/) )
Theorem	tpnz 4313	A triplet containing a set is not empty. (Contributed by NM, 10-Apr-1994.)
|- A e. _V   =>    |- { A , B , C } =/= (/)
Theorem	tpnzd 4314	A triplet containing a set is not empty. (Contributed by Thierry Arnoux, 8-Apr-2019.)
|- ( ph -> A e. V )   =>    |- ( ph -> { A , B , C } =/= (/) )
Theorem	raltpd 4315*	Convert a quantification over a triple to a conjunction. (Contributed by Thierry Arnoux, 8-Apr-2019.)
|- ( ( ph /\ x = A ) -> ( ps <-> ch ) )   &    |- ( ( ph /\ x = B ) -> ( ps <-> th ) )   &    |- ( ( ph /\ x = C ) -> ( ps <-> ta ) )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   =>    |- ( ph -> ( A. x e. { A , B , C } ps <-> ( ch /\ th /\ ta ) ) )
Theorem	snss 4316	The singleton of an element of a class is a subset of the class. Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 21-Jun-1993.)
|- A e. _V   =>    |- ( A e. B <-> { A } C_ B )
Theorem	eldifsn 4317	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 4318	Subset of a set with an element removed. (Contributed by Emmett Weisz, 7-Jul-2021.)
|- ( A C_ ( B \ { C } ) <-> ( A C_ B /\ -. C e. A ) )
Theorem	elpwdifsn 4319	A subset of a set is an element of the power set of the difference of the set with a singleton if the subset does not contain the singleton element. (Contributed by AV, 10-Jan-2020.)
|- ( ( S e. W /\ S C_ V /\ A e/ S ) -> S e. ~P ( V \ { A } ) )
Theorem	eldifsni 4320	Membership in a set with an element removed. (Contributed by NM, 10-Mar-2015.)
|- ( A e. ( B \ { C } ) -> A =/= C )
Theorem	neldifsn 4321	The class A is not in ( B \ { A } ). (Contributed by David Moews, 1-May-2017.)
|- -. A e. ( B \ { A } )
Theorem	neldifsnd 4322	The class A is not in ( B \ { A } ). Deduction form. (Contributed by David Moews, 1-May-2017.)
|- ( ph -> -. A e. ( B \ { A } ) )
Theorem	rexdifsn 4323	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	raldifsni 4324	Rearrangement of a property of a singleton difference. (Contributed by Stefan O'Rear, 27-Feb-2015.)
|- ( A. x e. ( A \ { B } ) -. ph <-> A. x e. A ( ph -> x = B ) )
Theorem	raldifsnb 4325*	Restricted universal quantification on a class difference with a singleton in terms of an implication. (Contributed by Alexander van der Vekens, 26-Jan-2018.)
|- ( A. x e. A ( x =/= Y -> ph ) <-> A. x e. ( A \ { Y } ) ph )
Theorem	eldifvsn 4326	A set is an element of the universal class excluding a singleton iff it is not the singleton element. (Contributed by AV, 7-Apr-2019.)
|- ( A e. V -> ( A e. ( _V \ { B } ) <-> A =/= B ) )
Theorem	snssg 4327	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 e. V -> ( A e. B <-> { A } C_ B ) )
Theorem	difsn 4328	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 4329	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 4330	Removal of a singleton from an unordered pair. (Contributed by Thierry Arnoux, 4-Feb-2017.)
|- ( A =/= B -> ( { A , B } \ { A } ) = { B } )
Theorem	difprsn2 4331	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 4332	Removal of a singleton from an unordered triple. (Contributed by Alexander van der Vekens, 5-Oct-2017.) (Proof shortened by JJ, 23-Jul-2021.)
|- ( ( A =/= C /\ B =/= C ) -> ( { A , B , C } \ { C } ) = { A , B } )
Theorem	diftpsn3OLD 4333	Obsolete proof of diftpsn3 4332 as of 23-Jul-2021. (Contributed by Alexander van der Vekens, 5-Oct-2017.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ( A =/= C /\ B =/= C ) -> ( { A , B , C } \ { C } ) = { A , B } )
Theorem	difpr 4334	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	tpprceq3 4335	An unordered triple is an unordered pair if one of its elements is a proper class or is identical with another element. (Contributed by Alexander van der Vekens, 6-Oct-2017.)
|- ( -. ( C e. _V /\ C =/= B ) -> { A , B , C } = { A , B } )
Theorem	tppreqb 4336	An unordered triple is an unordered pair if and only if one of its elements is a proper class or is identical with one of the another elements. (Contributed by Alexander van der Vekens, 15-Jan-2018.)
|- ( -. ( C e. _V /\ C =/= A /\ C =/= B ) <-> { A , B , C } = { A , B } )
Theorem	difsnb 4337	( B \ { A } ) equals B if and only if A is not a member of B. Generalization of difsn 4328. (Contributed by David Moews, 1-May-2017.)
|- ( -. A e. B <-> ( B \ { A } ) = B )
Theorem	difsnpss 4338	( B \ { A } ) is a proper subclass of B if and only if A is a member of B. (Contributed by David Moews, 1-May-2017.)
|- ( A e. B <-> ( B \ { A } ) C. B )
Theorem	snssi 4339	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 4340	The singleton of an element of a class is a subset of the class (deduction rule). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ph -> A e. B )   =>    |- ( ph -> { A } C_ B )
Theorem	difsnid 4341	If we remove a single element from a class then put it back in, we end up with the original class. (Contributed by NM, 2-Oct-2006.)
|- ( B e. A -> ( ( A \ { B } ) u. { B } ) = A )
Theorem	eldifeldifsn 4342	An element of a difference set is an element of the difference with a singleton. (Contributed by AV, 2-Jan-2022.)
|- ( ( X e. A /\ Y e. ( B \ A ) ) -> Y e. ( B \ { X } ) )
Theorem	pw0 4343	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	pwpw0 4344	Compute the power set of the power set of the empty set. (See pw0 4343 for the power set of the empty set.) Theorem 90 of [Suppes] p. 48. Although this theorem is a special case of pwsn 4428, we have chosen to show a direct elementary proof. (Contributed by NM, 7-Aug-1994.)
|- ~P { (/) } = { (/) , { (/) } }
Theorem	snsspr1 4345	A singleton is a subset of an unordered pair containing its member. (Contributed by NM, 27-Aug-2004.)
|- { A } C_ { A , B }
Theorem	snsspr2 4346	A singleton is a subset of an unordered pair containing its member. (Contributed by NM, 2-May-2009.)
|- { B } C_ { A , B }
Theorem	snsstp1 4347	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 4348	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 4349	A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.)
|- { C } C_ { A , B , C }
Theorem	prssg 4350	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	prss 4351	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.) (Proof shortened by JJ, 23-Jul-2021.)
|- A e. _V   &    |- B e. _V   =>    |- ( ( A e. C /\ B e. C ) <-> { A , B } C_ C )
Theorem	prssOLD 4352	Obsolete proof of prss 4351 as of 23-Jul-2021. (Contributed by NM, 30-May-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) (New usage is discouraged.) (Proof modification is discouraged.)
|- A e. _V   &    |- B e. _V   =>    |- ( ( A e. C /\ B e. C ) <-> { A , B } C_ C )
Theorem	prssi 4353	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	prssd 4354	Deduction version of prssi 4353: A pair of elements of a class is a subset of the class. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. C )   &    |- ( ph -> B e. C )   =>    |- ( ph -> { A , B } C_ C )
Theorem	prsspwg 4355	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	ssprss 4356	A pair as subset of a pair. (Contributed by AV, 26-Oct-2020.)
|- ( ( A e. V /\ B e. W ) -> ( { A , B } C_ { C , D } <-> ( ( A = C \/ A = D ) /\ ( B = C \/ B = D ) ) ) )
Theorem	ssprsseq 4357	A proper pair is a subset of a pair iff it is equal to the superset. (Contributed by AV, 26-Oct-2020.)
|- ( ( A e. V /\ B e. W /\ A =/= B ) -> ( { A , B } C_ { C , D } <-> { A , B } = { C , D } ) )
Theorem	sssn 4358	The subsets of a singleton. (Contributed by NM, 24-Apr-2004.)
|- ( A C_ { B } <-> ( A = (/) \/ A = { B } ) )
Theorem	ssunsn2 4359	The property of being sandwiched between two sets naturally splits under union with a singleton. This is the induction hypothesis for the determination of large powersets such as pwtp 4431. (Contributed by Mario Carneiro, 2-Jul-2016.)
|- ( ( B C_ A /\ A C_ ( C u. { D } ) ) <-> ( ( B C_ A /\ A C_ C ) \/ ( ( B u. { D } ) C_ A /\ A C_ ( C u. { D } ) ) ) )
Theorem	ssunsn 4360	Possible values for a set sandwiched between another set and it plus a singleton. (Contributed by Mario Carneiro, 2-Jul-2016.)
|- ( ( B C_ A /\ A C_ ( B u. { C } ) ) <-> ( A = B \/ A = ( B u. { C } ) ) )
Theorem	eqsn 4361*	Two ways to express that a nonempty set equals a singleton. (Contributed by NM, 15-Dec-2007.) (Proof shortened by JJ, 23-Jul-2021.)
|- ( A =/= (/) -> ( A = { B } <-> A. x e. A x = B ) )
Theorem	eqsnOLD 4362*	Obsolete proof of eqsn 4361 as of 23-Jul-2021. (Contributed by NM, 15-Dec-2007.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( A =/= (/) -> ( A = { B } <-> A. x e. A x = B ) )
Theorem	issn 4363*	A sufficient condition for a (nonempty) set to be a singleton. (Contributed by AV, 20-Sep-2020.)
|- ( E. x e. A A. y e. A x = y -> E. z A = { z } )
Theorem	n0snor2el 4364*	A nonempty set is either a singleton or contains at least two different elements. (Contributed by AV, 20-Sep-2020.)
|- ( A =/= (/) -> ( E. x e. A E. y e. A x =/= y \/ E. z A = { z } ) )
Theorem	ssunpr 4365	Possible values for a set sandwiched between another set and it plus a singleton. (Contributed by Mario Carneiro, 2-Jul-2016.)
|- ( ( B C_ A /\ A C_ ( B u. { C , D } ) ) <-> ( ( A = B \/ A = ( B u. { C } ) ) \/ ( A = ( B u. { D } ) \/ A = ( B u. { C , D } ) ) ) )
Theorem	sspr 4366	The subsets of a pair. (Contributed by NM, 16-Mar-2006.) (Proof shortened by Mario Carneiro, 2-Jul-2016.)
|- ( A C_ { B , C } <-> ( ( A = (/) \/ A = { B } ) \/ ( A = { C } \/ A = { B , C } ) ) )
Theorem	sstp 4367	The subsets of a triple. (Contributed by Mario Carneiro, 2-Jul-2016.)
|- ( A C_ { B , C , D } <-> ( ( ( A = (/) \/ A = { B } ) \/ ( A = { C } \/ A = { B , C } ) ) \/ ( ( A = { D } \/ A = { B , D } ) \/ ( A = { C , D } \/ A = { B , C , D } ) ) ) )
Theorem	tpss 4368	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 4369	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	sneqrg 4370	Closed form of sneqr 4371. (Contributed by Scott Fenton, 1-Apr-2011.) (Proof shortened by JJ, 23-Jul-2021.)
|- ( A e. V -> ( { A } = { B } -> A = B ) )
Theorem	sneqr 4371	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 4372	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	sneqrgOLD 4373	Obsolete proof of sneqrg 4370 as of 23-Jul-2021. (Contributed by Scott Fenton, 1-Apr-2011.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( A e. V -> ( { A } = { B } -> A = B ) )
Theorem	sneqbg 4374	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 4375	The singleton of a class is a subset of its power class. (Contributed by NM, 21-Jun-1993.)
|- { A } C_ ~P A
Theorem	prsspw 4376	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.) (Proof shortened by OpenAI, 25-Mar-2020.)
|- A e. _V   &    |- B e. _V   =>    |- ( { A , B } C_ ~P C <-> ( A C_ C /\ B C_ C ) )
Theorem	preq1b 4377	Biconditional equality lemma for unordered pairs, deduction form. Two unordered pairs have the same second element iff the first elements are equal. (Contributed by AV, 18-Dec-2020.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   =>    |- ( ph -> ( { A , C } = { B , C } <-> A = B ) )
Theorem	preq2b 4378	Biconditional equality lemma for unordered pairs, deduction form. Two unordered pairs have the same first element iff the second elements are equal. (Contributed by AV, 18-Dec-2020.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   =>    |- ( ph -> ( { C , A } = { C , B } <-> A = B ) )
Theorem	preqr1 4379	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	preqr1OLD 4380	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.) Obsolete version of preqr1 4379 as of 18-Dec-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- A e. _V   &    |- B e. _V   =>    |- ( { A , C } = { B , C } -> A = B )
Theorem	preqr2 4381	Reverse equality lemma for unordered pairs. If two unordered pairs have the same first element, the second elements are equal. (Contributed by NM, 15-Jul-1993.)
|- A e. _V   &    |- B e. _V   =>    |- ( { C , A } = { C , B } -> A = B )
Theorem	preq12b 4382	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 4383	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 4384	An unordered pair has the ordered pair property (compare opth 4945) under certain conditions. (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	preqr1g 4385	Reverse equality lemma for unordered pairs. If two unordered pairs have the same second element, the first elements are equal. Closed form of preqr1 4379. (Contributed by AV, 29-Jan-2021.) (Revised by AV, 18-Sep-2021.)
|- ( ( A e. V /\ B e. W ) -> ( { A , C } = { B , C } -> A = B ) )
Theorem	preq12bg 4386	Closed form of preq12b 4382. (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	prel12g 4387	Closed form of prel12 4383. (Contributed by AV, 9-Dec-2018.)
|- ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) -> ( -. A = B -> ( { A , B } = { C , D } <-> ( A e. { C , D } /\ B e. { C , D } ) ) ) )
Theorem	prneimg 4388	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	prnebg 4389	A (proper) pair is not equal to another (maybe improper) pair if and only if an element of the first pair is not contained in the second pair. (Contributed by Alexander van der Vekens, 16-Jan-2018.)
|- ( ( ( A e. U /\ B e. V ) /\ ( C e. X /\ D e. Y ) /\ A =/= B ) -> ( ( ( A =/= C /\ A =/= D ) \/ ( B =/= C /\ B =/= D ) ) <-> { A , B } =/= { C , D } ) )
Theorem	pr1eqbg 4390	A (proper) pair is equal to another (maybe improper) pair containing one element of the first pair if and only if the other element of the first pair is contained in the second pair. (Contributed by Alexander van der Vekens, 26-Jan-2018.)
|- ( ( ( A e. U /\ B e. V /\ C e. X ) /\ A =/= B ) -> ( A = C <-> { A , B } = { B , C } ) )
Theorem	pr1nebg 4391	A (proper) pair is not equal to another (maybe improper) pair containing one element of the first pair if and only if the other element of the first pair is not contained in the second pair. (Contributed by Alexander van der Vekens, 26-Jan-2018.)
|- ( ( ( A e. U /\ B e. V /\ C e. X ) /\ A =/= B ) -> ( A =/= C <-> { A , B } =/= { B , C } ) )
Theorem	preqsnd 4392	Equivalence for a pair equal to a singleton, deduction form. (Contributed by Thierry Arnoux, 27-Dec-2016.)
|- ( ph -> A e. _V )   &    |- ( ph -> B e. _V )   &    |- ( ph -> C e. _V )   =>    |- ( ph -> ( { A , B } = { C } <-> ( A = C /\ B = C ) ) )
Theorem	preqsn 4393	Equivalence for a pair equal to a singleton. (Contributed by NM, 3-Jun-2008.) (Proof shortened by JJ, 23-Jul-2021.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   =>    |- ( { A , B } = { C } <-> ( A = B /\ B = C ) )
Theorem	preqsnOLD 4394	Obsolete proof of preqsn 4393 as of 23-Jul-2021. (Contributed by NM, 3-Jun-2008.) (New usage is discouraged.) (Proof modification is discouraged.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   =>    |- ( { A , B } = { C } <-> ( A = B /\ B = C ) )
Theorem	elpreqprlem 4395*	Lemma for elpreqpr 4396. (Contributed by Scott Fenton, 7-Dec-2020.) (Revised by AV, 9-Dec-2020.)
|- ( B e. V -> E. x { B , C } = { B , x } )
Theorem	elpreqpr 4396*	Equality and membership rule for pairs. (Contributed by Scott Fenton, 7-Dec-2020.)
|- ( A e. { B , C } -> E. x { B , C } = { A , x } )
Theorem	elpreqprb 4397*	A set is an element of an unordered pair iff there is another (maybe the same) set which is an element of the unordered pair. (Proposed by BJ, 8-Dec-2020.) (Contributed by AV, 9-Dec-2020.)
|- ( A e. V -> ( A e. { B , C } <-> E. x { B , C } = { A , x } ) )
Theorem	elpr2elpr 4398*	For an element A of an unordered pair which is a subset of a given set V, there is another (maybe the same) element b of the given set V being an element of the unordered pair. (Contributed by AV, 5-Dec-2020.)
|- ( ( X e. V /\ Y e. V /\ A e. { X , Y } ) -> E. b e. V { X , Y } = { A , b } )
Theorem	dfopif 4399	Rewrite df-op 4184 using if. When both arguments are sets, it reduces to the standard Kuratowski definition; otherwise, it is defined to be the empty set. Avoid directly depending on this detail so that theorems will not depend on the Kuratowski construction. (Contributed by Mario Carneiro, 26-Apr-2015.) (Avoid depending on this detail.)
|- <. A , B >. = if ( ( A e. _V /\ B e. _V ) , { { A } , { A , B } } , (/) )
Theorem	dfopg 4400	Value of the ordered pair when the arguments are sets. (Contributed by Mario Carneiro, 26-Apr-2015.) (Avoid depending on this detail.)
|- ( ( A e. V /\ B e. W ) -> <. A , B >. = { { A } , { A , B } } )