P. 347 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 34601-34700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bj-exlimmpbir 34601	Lemma for theorems of the vtoclg 3167 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 34602*	Remove dependency on ax-ext 2435, df-clab 2443 and df-cleq 2449 (and df-sb 1741 and df-v 3111) from vtoclf 3160. (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 34603*	Remove dependency on ax-ext 2435, df-clab 2443 and df-cleq 2449 (and df-sb 1741 and df-v 3111) from vtocl 3161. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.)
|- A e. V   &    |- ( x = A -> ( ph <-> ps ) )   &    |- ph   =>    |- ps
Theorem	bj-vtoclg1f1 34604*	The FOL content of vtoclg1f 3166 (hence not using ax-ext 2435, df-cleq 2449, df-nfc 2607, df-v 3111). 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 2435; as a byproduct, this dispenses with ax-11 1843 and ax-13 2000). (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 34605*	Reprove vtoclg1f 3166 from bj-vtoclg1f1 34604. This removes dependency on ax-ext 2435, df-cleq 2449 and df-v 3111. Use bj-vtoclg1fv 34606 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 34606*	Version of bj-vtoclg1f 34605 with a dv condition on x , V. This removes dependency on df-sb 1741 and df-clab 2443. Prefer its use over bj-vtoclg1f 34605 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 34607	Version of rabbidva2 3099 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 34608	Version of rabbidva 3100 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 34609	Version of rabbidv 3101 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 34610	Deduction form of rabeq 3103. Note that contrary to rabeq 3103 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 34611	Version of rabeqbidv 3104 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 34612	Version of rabeqbidva 3105 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 34613*	Version of seex 4851 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 34614*	Version of df-nfc 2607 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 34615*	Remove dependency on ax-13 2000, ax-ext 2435, df-cleq 2449 and df-clel 2452 from axsep2 4579 while shortening its proof. Remark: the comment in zfauscl 4580 is misleading: the essential use of ax-ext 2435 is the one via eleq2 2530 and not the one via vtocl 3161, since the latter can be proved without ax-ext 2435 (see bj-vtocl 34603). (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.)
|- E. y A. x ( x e. y <-> ( x e. z /\ ph ) )
21.29.5.7  Class abstractions A few additional theorems on class abstractions and restricted class abstractions.
Theorem	bj-unrab 34616*	Generalization of unrab 3776. 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 34617	Generalization of inrab 3777. (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 34618	Shorter proof of inrab 3777. (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-rabtr 34619*	Restricted class abstraction with true formula. (Contributed by BJ, 22-Apr-2019.)
|- { x e. A | T. } = A
Theorem	bj-rabtrALT 34620*	Alternate proof of bj-rabtr 34619. (Contributed by BJ, 22-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- { x e. A | T. } = A
Theorem	bj-rabtrAUTO 34621*	Proof of bj-rabtr 34619 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
21.29.5.8  Russell's paradox A few results around Russell's paradox. For clarity, we prove separately its FOL part (bj-ru0 34622) and then two versions (bj-ru1 34623 and bj-ru 34624). Special attention is put on minimizing axiom depencencies.
Theorem	bj-ru0 34622*	The FOL part of Russell's paradox ru 3326 (see also bj-ru1 34623, bj-ru 34624). Use of elequ1 1822, bj-elequ12 34361, bj-spvv 34406 (instead of eleq1 2529, eleq12d 2539, spv 2012 as in ru 3326) permits to remove dependency on ax-11 1843, ax-13 2000, ax-ext 2435, df-sb 1741, df-clab 2443, df-cleq 2449, df-clel 2452. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
|- -. A. x ( x e. y <-> -. x e. x )
Theorem	bj-ru1 34623*	A version of Russell's paradox ru 3326 (see also bj-ru 34624). Note the more economical use of bj-abeq2 34481 instead of abeq2 2581 to avoid dependency on ax-13 2000. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
|- -. E. y y = { x | -. x e. x }
Theorem	bj-ru 34624	Remove dependency on ax-13 2000 (and df-v 3111) from Russell's paradox ru 3326 expressed with primitive symbols and with a class variable V. Note the more economical use of bj-elissetv 34559 instead of isset 3113 to avoid use of df-v 3111. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
|- -. { x | -. x e. x } e. V
21.29.5.9  Some disjointness results A few utility theorems on disjointness of classes.
Theorem	bj-n0i 34625*	Inference associated with n0 3803. (Minimizes three statements by a total of 29 bytes.) (Contributed by BJ, 22-Apr-2019.)
|- A =/= (/)   =>    |- E. x x e. A
Theorem	bj-nel0 34626*	From the general negation of membership in A, infer that A is the empty set. [Could shorten 0xp 5089?] (Contributed by BJ, 6-Oct-2018.)
|- -. x e. A   =>    |- A = (/)
Theorem	bj-disjcsn 34627	A class is disjoint from its singleton. A consequence of regularity. Shorter proof than bnj521 33914. (Contributed by BJ, 4-Apr-2019.)
|- ( A i^i { A } ) = (/)
Theorem	bj-disjsn01 34628	Disjointness of the singletons containing 0 and 1. This is a consequence of bj-disjcsn 34627 but the present proof does not use regularity. (Contributed by BJ, 4-Apr-2019.) (Proof modification is discouraged.)
|- ( { (/) } i^i { 1o } ) = (/)
Theorem	bj-1ex 34629	1o is a set. (Contributed by BJ, 6-Apr-2019.)
|- 1o e. _V
Theorem	bj-2ex 34630	2o is a set. (Contributed by BJ, 6-Apr-2019.)
|- 2o e. _V
Theorem	bj-0nel1 34631	The empty set does not belong to { 1o }. (Contributed by BJ, 6-Apr-2019.)
|- (/) e/ { 1o }
Theorem	bj-1nel0 34632	1o does not belong to { (/) }. (Contributed by BJ, 6-Apr-2019.)
|- 1o e/ { (/) }
Theorem	bj-disjdif 34633	The difference of a class and a class disjoint from it is the original class. (Contributed by BJ, 21-Apr-2019.)
|- ( ( A i^i B ) = (/) -> ( A \ B ) = A )
21.29.5.10  Complements on direct products A few utility theorems on direct products.
Theorem	bj-xpimasn 34634	The image of a singleton, general case. [Change and relabel xpimasn 5459 accordingly, maybe to xpima2sn.] (Contributed by BJ, 6-Apr-2019.)
|- ( ( A X. B ) " { X } ) = if ( X e. A , B , (/) )
Theorem	bj-xpima1sn 34635	The image of a singleton by a direct product, empty case. [Change and relabel xpimasn 5459 accordingly, maybe to xpima2sn.] (Contributed by BJ, 6-Apr-2019.)
|- ( X e/ A -> ( ( A X. B ) " { X } ) = (/) )
Theorem	bj-xpima1snALT 34636	Alternate proof of bj-xpima1sn 34635. (Contributed by BJ, 6-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( X e/ A -> ( ( A X. B ) " { X } ) = (/) )
Theorem	bj-xpima2sn 34637	The image of a singleton by a direct product, nonempty case. [To replace xpimasn 5459] (Contributed by BJ, 6-Apr-2019.) (Proof modification is discouraged.)
|- ( X e. A -> ( ( A X. B ) " { X } ) = B )
Theorem	bj-xpnzex 34638	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 exported form (curried form) of xpexcnv 6741 (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 34639	Exported form (curried form) of xpexg 6601. (Contributed by BJ, 2-Apr-2019.)
|- ( A e. V -> ( B e. W -> ( A X. B ) e. _V ) )
Theorem	bj-xpnzexb 34640	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 34641*	Substitution property for certain classes. (Contributed by BJ, 2-Apr-2019.)
|- ( A = B -> { x | { x } e. ( A " C ) } = { x | { x } e. ( B " C ) } )
21.29.5.11  "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 34642*	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 34643*	The class of sets "whose singletons" belong to a set is a set. Nice application of ax-rep 4568. (Contributed by BJ, 6-Oct-2018.)
|- ( A e. V -> { x | { x } e. A } e. _V )
Theorem	bj-clex 34644*	Sethood of certain classes. (Contributed by BJ, 2-Apr-2019.)
|- ( A e. V -> { x | { x } e. ( A " B ) } e. _V )
Syntax	bj-csngl 34645	Syntax for singletonization. (Contributed by BJ, 6-Oct-2018.)
class sngl A
Definition	df-bj-sngl 34646*	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 34647	Substitution property for sngl. (Contributed by BJ, 6-Oct-2018.)
|- ( A = B -> sngl A = sngl B )
Theorem	bj-elsngl 34648*	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 34649	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 34650	The singletonization of a class is included in its powerclass. (Contributed by BJ, 6-Oct-2018.)
|- sngl A C_ ~P A
Theorem	bj-0nelsngl 34651	The empty set is not a member of a singletonization (neither is any nonsingleton, in particular any von Neuman ordinal except possibly df-1o 7148). (Contributed by BJ, 6-Oct-2018.)
|- (/) e/ sngl A
Theorem	bj-snglinv 34652*	Inverse of singletonization. (Contributed by BJ, 6-Oct-2018.)
|- A = { x | { x } e. sngl A }
Theorem	bj-snglex 34653	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 34654	Syntax for the tagged copy of a class. (Contributed by BJ, 6-Oct-2018.)
class tag A
Definition	df-bj-tag 34655	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 34656	Substitution property for tag. (Contributed by BJ, 6-Oct-2018.)
|- ( A = B -> tag A = tag B )
Theorem	bj-eltag 34657*	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 34658	The empty set belongs to the tagging of a class. (Contributed by BJ, 6-Apr-2019.)
|- (/) e. tag A
Theorem	bj-tagn0 34659	The tagging of a class is nonempty. (Contributed by BJ, 6-Apr-2019.)
|- tag A =/= (/)
Theorem	bj-tagss 34660	The tagging of a class is included in its powerclass. (Contributed by BJ, 6-Oct-2018.)
|- tag A C_ ~P A
Theorem	bj-snglsstag 34661	The singletonization is included in the tagging. (Contributed by BJ, 6-Oct-2018.)
|- sngl A C_ tag A
Theorem	bj-sngltagi 34662	The singletonization is included in the tagging. (Contributed by BJ, 6-Oct-2018.)
|- ( A e. sngl B -> A e. tag B )
Theorem	bj-sngltag 34663	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 34664	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 34665	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 34666*	Inverse of tagging. (Contributed by BJ, 6-Oct-2018.)
|- A = { x | { x } e. tag A }
Theorem	bj-tagex 34667	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 34668	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 34669	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 ) )
21.29.5.12  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 34701 and bj-2uplex 34702 (but more importantly, bj-pr21val 34693 and bj-pr22val 34699). 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 4039) as a preliminary definition, and then "redefines" a couple. It could also use the "short" version of the Kuratowski pair (see opthreg 8052) 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 5056, but here we use "tagged versions" of the factors (see df-bj-tag 34655) 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 34670	Syntax for the class projection. (Contributed by BJ, 6-Apr-2019.)
class ( A Proj B )
Definition	df-bj-proj 34671*	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 34672	Substitution property for Proj. (Contributed by BJ, 6-Apr-2019.)
|- ( A = C -> ( B = D -> ( A Proj B ) = ( C Proj D ) ) )
Theorem	bj-projeq2 34673	Substitution property for Proj. (Contributed by BJ, 6-Apr-2019.)
|- ( B = C -> ( A Proj B ) = ( A Proj C ) )
Theorem	bj-projun 34674	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 34675	Sethood of the class projection. (Contributed by BJ, 6-Apr-2019.)
|- ( B e. V -> ( A Proj B ) e. _V )
Theorem	bj-projval 34676	Value of the class projection (proof can be shortened by 19 bytes by using sylancl3 34291). (Contributed by BJ, 6-Apr-2019.)
|- ( A e. V -> ( A Proj ( { B } X. tag C ) ) = if ( B = A , C , (/) ) )
Syntax	bj-c1upl 34677	Syntax for Morse monuple. (Contributed by BJ, 6-Apr-2019.)
class (| A|)
Definition	df-bj-1upl 34678	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 34692, bj-2uplth 34701, bj-2uplex 34702, and the properties of the projections (see df-bj-pr1 34681 and df-bj-pr2 34695). (Contributed by BJ, 6-Apr-2019.) (New usage is discouraged.)
|- (| A|) = ( { (/) } X. tag A )
Theorem	bj-1upleq 34679	Substitution property for (| - |). (Contributed by BJ, 6-Apr-2019.)
|- ( A = B -> (| A|) = (| B|) )
Syntax	bj-cpr1 34680	Syntax for the first class tuple projection. (Contributed by BJ, 6-Apr-2019.)
class pr1 A
Definition	df-bj-pr1 34681	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 34682, bj-pr11val 34685, bj-pr21val 34693, bj-pr1ex 34686. (Contributed by BJ, 6-Apr-2019.) (New usage is discouraged.)
|- pr1 A = ( (/) Proj A )
Theorem	bj-pr1eq 34682	Substitution property for pr1. (Contributed by BJ, 6-Apr-2019.)
|- ( A = B -> pr1 A = pr1 B )
Theorem	bj-pr1un 34683	The first projection preserves unions. (Contributed by BJ, 6-Apr-2019.)
|- pr1 ( A u. B ) = (pr1 A u. pr1 B )
Theorem	bj-pr1val 34684	Value of the first projection. (Contributed by BJ, 6-Apr-2019.)
|- pr1 ( { A } X. tag B ) = if ( A = (/) , B , (/) )
Theorem	bj-pr11val 34685	Value of the first projection of a monuple. (Contributed by BJ, 6-Apr-2019.)
|- pr1 (| A|) = A
Theorem	bj-pr1ex 34686	Sethood of the first projection. (Contributed by BJ, 6-Oct-2018.)
|- ( A e. V -> pr1 A e. _V )
Theorem	bj-1uplth 34687	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 34688	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 34689	A monuple is nonempty. (Contributed by BJ, 6-Apr-2019.)
|- (| A|) =/= (/)
Syntax	bj-c2uple 34690	Syntax for Morse couple. (Contributed by BJ, 6-Oct-2018.)
class (| A, B|)
Definition	df-bj-2upl 34691	Definition of the Morse couple. See df-bj-1upl 34678. New usage is discouraged because the precise definition is generally unimportant compared to the characteristic properties bj-2upleq 34692, bj-2uplth 34701, bj-2uplex 34702, and the properties of the projections (see df-bj-pr1 34681 and df-bj-pr2 34695). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.)
|- (| A, B|) = ((| A|) u. ( { 1o } X. tag B ) )
Theorem	bj-2upleq 34692	Substitution property for (| - , - |). (Contributed by BJ, 6-Oct-2018.)
|- ( A = B -> ( C = D -> (| A, C|) = (| B, D|) ) )
Theorem	bj-pr21val 34693	Value of the first projection of a couple. (Contributed by BJ, 6-Oct-2018.)
|- pr1 (| A, B|) = A
Syntax	bj-cpr2 34694	Syntax for the second class tuple projection. (Contributed by BJ, 6-Oct-2018.)
class pr2 A
Definition	df-bj-pr2 34695	Definition of the second projection of a class tuple. New usage is discouraged because the precise definition is generally unimportant compared to the characteristic properties bj-pr2eq 34696, bj-pr22val 34699, bj-pr2ex 34700. (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.)
|- pr2 A = ( 1o Proj A )
Theorem	bj-pr2eq 34696	Substitution property for pr2. (Contributed by BJ, 6-Oct-2018.)
|- ( A = B -> pr2 A = pr2 B )
Theorem	bj-pr2un 34697	The second projection preserves unions. (Contributed by BJ, 6-Apr-2019.)
|- pr2 ( A u. B ) = (pr2 A u. pr2 B )
Theorem	bj-pr2val 34698	Value of the second projection. (Contributed by BJ, 6-Apr-2019.)
|- pr2 ( { A } X. tag B ) = if ( A = 1o , B , (/) )
Theorem	bj-pr22val 34699	Value of the second projection of a couple. (Contributed by BJ, 6-Oct-2018.)
|- pr2 (| A, B|) = B
Theorem	bj-pr2ex 34700	Sethood of the second projection. (Contributed by BJ, 6-Oct-2018.)
|- ( A e. V -> pr2 A e. _V )