P. 370 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36901-37000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bj-vtoclg1fv 36901*	Version of bj-vtoclg1f 36900 with a disjoint variable condition on 𝑥, 𝑉. This removes dependency on df-sb 2062 and df-clab 2712. Prefer its use over bj-vtoclg1f 36900 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝜓)
Theorem	bj-vtoclg 36902*	A version of vtoclg 3553 with an additional disjoint variable condition (which is removable if we allow use of df-clab 2712, see bj-vtoclg1f 36900), which requires fewer axioms (i.e., removes dependency on ax-6 1964, ax-7 2004, ax-9 2115, ax-12 2174, ax-ext 2705, df-clab 2712, df-cleq 2726, df-v 3479). (Contributed by BJ, 2-Jul-2022.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝜓)
Theorem	bj-rabeqbid 36903	Version of rabeqbidv 3451 with two disjoint variable conditions removed and the third replaced by a nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})
Theorem	bj-seex 36904*	Version of seex 5647 with a disjoint variable condition replaced by a nonfreeness hypothesis (for the sake of illustration). (Contributed by BJ, 27-Apr-2019.)
⊢ Ⅎ𝑥𝐵    ⇒   ⊢ ((𝑅 Se 𝐴 ∧ 𝐵 ∈ 𝐴) → {𝑥 ∈ 𝐴 ∣ 𝑥𝑅𝐵} ∈ V)
Theorem	bj-nfcf 36905*	Version of df-nfc 2889 with a disjoint variable condition replaced with a nonfreeness hypothesis. (Contributed by BJ, 2-May-2019.)
⊢ Ⅎ𝑦𝐴    ⇒   ⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴)
Theorem	bj-zfauscl 36906*	General version of zfauscl 5303. Remark: the comment in zfauscl 5303 is misleading: the essential use of ax-ext 2705 is the one via eleq2 2827 and not the one via vtocl 3557, since the latter can be proved without ax-ext 2705 (see bj-vtoclg 36902). (Contributed by BJ, 2-Jul-2022.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑)))
21.19.5.7  Class abstractions A few additional theorems on class abstractions and restricted class abstractions.
Theorem	bj-elabd2ALT 36907*	Alternate proof of elabd2 3669 bypassing elab6g 3668 (and using sbiedvw 2092 instead of the ∀𝑥(𝑥 = 𝑦 → 𝜓) idiom). (Contributed by BJ, 16-Oct-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = {𝑥 ∣ 𝜓})    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝐴 ∈ 𝐵 ↔ 𝜒))
Theorem	bj-unrab 36908*	Generalization of unrab 4320. Equality need not hold. (Contributed by BJ, 21-Apr-2019.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐵 ∣ 𝜓}) ⊆ {𝑥 ∈ (𝐴 ∪ 𝐵) ∣ (𝜑 ∨ 𝜓)}
Theorem	bj-inrab 36909	Generalization of inrab 4321. (Contributed by BJ, 21-Apr-2019.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐵 ∣ 𝜓}) = {𝑥 ∈ (𝐴 ∩ 𝐵) ∣ (𝜑 ∧ 𝜓)}
Theorem	bj-inrab2 36910	Shorter proof of inrab 4321. (Contributed by BJ, 21-Apr-2019.) (Proof modification is discouraged.)
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)}
Theorem	bj-inrab3 36911*	Generalization of dfrab3ss 4328, which it may shorten. (Contributed by BJ, 21-Apr-2019.) (Revised by OpenAI, 7-Jul-2020.)
⊢ (𝐴 ∩ {𝑥 ∈ 𝐵 ∣ 𝜑}) = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ 𝐵)
Theorem	bj-rabtr 36912*	Restricted class abstraction with true formula. (Contributed by BJ, 22-Apr-2019.)
⊢ {𝑥 ∈ 𝐴 ∣ ⊤} = 𝐴
Theorem	bj-rabtrALT 36913*	Alternate proof of bj-rabtr 36912. (Contributed by BJ, 22-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ {𝑥 ∈ 𝐴 ∣ ⊤} = 𝐴
Theorem	bj-rabtrAUTO 36914*	Proof of bj-rabtr 36912 found automatically by the Metamath program "MM-PA> IMPROVE ALL / DEPTH 3 / 3" command followed by "MM-PA> MINIMIZE_WITH *". (Contributed by BJ, 22-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ {𝑥 ∈ 𝐴 ∣ ⊤} = 𝐴
21.19.5.8  Generalized class abstractions
Syntax	bj-cgab 36915	Syntax for generalized class abstractions.
class {𝐴 ∣ 𝑥 ∣ 𝜑}
Definition	df-bj-gab 36916*	Definition of generalized class abstractions: typically, 𝑥 is a bound variable in 𝐴 and 𝜑 and {𝐴 ∣ 𝑥 ∣ 𝜑} denotes "the class of 𝐴(𝑥)'s such that 𝜑(𝑥)". (Contributed by BJ, 4-Oct-2024.)
⊢ {𝐴 ∣ 𝑥 ∣ 𝜑} = {𝑦 ∣ ∃𝑥(𝐴 = 𝑦 ∧ 𝜑)}
Theorem	bj-gabss 36917	Inclusion of generalized class abstractions. (Contributed by BJ, 4-Oct-2024.)
⊢ (∀𝑥(𝐴 = 𝐵 ∧ (𝜑 → 𝜓)) → {𝐴 ∣ 𝑥 ∣ 𝜑} ⊆ {𝐵 ∣ 𝑥 ∣ 𝜓})
Theorem	bj-gabssd 36918	Inclusion of generalized class abstractions. Deduction form. (Contributed by BJ, 4-Oct-2024.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → {𝐴 ∣ 𝑥 ∣ 𝜓} ⊆ {𝐵 ∣ 𝑥 ∣ 𝜒})
Theorem	bj-gabeqd 36919	Equality of generalized class abstractions. Deduction form. (Contributed by BJ, 4-Oct-2024.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝐴 ∣ 𝑥 ∣ 𝜓} = {𝐵 ∣ 𝑥 ∣ 𝜒})
Theorem	bj-gabeqis 36920*	Equality of generalized class abstractions, with implicit substitution. (Contributed by BJ, 4-Oct-2024.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝐴 ∣ 𝑥 ∣ 𝜑} = {𝐵 ∣ 𝑦 ∣ 𝜓}
Theorem	bj-elgab 36921	Elements of a generalized class abstraction. (Contributed by BJ, 4-Oct-2024.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → (∃𝑥(𝐴 = 𝐵 ∧ 𝜓) ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝐴 ∈ {𝐵 ∣ 𝑥 ∣ 𝜓} ↔ 𝜒))
Theorem	bj-gabima 36922	Generalized class abstraction as a direct image. TODO: improve the support lemmas elimag 6083 and fvelima 6973 to nonfreeness hypothesis (and for the latter, biconditional). (Contributed by BJ, 4-Oct-2024.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → Ⅎ𝑥𝐹)    &   ⊢ (𝜑 → Fun 𝐹)    &   ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ dom 𝐹)    ⇒   ⊢ (𝜑 → {(𝐹‘𝑥) ∣ 𝑥 ∣ 𝜓} = (𝐹 “ {𝑥 ∣ 𝜓}))
21.19.5.9  Restricted nonfreeness In this subsection, we define restricted nonfreeness (or relative nonfreeness).
Syntax	wrnf 36923	Syntax for restricted nonfreeness.
wff Ⅎ𝑥 ∈ 𝐴𝜑
Definition	df-bj-rnf 36924	Definition of restricted nonfreeness. Informally, the proposition Ⅎ𝑥 ∈ 𝐴𝜑 means that 𝜑(𝑥) does not vary on 𝐴. (Contributed by BJ, 19-Mar-2021.)
⊢ (Ⅎ𝑥 ∈ 𝐴𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜑))
21.19.5.10  Russell's paradox A few results around Russell's paradox. For clarity, we prove separately a FOL statement (now in the main part as ru0 2124) and then two versions (bj-ru1 36925 and bj-ru 36926). Special attention is put on minimizing axiom depencencies.
Theorem	bj-ru1 36925*	A version of Russell's paradox ru 3788 not mentioning the universal class. (see also bj-ru 36926). (Contributed by BJ, 12-Oct-2019.) Remove usage of ax-10 2138, ax-11 2154, ax-12 2174 by using eqabbw 2812 following BTernaryTau's similar revision of ru 3788. (Revised by BJ, 28-Jun-2025.) (Proof modification is discouraged.)
⊢ ¬ ∃𝑦 𝑦 = {𝑥 ∣ ¬ 𝑥 ∈ 𝑥}
Theorem	bj-ru 36926	Remove dependency on ax-13 2374 (and df-v 3479) from Russell's paradox ru 3788 expressed with primitive symbols and with a class variable 𝑉. Note the more economical use of elissetv 2819 instead of isset 3491 to avoid use of df-v 3479. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ ¬ {𝑥 ∣ ¬ 𝑥 ∈ 𝑥} ∈ 𝑉
21.19.5.11  Curry's paradox in set theory
Theorem	currysetlem 36927*	Lemma for currysetlem 36927, where it is used with (𝑥 ∈ 𝑥 → 𝜑) substituted for 𝜓. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.)
⊢ ({𝑥 ∣ 𝜓} ∈ 𝑉 → ({𝑥 ∣ 𝜓} ∈ {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ↔ ({𝑥 ∣ 𝜓} ∈ {𝑥 ∣ 𝜓} → 𝜑)))
Theorem	curryset 36928*	Curry's paradox in set theory. This can be seen as a generalization of Russell's paradox, which corresponds to the case where 𝜑 is ⊥. See alternate exposal of basically the same proof currysetALT 36932. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.)
⊢ ¬ {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ∈ 𝑉
Theorem	currysetlem1 36929*	Lemma for currysetALT 36932. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.)
⊢ 𝑋 = {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)}    ⇒   ⊢ (𝑋 ∈ 𝑉 → (𝑋 ∈ 𝑋 ↔ (𝑋 ∈ 𝑋 → 𝜑)))
Theorem	currysetlem2 36930*	Lemma for currysetALT 36932. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.)
⊢ 𝑋 = {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)}    ⇒   ⊢ (𝑋 ∈ 𝑉 → (𝑋 ∈ 𝑋 → 𝜑))
Theorem	currysetlem3 36931*	Lemma for currysetALT 36932. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.)
⊢ 𝑋 = {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)}    ⇒   ⊢ ¬ 𝑋 ∈ 𝑉
Theorem	currysetALT 36932*	Alternate proof of curryset 36928, or more precisely alternate exposal of the same proof. (Contributed by BJ, 23-Sep-2023.) This proof is intuitionistically valid. (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ {𝑥 ∣ (𝑥 ∈ 𝑥 → 𝜑)} ∈ 𝑉
21.19.5.12  Some disjointness results A few utility theorems on disjointness of classes.
Theorem	bj-n0i 36933*	Inference associated with n0 4358. Shortens 2ndcdisj 23479 (2888>2878), notzfaus 5368 (264>253). (Contributed by BJ, 22-Apr-2019.)
⊢ 𝐴 ≠ ∅    ⇒   ⊢ ∃𝑥 𝑥 ∈ 𝐴
Theorem	bj-disjsn01 36934	Disjointness of the singletons containing 0 and 1. This is a consequence of disjcsn 9641 but the present proof does not use regularity. (Contributed by BJ, 4-Apr-2019.) (Proof modification is discouraged.)
⊢ ({∅} ∩ {1o}) = ∅
Theorem	bj-0nel1 36935	The empty set does not belong to {1o}. (Contributed by BJ, 6-Apr-2019.)
⊢ ∅ ∉ {1o}
Theorem	bj-1nel0 36936	1o does not belong to {∅}. (Contributed by BJ, 6-Apr-2019.)
⊢ 1o ∉ {∅}
21.19.5.13  Complements on direct products A few utility theorems on direct products.
Theorem	bj-xpimasn 36937	The image of a singleton, general case. [Change and relabel xpimasn 6206 accordingly, maybe to xpima2sn.] (Contributed by BJ, 6-Apr-2019.)
⊢ ((𝐴 × 𝐵) “ {𝑋}) = if(𝑋 ∈ 𝐴, 𝐵, ∅)
Theorem	bj-xpima1sn 36938	The image of a singleton by a direct product, empty case. [Change and relabel xpimasn 6206 accordingly, maybe to xpima2sn.] (Contributed by BJ, 6-Apr-2019.)
⊢ (¬ 𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = ∅)
Theorem	bj-xpima1snALT 36939	Alternate proof of bj-xpima1sn 36938. (Contributed by BJ, 6-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ 𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = ∅)
Theorem	bj-xpima2sn 36940	The image of a singleton by a direct product, nonempty case. [To replace xpimasn 6206.] (Contributed by BJ, 6-Apr-2019.) (Proof modification is discouraged.)
⊢ (𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = 𝐵)
Theorem	bj-xpnzex 36941	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 7942 (up to commutation in the product). (Contributed by BJ, 6-Oct-2018.) (Proof modification is discouraged.)
⊢ (𝐴 ≠ ∅ → ((𝐴 × 𝐵) ∈ 𝑉 → 𝐵 ∈ V))
Theorem	bj-xpexg2 36942	Curried (exported) form of xpexg 7768. (Contributed by BJ, 2-Apr-2019.)
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ 𝑊 → (𝐴 × 𝐵) ∈ V))
Theorem	bj-xpnzexb 36943	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.)
⊢ (𝐴 ∈ (𝑉 ∖ {∅}) → (𝐵 ∈ V ↔ (𝐴 × 𝐵) ∈ V))
Theorem	bj-cleq 36944*	Substitution property for certain classes. (Contributed by BJ, 2-Apr-2019.)
⊢ (𝐴 = 𝐵 → {𝑥 ∣ {𝑥} ∈ (𝐴 “ 𝐶)} = {𝑥 ∣ {𝑥} ∈ (𝐵 “ 𝐶)})
21.19.5.14  "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-snsetex 36945*	The class of sets "whose singletons" belong to a set is a set. Nice application of ax-rep 5284. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V)
Theorem	bj-clexab 36946*	Sethood of certain classes. (Contributed by BJ, 2-Apr-2019.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ {𝑥} ∈ (𝐴 “ 𝐵)} ∈ V)
Syntax	bj-csngl 36947	Syntax for singletonization. (Contributed by BJ, 6-Oct-2018.)
class sngl 𝐴
Definition	df-bj-sngl 36948*	Definition of "singletonization". The class sngl 𝐴 is isomorphic to 𝐴 and since it contains only singletons, it can be easily be adjoined disjoint elements, which can be useful in various constructions. (Contributed by BJ, 6-Oct-2018.)
⊢ sngl 𝐴 = {𝑥 ∣ ∃𝑦 ∈ 𝐴 𝑥 = {𝑦}}
Theorem	bj-sngleq 36949	Substitution property for sngl. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 = 𝐵 → sngl 𝐴 = sngl 𝐵)
Theorem	bj-elsngl 36950*	Characterization of the elements of the singletonization of a class. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ sngl 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 = {𝑥})
Theorem	bj-snglc 36951	Characterization of the elements of 𝐴 in terms of elements of its singletonization. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ sngl 𝐵)
Theorem	bj-snglss 36952	The singletonization of a class is included in its powerclass. (Contributed by BJ, 6-Oct-2018.)
⊢ sngl 𝐴 ⊆ 𝒫 𝐴
Theorem	bj-0nelsngl 36953	The empty set is not a member of a singletonization (neither is any nonsingleton, in particular any von Neuman ordinal except possibly df-1o 8504). (Contributed by BJ, 6-Oct-2018.)
⊢ ∅ ∉ sngl 𝐴
Theorem	bj-snglinv 36954*	Inverse of singletonization. (Contributed by BJ, 6-Oct-2018.)
⊢ 𝐴 = {𝑥 ∣ {𝑥} ∈ sngl 𝐴}
Theorem	bj-snglex 36955	A class is a set if and only if its singletonization is a set. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ V ↔ sngl 𝐴 ∈ V)
Syntax	bj-ctag 36956	Syntax for the tagged copy of a class. (Contributed by BJ, 6-Oct-2018.)
class tag 𝐴
Definition	df-bj-tag 36957	Definition of the tagged copy of a class, that is, the adjunction to (an isomorph of) 𝐴 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 𝐴 = (sngl 𝐴 ∪ {∅})
Theorem	bj-tageq 36958	Substitution property for tag. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 = 𝐵 → tag 𝐴 = tag 𝐵)
Theorem	bj-eltag 36959*	Characterization of the elements of the tagging of a class. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ tag 𝐵 ↔ (∃𝑥 ∈ 𝐵 𝐴 = {𝑥} ∨ 𝐴 = ∅))
Theorem	bj-0eltag 36960	The empty set belongs to the tagging of a class. (Contributed by BJ, 6-Apr-2019.)
⊢ ∅ ∈ tag 𝐴
Theorem	bj-tagn0 36961	The tagging of a class is nonempty. (Contributed by BJ, 6-Apr-2019.)
⊢ tag 𝐴 ≠ ∅
Theorem	bj-tagss 36962	The tagging of a class is included in its powerclass. (Contributed by BJ, 6-Oct-2018.)
⊢ tag 𝐴 ⊆ 𝒫 𝐴
Theorem	bj-snglsstag 36963	The singletonization is included in the tagging. (Contributed by BJ, 6-Oct-2018.)
⊢ sngl 𝐴 ⊆ tag 𝐴
Theorem	bj-sngltagi 36964	The singletonization is included in the tagging. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ sngl 𝐵 → 𝐴 ∈ tag 𝐵)
Theorem	bj-sngltag 36965	The singletonization and the tagging of a set contain the same singletons. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ 𝑉 → ({𝐴} ∈ sngl 𝐵 ↔ {𝐴} ∈ tag 𝐵))
Theorem	bj-tagci 36966	Characterization of the elements of 𝐵 in terms of elements of its tagged version. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ tag 𝐵)
Theorem	bj-tagcg 36967	Characterization of the elements of 𝐵 in terms of elements of its tagged version. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ tag 𝐵))
Theorem	bj-taginv 36968*	Inverse of tagging. (Contributed by BJ, 6-Oct-2018.)
⊢ 𝐴 = {𝑥 ∣ {𝑥} ∈ tag 𝐴}
Theorem	bj-tagex 36969	A class is a set if and only if its tagging is a set. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ V ↔ tag 𝐴 ∈ V)
Theorem	bj-xtageq 36970	The products of a given class and the tagging of either of two equal classes are equal. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐴 = 𝐵 → (𝐶 × tag 𝐴) = (𝐶 × tag 𝐵))
Theorem	bj-xtagex 36971	The product of a set and the tagging of a set is a set. (Contributed by BJ, 2-Apr-2019.)
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ 𝑊 → (𝐴 × tag 𝐵) ∈ V))
21.19.5.15  Tuples of classes This subsection gives a definition of an ordered pair, or couple (2-tuple), that "works" for proper classes, as evidenced by Theorems bj-2uplth 37003 and bj-2uplex 37004, and more importantly, bj-pr21val 36995 and bj-pr22val 37001. In particular, one can define well-behaved tuples of classes. Classes in ZF(C) are only virtual, and in particular they cannot be quantified over. Theorem bj-2uplex 37004 has advantages: in view of df-br 5148, several sethood antecedents could be removed from existing theorems. For instance, relsnopg 5815 (resp. relsnop 5817) would hold without antecedents (resp. hypotheses) thanks to relsnb 5814). Also, the antecedent Rel 𝑅 could be removed from brrelex12 5740 and related theorems brrelex*, and, as a consequence, of multiple later theorems. Similarly, df-struct 17180 could be simplified by removing the exception currently made for the empty set. The projections are denoted by pr1 and pr2 and the couple with projections (or coordinates) 𝐴 and 𝐵 is denoted by ⦅𝐴, 𝐵⦆. Note that this definition uses the Kuratowski definition (df-op 4637) as a preliminary definition, and then "redefines" a couple. It could also use the "short" version of the Kuratowski pair (see opthreg 9655) 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 5752, but here we use "tagged versions" of the factors (see df-bj-tag 36957) 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 two-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 36957)
Syntax	bj-cproj 36972	Syntax for the class projection. (Contributed by BJ, 6-Apr-2019.)
class (𝐴 Proj 𝐵)
Definition	df-bj-proj 36973*	Definition of the class projection corresponding to tagged tuples. The expression (𝐴 Proj 𝐵) denotes the projection on the A^th component. (Contributed by BJ, 6-Apr-2019.) (New usage is discouraged.)
⊢ (𝐴 Proj 𝐵) = {𝑥 ∣ {𝑥} ∈ (𝐵 “ {𝐴})}
Theorem	bj-projeq 36974	Substitution property for Proj. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐴 = 𝐶 → (𝐵 = 𝐷 → (𝐴 Proj 𝐵) = (𝐶 Proj 𝐷)))
Theorem	bj-projeq2 36975	Substitution property for Proj. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐵 = 𝐶 → (𝐴 Proj 𝐵) = (𝐴 Proj 𝐶))
Theorem	bj-projun 36976	The class projection on a given component preserves unions. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐴 Proj (𝐵 ∪ 𝐶)) = ((𝐴 Proj 𝐵) ∪ (𝐴 Proj 𝐶))
Theorem	bj-projex 36977	Sethood of the class projection. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 Proj 𝐵) ∈ V)
Theorem	bj-projval 36978	Value of the class projection. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 Proj ({𝐵} × tag 𝐶)) = if(𝐵 = 𝐴, 𝐶, ∅))
Syntax	bj-c1upl 36979	Syntax for Morse monuple. (Contributed by BJ, 6-Apr-2019.)
class ⦅𝐴⦆
Definition	df-bj-1upl 36980	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 36994, bj-2uplth 37003, bj-2uplex 37004, and the properties of the projections (see df-bj-pr1 36983 and df-bj-pr2 36997). (Contributed by BJ, 6-Apr-2019.) (New usage is discouraged.)
⊢ ⦅𝐴⦆ = ({∅} × tag 𝐴)
Theorem	bj-1upleq 36981	Substitution property for ⦅ − ⦆. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐴 = 𝐵 → ⦅𝐴⦆ = ⦅𝐵⦆)
Syntax	bj-cpr1 36982	Syntax for the first class tuple projection. (Contributed by BJ, 6-Apr-2019.)
class pr1 𝐴
Definition	df-bj-pr1 36983	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 36984, bj-pr11val 36987, bj-pr21val 36995, bj-pr1ex 36988. (Contributed by BJ, 6-Apr-2019.) (New usage is discouraged.)
⊢ pr1 𝐴 = (∅ Proj 𝐴)
Theorem	bj-pr1eq 36984	Substitution property for pr1. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐴 = 𝐵 → pr1 𝐴 = pr1 𝐵)
Theorem	bj-pr1un 36985	The first projection preserves unions. (Contributed by BJ, 6-Apr-2019.)
⊢ pr1 (𝐴 ∪ 𝐵) = (pr1 𝐴 ∪ pr1 𝐵)
Theorem	bj-pr1val 36986	Value of the first projection. (Contributed by BJ, 6-Apr-2019.)
⊢ pr1 ({𝐴} × tag 𝐵) = if(𝐴 = ∅, 𝐵, ∅)
Theorem	bj-pr11val 36987	Value of the first projection of a monuple. (Contributed by BJ, 6-Apr-2019.)
⊢ pr1 ⦅𝐴⦆ = 𝐴
Theorem	bj-pr1ex 36988	Sethood of the first projection. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 ∈ 𝑉 → pr1 𝐴 ∈ V)
Theorem	bj-1uplth 36989	The characteristic property of monuples. Note that this holds without sethood hypotheses. (Contributed by BJ, 6-Apr-2019.)
⊢ (⦅𝐴⦆ = ⦅𝐵⦆ ↔ 𝐴 = 𝐵)
Theorem	bj-1uplex 36990	A monuple is a set if and only if its coordinates are sets. (Contributed by BJ, 6-Apr-2019.)
⊢ (⦅𝐴⦆ ∈ V ↔ 𝐴 ∈ V)
Theorem	bj-1upln0 36991	A monuple is nonempty. (Contributed by BJ, 6-Apr-2019.)
⊢ ⦅𝐴⦆ ≠ ∅
Syntax	bj-c2uple 36992	Syntax for Morse couple. (Contributed by BJ, 6-Oct-2018.)
class ⦅𝐴, 𝐵⦆
Definition	df-bj-2upl 36993	Definition of the Morse couple. See df-bj-1upl 36980. New usage is discouraged because the precise definition is generally unimportant compared to the characteristic properties bj-2upleq 36994, bj-2uplth 37003, bj-2uplex 37004, and the properties of the projections (see df-bj-pr1 36983 and df-bj-pr2 36997). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.)
⊢ ⦅𝐴, 𝐵⦆ = (⦅𝐴⦆ ∪ ({1o} × tag 𝐵))
Theorem	bj-2upleq 36994	Substitution property for ⦅ − , − ⦆. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 = 𝐵 → (𝐶 = 𝐷 → ⦅𝐴, 𝐶⦆ = ⦅𝐵, 𝐷⦆))
Theorem	bj-pr21val 36995	Value of the first projection of a couple. (Contributed by BJ, 6-Oct-2018.)
⊢ pr1 ⦅𝐴, 𝐵⦆ = 𝐴
Syntax	bj-cpr2 36996	Syntax for the second class tuple projection. (Contributed by BJ, 6-Oct-2018.)
class pr2 𝐴
Definition	df-bj-pr2 36997	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 36998, bj-pr22val 37001, bj-pr2ex 37002. (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.)
⊢ pr2 𝐴 = (1o Proj 𝐴)
Theorem	bj-pr2eq 36998	Substitution property for pr2. (Contributed by BJ, 6-Oct-2018.)
⊢ (𝐴 = 𝐵 → pr2 𝐴 = pr2 𝐵)
Theorem	bj-pr2un 36999	The second projection preserves unions. (Contributed by BJ, 6-Apr-2019.)
⊢ pr2 (𝐴 ∪ 𝐵) = (pr2 𝐴 ∪ pr2 𝐵)
Theorem	bj-pr2val 37000	Value of the second projection. (Contributed by BJ, 6-Apr-2019.)
⊢ pr2 ({𝐴} × tag 𝐵) = if(𝐴 = 1o, 𝐵, ∅)