P. 330 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32901-33000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bj-abv 32901	The class of sets verifying a tautology is the universal class. (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.)
|- ( A. x ph -> { x | ph } = _V )
Theorem	bj-ab0 32902	The class of sets verifying a falsity is the empty set (closed form of abf 3978). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.)
|- ( A. x -. ph -> { x | ph } = (/) )
Theorem	bj-abf 32903	Shorter proof of abf 3978 (which should be kept as abfALT). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.)
|- -. ph   =>    |- { x | ph } = (/)
Theorem	bj-csbprc 32904	More direct proof of csbprc 3980 (fewer essential steps). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.)
|- ( -. A e. _V -> [_ A / x ]_ B = (/) )
20.14.5.6  Removing some dv conditions
Theorem	bj-exlimmpi 32905	Lemma for bj-vtoclg1f1 32910 (an instance of this lemma is a version of bj-vtoclg1f1 32910 where x and y are identified). (Contributed by BJ, 30-Apr-2019.) (Proof modification is discouraged.)
|- F/ x ps   &    |- ( ch -> ( ph -> ps ) )   &    |- ph   =>    |- ( E. x ch -> ps )
Theorem	bj-exlimmpbi 32906	Lemma for theorems of the vtoclg 3266 family. (Contributed by BJ, 3-Oct-2019.) (Proof modification is discouraged.)
|- F/ x ps   &    |- ( ch -> ( ph <-> ps ) )   &    |- ph   =>    |- ( E. x ch -> ps )
Theorem	bj-exlimmpbir 32907	Lemma for theorems of the vtoclg 3266 family. (Contributed by BJ, 3-Oct-2019.) (Proof modification is discouraged.)
|- F/ x ph   &    |- ( ch -> ( ph <-> ps ) )   &    |- ps   =>    |- ( E. x ch -> ph )
Theorem	bj-vtoclf 32908*	Remove dependency on ax-ext 2602, df-clab 2609 and df-cleq 2615 (and df-sb 1881 and df-v 3202) from vtoclf 3258. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.)
|- F/ x ps   &    |- A e. V   &    |- ( x = A -> ( ph <-> ps ) )   &    |- ph   =>    |- ps
Theorem	bj-vtocl 32909*	Remove dependency on ax-ext 2602, df-clab 2609 and df-cleq 2615 (and df-sb 1881 and df-v 3202) from vtocl 3259. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.)
|- A e. V   &    |- ( x = A -> ( ph <-> ps ) )   &    |- ph   =>    |- ps
Theorem	bj-vtoclg1f1 32910*	The FOL content of vtoclg1f 3265 (hence not using ax-ext 2602, df-cleq 2615, df-nfc 2753, df-v 3202). Note the weakened "major" hypothesis and the dv condition between x and A (needed since the class-form non-free predicate is not available without ax-ext 2602; as a byproduct, this dispenses with ax-11 2034 and ax-13 2246). (Contributed by BJ, 30-Apr-2019.) (Proof modification is discouraged.)
|- F/ x ps   &    |- ( x = A -> ( ph -> ps ) )   &    |- ph   =>    |- ( E. y y = A -> ps )
Theorem	bj-vtoclg1f 32911*	Reprove vtoclg1f 3265 from bj-vtoclg1f1 32910. This removes dependency on ax-ext 2602, df-cleq 2615 and df-v 3202. Use bj-vtoclg1fv 32912 instead when sufficient (in particular when V is substituted for _V). (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.)
|- F/ x ps   &    |- ( x = A -> ( ph -> ps ) )   &    |- ph   =>    |- ( A e. V -> ps )
Theorem	bj-vtoclg1fv 32912*	Version of bj-vtoclg1f 32911 with a dv condition on x , V. This removes dependency on df-sb 1881 and df-clab 2609. Prefer its use over bj-vtoclg1f 32911 when sufficient (in particular when V is substituted for _V). (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.)
|- F/ x ps   &    |- ( x = A -> ( ph -> ps ) )   &    |- ph   =>    |- ( A e. V -> ps )
Theorem	bj-rabbida2 32913	Version of rabbidva2 3186 with dv condition replaced by non-freeness hypothesis. (Contributed by BJ, 27-Apr-2019.)
|- F/ x ph   &    |- ( ph -> ( ( x e. A /\ ps ) <-> ( x e. B /\ ch ) ) )   =>    |- ( ph -> { x e. A | ps } = { x e. B | ch } )
Theorem	bj-rabbida 32914	Version of rabbidva 3188 with dv condition replaced by non-freeness hypothesis. (Contributed by BJ, 27-Apr-2019.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )   =>    |- ( ph -> { x e. A | ps } = { x e. A | ch } )
Theorem	bj-rabbid 32915	Version of rabbidv 3189 with dv condition replaced by non-freeness hypothesis. (Contributed by BJ, 27-Apr-2019.)
|- F/ x ph   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> { x e. A | ps } = { x e. A | ch } )
Theorem	bj-rabeqd 32916	Deduction form of rabeq 3192. Note that contrary to rabeq 3192 it has no dv condition. (Contributed by BJ, 27-Apr-2019.)
|- F/ x ph   &    |- ( ph -> A = B )   =>    |- ( ph -> { x e. A | ps } = { x e. B | ps } )
Theorem	bj-rabeqbid 32917	Version of rabeqbidv 3195 with two dv conditions removed and the third replaced by a non-freeness hypothesis. (Contributed by BJ, 27-Apr-2019.)
|- F/ x ph   &    |- ( ph -> A = B )   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> { x e. A | ps } = { x e. B | ch } )
Theorem	bj-rabeqbida 32918	Version of rabeqbidva 3196 with two dv conditions removed and the third replaced by a non-freeness hypothesis. (Contributed by BJ, 27-Apr-2019.)
|- F/ x ph   &    |- ( ph -> A = B )   &    |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )   =>    |- ( ph -> { x e. A | ps } = { x e. B | ch } )
Theorem	bj-seex 32919*	Version of seex 5077 with a dv condition replaced by a non-freeness hypothesis (for the sake of illustration). (Contributed by BJ, 27-Apr-2019.)
|- F/_ x B   =>    |- ( ( R Se A /\ B e. A ) -> { x e. A | x R B } e. _V )
Theorem	bj-nfcf 32920*	Version of df-nfc 2753 with a dv condition replaced with a non-freeness hypothesis. (Contributed by BJ, 2-May-2019.)
|- F/_ y A   =>    |- ( F/_ x A <-> A. y F/ x y e. A )
Theorem	bj-axsep2 32921*	Remove dependency on ax-12 2047 and ax-13 2246 from axsep2 4782 while shortening its proof. Remark: the comment in zfauscl 4783 is misleading: the essential use of ax-ext 2602 is the one via eleq2 2690 and not the one via vtocl 3259, since the latter can be proved without ax-ext 2602 (see bj-vtocl 32909). (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.)
|- E. y A. x ( x e. y <-> ( x e. z /\ ph ) )
20.14.5.7  Class abstractions A few additional theorems on class abstractions and restricted class abstractions.
Theorem	bj-unrab 32922*	Generalization of unrab 3898. Equality need not hold. (Contributed by BJ, 21-Apr-2019.)
|- ( { x e. A | ph } u. { x e. B | ps } ) C_ { x e. ( A u. B ) | ( ph \/ ps ) }
Theorem	bj-inrab 32923	Generalization of inrab 3899. (Contributed by BJ, 21-Apr-2019.)
|- ( { x e. A | ph } i^i { x e. B | ps } ) = { x e. ( A i^i B ) | ( ph /\ ps ) }
Theorem	bj-inrab2 32924	Shorter proof of inrab 3899. (Contributed by BJ, 21-Apr-2019.) (Proof modification is discouraged.)
|- ( { x e. A | ph } i^i { x e. A | ps } ) = { x e. A | ( ph /\ ps ) }
Theorem	bj-inrab3 32925*	Generalization of dfrab3ss 3905, which it may shorten. (Contributed by BJ, 21-Apr-2019.) (Revised by OpenAI, 7-Jul-2020.)
|- ( A i^i { x e. B | ph } ) = ( { x e. A | ph } i^i B )
Theorem	bj-rabtr 32926*	Restricted class abstraction with true formula. (Contributed by BJ, 22-Apr-2019.)
|- { x e. A | T. } = A
Theorem	bj-rabtrALT 32927*	Alternate proof of bj-rabtr 32926. (Contributed by BJ, 22-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- { x e. A | T. } = A
Theorem	bj-rabtrALTALT 32928*	Alternate proof of bj-rabtr 32926. (Contributed by BJ, 22-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- { x e. A | T. } = A
Theorem	bj-rabtrAUTO 32929*	Proof of bj-rabtr 32926 found automatically by "improve all /depth 3 /3" followed by "minimize *". (Contributed by BJ, 22-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- { x e. A | T. } = A
20.14.5.8  Restricted non-freeness In this subsection, we define restricted non-freeness (or relative non-freeness).
Syntax	wrnf 32930	Syntax for restricted non-freeness.
wff F/ x e. A ph
Definition	df-bj-rnf 32931	Definition of restricted non-freeness. Informally, the proposition F/ x e. A ph means that ph ( x ) does not vary on A. (Contributed by BJ, 19-Mar-2021.)
|- ( F/ x e. A ph <-> ( E. x e. A ph -> A. x e. A ph ) )
20.14.5.9  Russell's paradox A few results around Russell's paradox. For clarity, we prove separately its FOL part (bj-ru0 32932) and then two versions (bj-ru1 32933 and bj-ru 32934). Special attention is put on minimizing axiom depencencies.
Theorem	bj-ru0 32932*	The FOL part of Russell's paradox ru 3434 (see also bj-ru1 32933, bj-ru 32934). Use of elequ1 1997, bj-elequ12 32668, bj-spvv 32723 (instead of eleq1 2689, eleq12d 2695, spv 2260 as in ru 3434) permits to remove dependency on ax-10 2019, ax-11 2034, ax-12 2047, ax-13 2246, ax-ext 2602, df-sb 1881, df-clab 2609, df-cleq 2615, df-clel 2618. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
|- -. A. x ( x e. y <-> -. x e. x )
Theorem	bj-ru1 32933*	A version of Russell's paradox ru 3434 (see also bj-ru 32934). Note the more economical use of bj-abeq2 32773 instead of abeq2 2732 to avoid dependency on ax-13 2246. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
|- -. E. y y = { x | -. x e. x }
Theorem	bj-ru 32934	Remove dependency on ax-13 2246 (and df-v 3202) from Russell's paradox ru 3434 expressed with primitive symbols and with a class variable V (note that axsep2 4782 does require ax-8 1992 and ax-9 1999 since it requires df-clel 2618 and df-cleq 2615--- see bj-df-clel 32888 and bj-df-cleq 32893). Note the more economical use of bj-elissetv 32861 instead of isset 3207 to avoid use of df-v 3202. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
|- -. { x | -. x e. x } e. V
20.14.5.10  Some disjointness results A few utility theorems on disjointness of classes.
Theorem	bj-n0i 32935*	Inference associated with n0 3931. Shortens 2ndcdisj 21259 (2888>2878), notzfaus 4840 (264>253). (Contributed by BJ, 22-Apr-2019.)
|- A =/= (/)   =>    |- E. x x e. A
Theorem	bj-disjcsn 32936	A class is disjoint from its singleton. A consequence of regularity. Shorter proof than bnj521 30805 and does not depend on df-ne 2795. (Contributed by BJ, 4-Apr-2019.)
|- ( A i^i { A } ) = (/)
Theorem	bj-disjsn01 32937	Disjointness of the singletons containing 0 and 1. This is a consequence of bj-disjcsn 32936 but the present proof does not use regularity. (Contributed by BJ, 4-Apr-2019.) (Proof modification is discouraged.)
|- ( { (/) } i^i { 1o } ) = (/)
Theorem	bj-1ex 32938	1o is a set. (Contributed by BJ, 6-Apr-2019.)
|- 1o e. _V
Theorem	bj-2ex 32939	2o is a set. (Contributed by BJ, 6-Apr-2019.)
|- 2o e. _V
Theorem	bj-0nel1 32940	The empty set does not belong to { 1o }. (Contributed by BJ, 6-Apr-2019.)
|- (/) e/ { 1o }
Theorem	bj-1nel0 32941	1o does not belong to { (/) }. (Contributed by BJ, 6-Apr-2019.)
|- 1o e/ { (/) }
20.14.5.11  Complements on direct products A few utility theorems on direct products.
Theorem	bj-xpimasn 32942	The image of a singleton, general case. [Change and relabel xpimasn 5579 accordingly, maybe to xpima2sn.] (Contributed by BJ, 6-Apr-2019.)
|- ( ( A X. B ) " { X } ) = if ( X e. A , B , (/) )
Theorem	bj-xpima1sn 32943	The image of a singleton by a direct product, empty case. [Change and relabel xpimasn 5579 accordingly, maybe to xpima2sn.] (Contributed by BJ, 6-Apr-2019.)
|- ( X e/ A -> ( ( A X. B ) " { X } ) = (/) )
Theorem	bj-xpima1snALT 32944	Alternate proof of bj-xpima1sn 32943. (Contributed by BJ, 6-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( X e/ A -> ( ( A X. B ) " { X } ) = (/) )
Theorem	bj-xpima2sn 32945	The image of a singleton by a direct product, nonempty case. [To replace xpimasn 5579] (Contributed by BJ, 6-Apr-2019.) (Proof modification is discouraged.)
|- ( X e. A -> ( ( A X. B ) " { X } ) = B )
Theorem	bj-xpnzex 32946	If the first factor of a product is nonempty, and the product is a set, then the second factor is a set. UPDATE: this is actually the curried (exported) form of xpexcnv 7108 (up to commutation in the product). (Contributed by BJ, 6-Oct-2018.) (Proof modification is discouraged.)
|- ( A =/= (/) -> ( ( A X. B ) e. V -> B e. _V ) )
Theorem	bj-xpexg2 32947	Curried (exported) form of xpexg 6960. (Contributed by BJ, 2-Apr-2019.)
|- ( A e. V -> ( B e. W -> ( A X. B ) e. _V ) )
Theorem	bj-xpnzexb 32948	If the first factor of a product is a nonempty set, then the product is a set if and only if the second factor is a set. (Contributed by BJ, 2-Apr-2019.)
|- ( A e. ( V \ { (/) } ) -> ( B e. _V <-> ( A X. B ) e. _V ) )
Theorem	bj-cleq 32949*	Substitution property for certain classes. (Contributed by BJ, 2-Apr-2019.)
|- ( A = B -> { x | { x } e. ( A " C ) } = { x | { x } e. ( B " C ) } )
20.14.5.12  "Singletonization" and tagging This subsection introduces the "singletonization" and the "tagging" of a class. The singletonization of a class is the class of singletons of elements of that class. It is useful since all nonsingletons are disjoint from it, so one can easily adjoin to it disjoint elements, which is what the tagging does: it adjoins the empty set. This can be used for instance to define the one-point compactification of a topological space. It will be used in the next section to define tuples which work for proper classes.
Theorem	bj-sels 32950*	If a class is a set, then it is a member of a set. (Contributed by BJ, 3-Apr-2019.)
|- ( A e. V -> E. x A e. x )
Theorem	bj-snsetex 32951*	The class of sets "whose singletons" belong to a set is a set. Nice application of ax-rep 4771. (Contributed by BJ, 6-Oct-2018.)
|- ( A e. V -> { x | { x } e. A } e. _V )
Theorem	bj-clex 32952*	Sethood of certain classes. (Contributed by BJ, 2-Apr-2019.)
|- ( A e. V -> { x | { x } e. ( A " B ) } e. _V )
Syntax	bj-csngl 32953	Syntax for singletonization. (Contributed by BJ, 6-Oct-2018.)
class sngl A
Definition	df-bj-sngl 32954*	Definition of "singletonization". The class sngl A is isomorphic to A and since it contains only singletons, it can be adjoined disjoint elements, which can be useful in various constructions. (Contributed by BJ, 6-Oct-2018.)
|- sngl A = { x | E. y e. A x = { y } }
Theorem	bj-sngleq 32955	Substitution property for sngl. (Contributed by BJ, 6-Oct-2018.)
|- ( A = B -> sngl A = sngl B )
Theorem	bj-elsngl 32956*	Characterization of the elements of the singletonization of a class. (Contributed by BJ, 6-Oct-2018.)
|- ( A e. sngl B <-> E. x e. B A = { x } )
Theorem	bj-snglc 32957	Characterization of the elements of A in terms of elements of its singletonization. (Contributed by BJ, 6-Oct-2018.)
|- ( A e. B <-> { A } e. sngl B )
Theorem	bj-snglss 32958	The singletonization of a class is included in its powerclass. (Contributed by BJ, 6-Oct-2018.)
|- sngl A C_ ~P A
Theorem	bj-0nelsngl 32959	The empty set is not a member of a singletonization (neither is any nonsingleton, in particular any von Neuman ordinal except possibly df-1o 7560). (Contributed by BJ, 6-Oct-2018.)
|- (/) e/ sngl A
Theorem	bj-snglinv 32960*	Inverse of singletonization. (Contributed by BJ, 6-Oct-2018.)
|- A = { x | { x } e. sngl A }
Theorem	bj-snglex 32961	A class is a set if and only if its singletonization is a set. (Contributed by BJ, 6-Oct-2018.)
|- ( A e. _V <-> sngl A e. _V )
Syntax	bj-ctag 32962	Syntax for the tagged copy of a class. (Contributed by BJ, 6-Oct-2018.)
class tag A
Definition	df-bj-tag 32963	Definition of the tagged copy of a class, that is, the adjunction to (an isomorph of) A of a disjoint element (here, the empty set). Remark: this could be used for the one-point compactification of a topological space. (Contributed by BJ, 6-Oct-2018.)
|- tag A = (sngl A u. { (/) } )
Theorem	bj-tageq 32964	Substitution property for tag. (Contributed by BJ, 6-Oct-2018.)
|- ( A = B -> tag A = tag B )
Theorem	bj-eltag 32965*	Characterization of the elements of the tagging of a class. (Contributed by BJ, 6-Oct-2018.)
|- ( A e. tag B <-> ( E. x e. B A = { x } \/ A = (/) ) )
Theorem	bj-0eltag 32966	The empty set belongs to the tagging of a class. (Contributed by BJ, 6-Apr-2019.)
|- (/) e. tag A
Theorem	bj-tagn0 32967	The tagging of a class is nonempty. (Contributed by BJ, 6-Apr-2019.)
|- tag A =/= (/)
Theorem	bj-tagss 32968	The tagging of a class is included in its powerclass. (Contributed by BJ, 6-Oct-2018.)
|- tag A C_ ~P A
Theorem	bj-snglsstag 32969	The singletonization is included in the tagging. (Contributed by BJ, 6-Oct-2018.)
|- sngl A C_ tag A
Theorem	bj-sngltagi 32970	The singletonization is included in the tagging. (Contributed by BJ, 6-Oct-2018.)
|- ( A e. sngl B -> A e. tag B )
Theorem	bj-sngltag 32971	The singletonization and the tagging of a set contain the same singletons. (Contributed by BJ, 6-Oct-2018.)
|- ( A e. V -> ( { A } e. sngl B <-> { A } e. tag B ) )
Theorem	bj-tagci 32972	Characterization of the elements of B in terms of elements of its tagged version. (Contributed by BJ, 6-Oct-2018.)
|- ( A e. B -> { A } e. tag B )
Theorem	bj-tagcg 32973	Characterization of the elements of B in terms of elements of its tagged version. (Contributed by BJ, 6-Oct-2018.)
|- ( A e. V -> ( A e. B <-> { A } e. tag B ) )
Theorem	bj-taginv 32974*	Inverse of tagging. (Contributed by BJ, 6-Oct-2018.)
|- A = { x | { x } e. tag A }
Theorem	bj-tagex 32975	A class is a set if and only if its tagging is a set. (Contributed by BJ, 6-Oct-2018.)
|- ( A e. _V <-> tag A e. _V )
Theorem	bj-xtageq 32976	The products of a given class and the tagging of either of two equal classes are equal. (Contributed by BJ, 6-Apr-2019.)
|- ( A = B -> ( C X. tag A ) = ( C X. tag B ) )
Theorem	bj-xtagex 32977	The product of a set and the tagging of a set is a set. (Contributed by BJ, 2-Apr-2019.)
|- ( A e. V -> ( B e. W -> ( A X. tag B ) e. _V ) )
20.14.5.13  Tuples of classes This subsection gives a definition of an ordered pair, or couple (2-tuple), which "works" for proper classes, as evidenced by Theorems bj-2uplth 33009 and bj-2uplex 33010 (but more importantly, bj-pr21val 33001 and bj-pr22val 33007). In particular, one can define well-behaved tuples of classes. Note, however, that classes in ZF(C) are only virtual, and in particular they cannot be quantified over. The projections are denoted by pr1 and pr2 and the couple with projections (or coordinates) A and B is denoted by (| A, B|). Note that this definition uses the Kuratowksi definition (df-op 4184) as a preliminary definition, and then "redefines" a couple. It could also use the "short" version of the Kuratowski pair (see opthreg 8515) without needing the axiom of regularity; it could even bypass this definition by "inlining" it. This definition is due to Anthony Morse and is expounded (with idiosyncratic notation) in Anthony P. Morse, A Theory of Sets, Academic Press, 1965 (second edition 1986). Note that this extends in a natural way to tuples. A variation of this definition is justified in opthprc 5167, but here we use "tagged versions" of the factors (see df-bj-tag 32963) so that an m-tuple can equal an n-tuple only when m = n (and the projections are the same). A comparison of the different definitions of tuples (strangely not mentioning Morse's), is given in Dominic McCarty and Dana Scott, Reconsidering ordered pairs, Bull. Symbolic Logic, Volume 14, Issue 3 (Sept. 2008), 379--397. where a recursive definition of tuples is given that avoids the 2-step definition of tuples and that can be adapted to various set theories. Finally, another survey is Akihiro Kanamori, The empty set, the singleton, and the ordered pair, Bull. Symbolic Logic, Volume 9, Number 3 (Sept. 2003), 273--298. (available at http://math.bu.edu/people/aki/8.pdf)
Syntax	bj-cproj 32978	Syntax for the class projection. (Contributed by BJ, 6-Apr-2019.)
class ( A Proj B )
Definition	df-bj-proj 32979*	Definition of the class projection corresponding to tagged tuples. The expression ( A Proj B ) denotes the projection on the A^th component. (Contributed by BJ, 6-Apr-2019.) (New usage is discouraged.)
|- ( A Proj B ) = { x | { x } e. ( B " { A } ) }
Theorem	bj-projeq 32980	Substitution property for Proj. (Contributed by BJ, 6-Apr-2019.)
|- ( A = C -> ( B = D -> ( A Proj B ) = ( C Proj D ) ) )
Theorem	bj-projeq2 32981	Substitution property for Proj. (Contributed by BJ, 6-Apr-2019.)
|- ( B = C -> ( A Proj B ) = ( A Proj C ) )
Theorem	bj-projun 32982	The class projection on a given component preserves unions. (Contributed by BJ, 6-Apr-2019.)
|- ( A Proj ( B u. C ) ) = ( ( A Proj B ) u. ( A Proj C ) )
Theorem	bj-projex 32983	Sethood of the class projection. (Contributed by BJ, 6-Apr-2019.)
|- ( B e. V -> ( A Proj B ) e. _V )
Theorem	bj-projval 32984	Value of the class projection. (Contributed by BJ, 6-Apr-2019.)
|- ( A e. V -> ( A Proj ( { B } X. tag C ) ) = if ( B = A , C , (/) ) )
Syntax	bj-c1upl 32985	Syntax for Morse monuple. (Contributed by BJ, 6-Apr-2019.)
class (| A|)
Definition	df-bj-1upl 32986	Definition of the Morse monuple (1-tuple). This is not useful per se, but is used as a step towards the definition of couples (2-tuples, or ordered pairs). The reason for "tagging" the set is so that an m-tuple and an n-tuple be equal only when m = n. Note that with this definition, the 0-tuple is the empty set. New usage is discouraged because the precise definition is generally unimportant compared to the characteristic properties bj-2upleq 33000, bj-2uplth 33009, bj-2uplex 33010, and the properties of the projections (see df-bj-pr1 32989 and df-bj-pr2 33003). (Contributed by BJ, 6-Apr-2019.) (New usage is discouraged.)
|- (| A|) = ( { (/) } X. tag A )
Theorem	bj-1upleq 32987	Substitution property for (| - |). (Contributed by BJ, 6-Apr-2019.)
|- ( A = B -> (| A|) = (| B|) )
Syntax	bj-cpr1 32988	Syntax for the first class tuple projection. (Contributed by BJ, 6-Apr-2019.)
class pr1 A
Definition	df-bj-pr1 32989	Definition of the first projection of a class tuple. New usage is discouraged because the precise definition is generally unimportant compared to the characteristic properties bj-pr1eq 32990, bj-pr11val 32993, bj-pr21val 33001, bj-pr1ex 32994. (Contributed by BJ, 6-Apr-2019.) (New usage is discouraged.)
|- pr1 A = ( (/) Proj A )
Theorem	bj-pr1eq 32990	Substitution property for pr1. (Contributed by BJ, 6-Apr-2019.)
|- ( A = B -> pr1 A = pr1 B )
Theorem	bj-pr1un 32991	The first projection preserves unions. (Contributed by BJ, 6-Apr-2019.)
|- pr1 ( A u. B ) = (pr1 A u. pr1 B )
Theorem	bj-pr1val 32992	Value of the first projection. (Contributed by BJ, 6-Apr-2019.)
|- pr1 ( { A } X. tag B ) = if ( A = (/) , B , (/) )
Theorem	bj-pr11val 32993	Value of the first projection of a monuple. (Contributed by BJ, 6-Apr-2019.)
|- pr1 (| A|) = A
Theorem	bj-pr1ex 32994	Sethood of the first projection. (Contributed by BJ, 6-Oct-2018.)
|- ( A e. V -> pr1 A e. _V )
Theorem	bj-1uplth 32995	The characteristic property of monuples. Note that this holds without sethood hypotheses. (Contributed by BJ, 6-Apr-2019.)
|- ((| A|) = (| B|) <-> A = B )
Theorem	bj-1uplex 32996	A monuple is a set if and only if its coordinates are sets. (Contributed by BJ, 6-Apr-2019.)
|- ((| A|) e. _V <-> A e. _V )
Theorem	bj-1upln0 32997	A monuple is nonempty. (Contributed by BJ, 6-Apr-2019.)
|- (| A|) =/= (/)
Syntax	bj-c2uple 32998	Syntax for Morse couple. (Contributed by BJ, 6-Oct-2018.)
class (| A, B|)
Definition	df-bj-2upl 32999	Definition of the Morse couple. See df-bj-1upl 32986. New usage is discouraged because the precise definition is generally unimportant compared to the characteristic properties bj-2upleq 33000, bj-2uplth 33009, bj-2uplex 33010, and the properties of the projections (see df-bj-pr1 32989 and df-bj-pr2 33003). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.)
|- (| A, B|) = ((| A|) u. ( { 1o } X. tag B ) )
Theorem	bj-2upleq 33000	Substitution property for (| - , - |). (Contributed by BJ, 6-Oct-2018.)
|- ( A = B -> ( C = D -> (| A, C|) = (| B, D|) ) )