P. 349 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 34801-34900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bj-ceqsalg 34801*	Remove from ceqsalg 3059 dependency on ax-ext 2360 (and on df-cleq 2374 and df-v 3036). See also bj-ceqsalgv 34803. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
|- F/ x ps   &    |- ( x = A -> ( ph <-> ps ) )   =>    |- ( A e. V -> ( A. x ( x = A -> ph ) <-> ps ) )
Theorem	bj-ceqsalgALT 34802*	Alternate proof of bj-ceqsalg 34801. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ x ps   &    |- ( x = A -> ( ph <-> ps ) )   =>    |- ( A e. V -> ( A. x ( x = A -> ph ) <-> ps ) )
Theorem	bj-ceqsalgv 34803*	Version of bj-ceqsalg 34801 with a dv condition on x , V, removing dependency on df-sb 1748 and df-clab 2368. Prefer its use over bj-ceqsalg 34801 when sufficient (in particular when V is substituted for _V). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
|- F/ x ps   &    |- ( x = A -> ( ph <-> ps ) )   =>    |- ( A e. V -> ( A. x ( x = A -> ph ) <-> ps ) )
Theorem	bj-ceqsalgvALT 34804*	Alternate proof of bj-ceqsalgv 34803. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ x ps   &    |- ( x = A -> ( ph <-> ps ) )   =>    |- ( A e. V -> ( A. x ( x = A -> ph ) <-> ps ) )
Theorem	bj-ceqsal 34805*	Remove from ceqsal 3061 dependency on ax-ext 2360 (and on df-cleq 2374, df-v 3036, df-clab 2368, df-sb 1748). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
|- F/ x ps   &    |- A e. _V   &    |- ( x = A -> ( ph <-> ps ) )   =>    |- ( A. x ( x = A -> ph ) <-> ps )
Theorem	bj-ceqsalv 34806*	Remove from ceqsalv 3062 dependency on ax-ext 2360 (and on df-cleq 2374, df-v 3036, df-clab 2368, df-sb 1748). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
|- A e. _V   &    |- ( x = A -> ( ph <-> ps ) )   =>    |- ( A. x ( x = A -> ph ) <-> ps )
21.29.5.3  The class-form not-free predicate In this section, we prove the symmetry of the class-form not-free predicate.
Theorem	bj-nfcsym 34807	The class-form not-free predicate defines a symmetric binary relation on var metavariables (irreflexivity is proved by nfnid 4591 with additional axioms; see also nfcv 2544). This could be proved from aecom 2057 and nfcvb 4592 but the latter requires a domain with at least two objects (hence uses extra axioms). (Contributed by BJ, 30-Sep-2018.) Proof modification is discouraged to avoid use of eqcomd 2390 instead of bj-equcomd 34581; removing dependency on ax-ext 2360 is possible: prove weak versions (i.e. replace classes with setvars) of drnfc1 2563, eleq2d 2452 (using elequ2 1831), nfcvf 2569, dvelimc 2568, dvelimdc 2567, nfcvf2 2570. (Proof modification is discouraged.)
|- ( F/_ x y <-> F/_ y x )
21.29.5.4  Proposal for the definitions of class membership and class equality In this section, we show (bj-ax8 34808 and bj-ax9 34811) that the current forms of the definitions of class membership (df-clel 2377) and class equality (df-cleq 2374) are too powerful, and we propose alternate definitions (bj-df-clel 34809 and bj-df-cleq 34812) which also have the advantage of making it clear that these definitions are conservative.
Theorem	bj-ax8 34808	Proof of ax-8 1828 from df-clel 2377 (and FOL). This shows that df-clel 2377 is "too powerful". A possible definition is given by bj-df-clel 34809. (Contributed by BJ, 27-Jun-2019.) (Proof modification is discouraged.)
|- ( x = y -> ( x e. z -> y e. z ) )
Theorem	bj-df-clel 34809*	Candidate definition for df-clel 2377 (the need for it is exposed in bj-ax8 34808). The similarity of the hypothesis and the conclusion makes it clear that this definition merely extends to class variables something that is true for setvar variables, hence is conservative. This definition should be directly referenced only by bj-dfclel 34810, which should be used instead. The proof is irrelevant since this is a proposal for an axiom. Note: the current definition df-clel 2377 already mentions cleljust 2113 as a justification; here, we merely propose to put it as a hypothesis to make things clearer. (Contributed by BJ, 27-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( y e. z <-> E. x ( x = y /\ x e. z ) )   =>    |- ( A e. B <-> E. x ( x = A /\ x e. B ) )
Theorem	bj-dfclel 34810*	Characterization of the elements of a class. (Contributed by BJ, 27-Jun-2019.) (Proof modification is discouraged.)
|- ( A e. B <-> E. x ( x = A /\ x e. B ) )
Theorem	bj-ax9 34811*	Proof of ax-9 1830 from ax-ext 2360 and df-cleq 2374 (and FOL). This shows that df-cleq 2374 is "too powerful". A possible definition is given by bj-df-cleq 34812. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
|- ( x = y -> ( z e. x -> z e. y ) )
Theorem	bj-df-cleq 34812*	Candidate definition for df-cleq 2374 (the need for it is exposed in bj-ax9 34811). The similarity of the hypothesis and the conclusion makes it clear that this definition merely extends to class variables something that is true for setvar variables, hence is conservative. This definition should be directly referenced only by bj-dfcleq 34813, which should be used instead. The proof is irrelevant since this is a proposal for an axiom. Another definition, which would give finer control, is actually the pair of definitions where each has one implication of the present biconditional as hypothesis and conclusion. They assert that extensionality (respectively, the left-substitution axiom for the membership predicate) extends from setvars to classes. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( y = z <-> A. x ( x e. y <-> x e. z ) )   =>    |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
Theorem	bj-dfcleq 34813*	Proof of class extensionality from the axiom of set extensionality (ax-ext 2360) and the definition of class equality (bj-df-cleq 34812). (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
|- ( A = B <-> A. x ( x e. A <-> x e. B ) )
21.29.5.5  Lemmas for class substitution Some useful theorems for dealing with substitutions: sbbi 2146, sbcbig 3297, sbcel1g 3754, sbcel2 3756, sbcel12 3750, sbceqg 3751, csbvarg 3770.
Theorem	bj-sbeqALT 34814*	Substitution in an equality (use the more genereal version bj-sbeq 34815 instead, without disjoint variable condition). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( [ y / x ] A = B <-> [_ y / x ]_ A = [_ y / x ]_ B )
Theorem	bj-sbeq 34815	Distribute proper substitution through an equality relation. (See sbceqg 3751). (Contributed by BJ, 6-Oct-2018.)
|- ( [ y / x ] A = B <-> [_ y / x ]_ A = [_ y / x ]_ B )
Theorem	bj-sbceqgALT 34816	Distribute proper substitution through an equality relation. Alternate proof of sbceqg 3751. (Contributed by BJ, 6-Oct-2018.) Proof modification is discouraged to avoid using sbceqg 3751, but "minimize */except sbceqg" is ok. (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A e. V -> ( [. A / x ]. B = C <-> [_ A / x ]_ B = [_ A / x ]_ C ) )
Theorem	bj-csbsnlem 34817*	Lemma for bj-csbsn 34818 (in this lemma, x cannot occur in A). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.)
|- [_ A / x ]_ { x } = { A }
Theorem	bj-csbsn 34818	Substitution in a singleton. (Contributed by BJ, 6-Oct-2018.)
|- [_ A / x ]_ { x } = { A }
Theorem	bj-sbel1 34819*	Version of sbcel1g 3754 when substituting a set. (Note: one could have a corresponding version of sbcel12 3750 when substituting a set, but the point here is that the antecedent of sbcel1g 3754 is not needed when substituting a set.) (Contributed by BJ, 6-Oct-2018.)
|- ( [ y / x ] A e. B <-> [_ y / x ]_ A e. B )
Theorem	bj-abtru 34820	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-abfal 34821	The class of sets verifying a falsity is the empty set (closed form of abf 3746). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.)
|- ( A. x -. ph -> { x | ph } = (/) )
Theorem	bj-abf 34822	Shorter proof of abf 3746 (which should be kept as abfALT). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.)
|- -. ph   =>    |- { x | ph } = (/)
Theorem	bj-csbprc 34823	More direct proof of csbprc 3748 (fewer essential steps). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.)
|- ( -. A e. _V -> [_ A / x ]_ B = (/) )
21.29.5.6  Removing some dv conditions
Theorem	bj-exlimmpi 34824	Lemma for bj-vtoclg1f1 34829 (an instance of this lemma is a version of bj-vtoclg1f1 34829 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 34825	Lemma for theorems of the vtoclg 3092 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 34826	Lemma for theorems of the vtoclg 3092 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 34827*	Remove dependency on ax-ext 2360, df-clab 2368 and df-cleq 2374 (and df-sb 1748 and df-v 3036) from vtoclf 3085. (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 34828*	Remove dependency on ax-ext 2360, df-clab 2368 and df-cleq 2374 (and df-sb 1748 and df-v 3036) from vtocl 3086. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.)
|- A e. V   &    |- ( x = A -> ( ph <-> ps ) )   &    |- ph   =>    |- ps
Theorem	bj-vtoclg1f1 34829*	The FOL content of vtoclg1f 3091 (hence not using ax-ext 2360, df-cleq 2374, df-nfc 2532, df-v 3036). 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 2360; as a byproduct, this dispenses with ax-11 1850 and ax-13 2006). (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 34830*	Reprove vtoclg1f 3091 from bj-vtoclg1f1 34829. This removes dependency on ax-ext 2360, df-cleq 2374 and df-v 3036. Use bj-vtoclg1fv 34831 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 34831*	Version of bj-vtoclg1f 34830 with a dv condition on x , V. This removes dependency on df-sb 1748 and df-clab 2368. Prefer its use over bj-vtoclg1f 34830 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 34832	Version of rabbidva2 3024 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 34833	Version of rabbidva 3025 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 34834	Version of rabbidv 3026 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 34835	Deduction form of rabeq 3028. Note that contrary to rabeq 3028 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 34836	Version of rabeqbidv 3029 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 34837	Version of rabeqbidva 3030 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 34838*	Version of seex 4756 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 34839*	Version of df-nfc 2532 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 34840*	Remove dependency on ax-13 2006, ax-ext 2360, df-cleq 2374 and df-clel 2377 from axsep2 4489 while shortening its proof. Remark: the comment in zfauscl 4490 is misleading: the essential use of ax-ext 2360 is the one via eleq2 2455 and not the one via vtocl 3086, since the latter can be proved without ax-ext 2360 (see bj-vtocl 34828). (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 34841*	Generalization of unrab 3694. 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 34842	Generalization of inrab 3695. (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 34843	Shorter proof of inrab 3695. (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 34844*	Generalization of dfrab3ss 3701, 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 34845*	Restricted class abstraction with true formula. (Contributed by BJ, 22-Apr-2019.)
|- { x e. A | T. } = A
Theorem	bj-rabtrALT 34846*	Alternate proof of bj-rabtr 34845. (Contributed by BJ, 22-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- { x e. A | T. } = A
Theorem	bj-rabtrAUTO 34847*	Proof of bj-rabtr 34845 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 34848) and then two versions (bj-ru1 34849 and bj-ru 34850). Special attention is put on minimizing axiom depencencies.
Theorem	bj-ru0 34848*	The FOL part of Russell's paradox ru 3251 (see also bj-ru1 34849, bj-ru 34850). Use of elequ1 1829, bj-elequ12 34586, bj-spvv 34631 (instead of eleq1 2454, eleq12d 2464, spv 2018 as in ru 3251) permits to remove dependency on ax-11 1850, ax-13 2006, ax-ext 2360, df-sb 1748, df-clab 2368, df-cleq 2374, df-clel 2377. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
|- -. A. x ( x e. y <-> -. x e. x )
Theorem	bj-ru1 34849*	A version of Russell's paradox ru 3251 (see also bj-ru 34850). Note the more economical use of bj-abeq2 34706 instead of abeq2 2506 to avoid dependency on ax-13 2006. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
|- -. E. y y = { x | -. x e. x }
Theorem	bj-ru 34850	Remove dependency on ax-13 2006 (and df-v 3036) from Russell's paradox ru 3251 expressed with primitive symbols and with a class variable V. Note the more economical use of bj-elissetv 34784 instead of isset 3038 to avoid use of df-v 3036. (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 34851*	Inference associated with n0 3721. (Minimizes three statements by a total of 29 bytes.) (Contributed by BJ, 22-Apr-2019.)
|- A =/= (/)   =>    |- E. x x e. A
Theorem	bj-nel0 34852*	From the general negation of membership in A, infer that A is the empty set. [Could shorten 0xp 4994?] (Contributed by BJ, 6-Oct-2018.)
|- -. x e. A   =>    |- A = (/)
Theorem	bj-disjcsn 34853	A class is disjoint from its singleton. A consequence of regularity. Shorter proof than bnj521 34139. (Contributed by BJ, 4-Apr-2019.)
|- ( A i^i { A } ) = (/)
Theorem	bj-disjsn01 34854	Disjointness of the singletons containing 0 and 1. This is a consequence of bj-disjcsn 34853 but the present proof does not use regularity. (Contributed by BJ, 4-Apr-2019.) (Proof modification is discouraged.)
|- ( { (/) } i^i { 1o } ) = (/)
Theorem	bj-1ex 34855	1o is a set. (Contributed by BJ, 6-Apr-2019.)
|- 1o e. _V
Theorem	bj-2ex 34856	2o is a set. (Contributed by BJ, 6-Apr-2019.)
|- 2o e. _V
Theorem	bj-0nel1 34857	The empty set does not belong to { 1o }. (Contributed by BJ, 6-Apr-2019.)
|- (/) e/ { 1o }
Theorem	bj-1nel0 34858	1o does not belong to { (/) }. (Contributed by BJ, 6-Apr-2019.)
|- 1o e/ { (/) }
Theorem	bj-disjdif 34859	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 34860	The image of a singleton, general case. [Change and relabel xpimasn 5362 accordingly, maybe to xpima2sn.] (Contributed by BJ, 6-Apr-2019.)
|- ( ( A X. B ) " { X } ) = if ( X e. A , B , (/) )
Theorem	bj-xpima1sn 34861	The image of a singleton by a direct product, empty case. [Change and relabel xpimasn 5362 accordingly, maybe to xpima2sn.] (Contributed by BJ, 6-Apr-2019.)
|- ( X e/ A -> ( ( A X. B ) " { X } ) = (/) )
Theorem	bj-xpima1snALT 34862	Alternate proof of bj-xpima1sn 34861. (Contributed by BJ, 6-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( X e/ A -> ( ( A X. B ) " { X } ) = (/) )
Theorem	bj-xpima2sn 34863	The image of a singleton by a direct product, nonempty case. [To replace xpimasn 5362] (Contributed by BJ, 6-Apr-2019.) (Proof modification is discouraged.)
|- ( X e. A -> ( ( A X. B ) " { X } ) = B )
Theorem	bj-xpnzex 34864	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 6641 (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 34865	Exported form (curried form) of xpexg 6501. (Contributed by BJ, 2-Apr-2019.)
|- ( A e. V -> ( B e. W -> ( A X. B ) e. _V ) )
Theorem	bj-xpnzexb 34866	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 34867*	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 34868*	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 34869*	The class of sets "whose singletons" belong to a set is a set. Nice application of ax-rep 4478. (Contributed by BJ, 6-Oct-2018.)
|- ( A e. V -> { x | { x } e. A } e. _V )
Theorem	bj-clex 34870*	Sethood of certain classes. (Contributed by BJ, 2-Apr-2019.)
|- ( A e. V -> { x | { x } e. ( A " B ) } e. _V )
Syntax	bj-csngl 34871	Syntax for singletonization. (Contributed by BJ, 6-Oct-2018.)
class sngl A
Definition	df-bj-sngl 34872*	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 34873	Substitution property for sngl. (Contributed by BJ, 6-Oct-2018.)
|- ( A = B -> sngl A = sngl B )
Theorem	bj-elsngl 34874*	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 34875	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 34876	The singletonization of a class is included in its powerclass. (Contributed by BJ, 6-Oct-2018.)
|- sngl A C_ ~P A
Theorem	bj-0nelsngl 34877	The empty set is not a member of a singletonization (neither is any nonsingleton, in particular any von Neuman ordinal except possibly df-1o 7048). (Contributed by BJ, 6-Oct-2018.)
|- (/) e/ sngl A
Theorem	bj-snglinv 34878*	Inverse of singletonization. (Contributed by BJ, 6-Oct-2018.)
|- A = { x | { x } e. sngl A }
Theorem	bj-snglex 34879	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 34880	Syntax for the tagged copy of a class. (Contributed by BJ, 6-Oct-2018.)
class tag A
Definition	df-bj-tag 34881	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 34882	Substitution property for tag. (Contributed by BJ, 6-Oct-2018.)
|- ( A = B -> tag A = tag B )
Theorem	bj-eltag 34883*	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 34884	The empty set belongs to the tagging of a class. (Contributed by BJ, 6-Apr-2019.)
|- (/) e. tag A
Theorem	bj-tagn0 34885	The tagging of a class is nonempty. (Contributed by BJ, 6-Apr-2019.)
|- tag A =/= (/)
Theorem	bj-tagss 34886	The tagging of a class is included in its powerclass. (Contributed by BJ, 6-Oct-2018.)
|- tag A C_ ~P A
Theorem	bj-snglsstag 34887	The singletonization is included in the tagging. (Contributed by BJ, 6-Oct-2018.)
|- sngl A C_ tag A
Theorem	bj-sngltagi 34888	The singletonization is included in the tagging. (Contributed by BJ, 6-Oct-2018.)
|- ( A e. sngl B -> A e. tag B )
Theorem	bj-sngltag 34889	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 34890	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 34891	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 34892*	Inverse of tagging. (Contributed by BJ, 6-Oct-2018.)
|- A = { x | { x } e. tag A }
Theorem	bj-tagex 34893	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 34894	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 34895	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 34927 and bj-2uplex 34928 (but more importantly, bj-pr21val 34919 and bj-pr22val 34925). 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 3951) as a preliminary definition, and then "redefines" a couple. It could also use the "short" version of the Kuratowski pair (see opthreg 7949) 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 4961, but here we use "tagged versions" of the factors (see df-bj-tag 34881) 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 34896	Syntax for the class projection. (Contributed by BJ, 6-Apr-2019.)
class ( A Proj B )
Definition	df-bj-proj 34897*	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 34898	Substitution property for Proj. (Contributed by BJ, 6-Apr-2019.)
|- ( A = C -> ( B = D -> ( A Proj B ) = ( C Proj D ) ) )
Theorem	bj-projeq2 34899	Substitution property for Proj. (Contributed by BJ, 6-Apr-2019.)
|- ( B = C -> ( A Proj B ) = ( A Proj C ) )
Theorem	bj-projun 34900	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 ) )