P. 43 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 4201-4300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	axpweq 4201*	Two equivalent ways to express the Power Set Axiom. Note that ax-pow 4204 is not used by the proof. (Contributed by NM, 22-Jun-2009.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝒫 𝐴 ∈ V ↔ ∃𝑥∀𝑦(∀𝑧(𝑧 ∈ 𝑦 → 𝑧 ∈ 𝐴) → 𝑦 ∈ 𝑥))
2.2.6  Collection principle
Theorem	bnd 4202*	A very strong generalization of the Axiom of Replacement (compare zfrep6 4147). Its strength lies in the rather profound fact that 𝜑(𝑥, 𝑦) does not have to be a "function-like" wff, as it does in the standard Axiom of Replacement. This theorem is sometimes called the Boundedness Axiom. In the context of IZF, it is just a slight variation of ax-coll 4145. (Contributed by NM, 17-Oct-2004.)
⊢ (∀𝑥 ∈ 𝑧 ∃𝑦𝜑 → ∃𝑤∀𝑥 ∈ 𝑧 ∃𝑦 ∈ 𝑤 𝜑)
Theorem	bnd2 4203*	A variant of the Boundedness Axiom bnd 4202 that picks a subset 𝑧 out of a possibly proper class 𝐵 in which a property is true. (Contributed by NM, 4-Feb-2004.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑧(𝑧 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑧 𝜑))
2.3  IZF Set Theory - add the Axioms of Power Sets and Pairing
2.3.1  Introduce the Axiom of Power Sets
Axiom	ax-pow 4204*	Axiom of Power Sets. An axiom of Intuitionistic Zermelo-Fraenkel set theory. It states that a set 𝑦 exists that includes the power set of a given set 𝑥 i.e. contains every subset of 𝑥. This is Axiom 8 of [Crosilla] p. "Axioms of CZF and IZF" except (a) unnecessary quantifiers are removed, and (b) Crosilla has a biconditional rather than an implication (but the two are equivalent by bm1.3ii 4151). The variant axpow2 4206 uses explicit subset notation. A version using class notation is pwex 4213. (Contributed by NM, 5-Aug-1993.)
⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
Theorem	zfpow 4205*	Axiom of Power Sets expressed with the fewest number of different variables. (Contributed by NM, 14-Aug-2003.)
⊢ ∃𝑥∀𝑦(∀𝑥(𝑥 ∈ 𝑦 → 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)
Theorem	axpow2 4206*	A variant of the Axiom of Power Sets ax-pow 4204 using subset notation. Problem in {BellMachover] p. 466. (Contributed by NM, 4-Jun-2006.)
⊢ ∃𝑦∀𝑧(𝑧 ⊆ 𝑥 → 𝑧 ∈ 𝑦)
Theorem	axpow3 4207*	A variant of the Axiom of Power Sets ax-pow 4204. For any set 𝑥, there exists a set 𝑦 whose members are exactly the subsets of 𝑥 i.e. the power set of 𝑥. Axiom Pow of [BellMachover] p. 466. (Contributed by NM, 4-Jun-2006.)
⊢ ∃𝑦∀𝑧(𝑧 ⊆ 𝑥 ↔ 𝑧 ∈ 𝑦)
Theorem	el 4208*	Every set is an element of some other set. (Contributed by NM, 4-Jan-2002.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ ∃𝑦 𝑥 ∈ 𝑦
Theorem	vpwex 4209	Power set axiom: the powerclass of a set is a set. Axiom 4 of [TakeutiZaring] p. 17. (Contributed by NM, 30-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) Revised to prove pwexg 4210 from vpwex 4209. (Revised by BJ, 10-Aug-2022.)
⊢ 𝒫 𝑥 ∈ V
Theorem	pwexg 4210	Power set axiom expressed in class notation, with the sethood requirement as an antecedent. (Contributed by NM, 30-Oct-2003.)
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V)
Theorem	pwexd 4211	Deduction version of the power set axiom. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝒫 𝐴 ∈ V)
Theorem	abssexg 4212*	Existence of a class of subsets. (Contributed by NM, 15-Jul-2006.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ 𝜑)} ∈ V)
Theorem	pwex 4213	Power set axiom expressed in class notation. (Contributed by NM, 21-Jun-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ 𝒫 𝐴 ∈ V
Theorem	snexg 4214	A singleton whose element exists is a set. The 𝐴 ∈ V case of Theorem 7.12 of [Quine] p. 51, proved using only Extensionality, Power Set, and Separation. Replacement is not needed. (Contributed by Jim Kingdon, 1-Sep-2018.)
⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V)
Theorem	snex 4215	A singleton whose element exists is a set. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 24-May-2019.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {𝐴} ∈ V
Theorem	snexprc 4216	A singleton whose element is a proper class is a set. The ¬ 𝐴 ∈ V case of Theorem 7.12 of [Quine] p. 51, proved using only Extensionality, Power Set, and Separation. Replacement is not needed. (Contributed by Jim Kingdon, 1-Sep-2018.)
⊢ (¬ 𝐴 ∈ V → {𝐴} ∈ V)
Theorem	notnotsnex 4217	A singleton is never a proper class. (Contributed by Mario Carneiro and Jim Kingdon, 3-Jul-2022.)
⊢ ¬ ¬ {𝐴} ∈ V
Theorem	p0ex 4218	The power set of the empty set (the ordinal 1) is a set. (Contributed by NM, 23-Dec-1993.)
⊢ {∅} ∈ V
Theorem	pp0ex 4219	{∅, {∅}} (the ordinal 2) is a set. (Contributed by NM, 5-Aug-1993.)
⊢ {∅, {∅}} ∈ V
Theorem	ord3ex 4220	The ordinal number 3 is a set, proved without the Axiom of Union. (Contributed by NM, 2-May-2009.)
⊢ {∅, {∅}, {∅, {∅}}} ∈ V
Theorem	dtruarb 4221*	At least two sets exist (or in terms of first-order logic, the universe of discourse has two or more objects). This theorem asserts the existence of two sets which do not equal each other; compare with dtruex 4592 in which we are given a set 𝑦 and go from there to a set 𝑥 which is not equal to it. (Contributed by Jim Kingdon, 2-Sep-2018.)
⊢ ∃𝑥∃𝑦 ¬ 𝑥 = 𝑦
Theorem	pwuni 4222	A class is a subclass of the power class of its union. Exercise 6(b) of [Enderton] p. 38. (Contributed by NM, 14-Oct-1996.)
⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴
Theorem	undifexmid 4223*	Union of complementary parts producing the whole and excluded middle. Although special cases such as undifss 3528 and undifdcss 6981 are provable, the full statement implies excluded middle as shown here. (Contributed by Jim Kingdon, 16-Jun-2022.)
⊢ (𝑥 ⊆ 𝑦 ↔ (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦)    ⇒   ⊢ (𝜑 ∨ ¬ 𝜑)
2.3.2  A notation for excluded middle
Syntax	wem 4224	Formula for an abbreviation of excluded middle.
wff EXMID
Definition	df-exmid 4225	The expression EXMID will be used as a readable shorthand for any form of the law of the excluded middle; this is a useful shorthand largely because it hides statements of the form "for any proposition" in a system which can only quantify over sets, not propositions. To see how this compares with other ways of expressing excluded middle, compare undifexmid 4223 with exmidundif 4236. The former may be more recognizable as excluded middle because it is in terms of propositions, and the proof may be easier to follow for much the same reason (it just has to show 𝜑 and ¬ 𝜑 in the the relevant parts of the proof). The latter, however, has the key advantage of being able to prove both directions of the biconditional. To state that excluded middle implies a proposition is hard to do gracefully without EXMID, because there is no way to write a hypothesis 𝜑 ∨ ¬ 𝜑 for an arbitrary proposition; instead the hypothesis would need to be the particular instance of excluded middle which that proof needs. Or to say it another way, EXMID implies DECID 𝜑 by exmidexmid 4226 but there is no good way to express the converse. This definition and how we use it is easiest to understand (and most appropriate to assign the name "excluded middle" to) if we assume ax-sep 4148, in which case EXMID means that all propositions are decidable (see exmidexmid 4226 and notice that it relies on ax-sep 4148). If we instead work with ax-bdsep 15446, EXMID as defined here means that all bounded propositions are decidable. (Contributed by Mario Carneiro and Jim Kingdon, 18-Jun-2022.)
⊢ (EXMID ↔ ∀𝑥(𝑥 ⊆ {∅} → DECID ∅ ∈ 𝑥))
Theorem	exmidexmid 4226	EXMID implies that an arbitrary proposition is decidable. That is, EXMID captures the usual meaning of excluded middle when stated in terms of propositions. To get other propositional statements which are equivalent to excluded middle, combine this with notnotrdc 844, peircedc 915, or condc 854. (Contributed by Jim Kingdon, 18-Jun-2022.)
⊢ (EXMID → DECID 𝜑)
Theorem	ss1o0el1 4227	A subclass of {∅} contains the empty set if and only if it equals {∅}. (Contributed by BJ and Jim Kingdon, 9-Aug-2024.)
⊢ (𝐴 ⊆ {∅} → (∅ ∈ 𝐴 ↔ 𝐴 = {∅}))
Theorem	exmid01 4228	Excluded middle is equivalent to saying any subset of {∅} is either ∅ or {∅}. (Contributed by BJ and Jim Kingdon, 18-Jun-2022.)
⊢ (EXMID ↔ ∀𝑥(𝑥 ⊆ {∅} → (𝑥 = ∅ ∨ 𝑥 = {∅})))
Theorem	pwntru 4229	A slight strengthening of pwtrufal 15558. (Contributed by Mario Carneiro and Jim Kingdon, 12-Sep-2023.)
⊢ ((𝐴 ⊆ {∅} ∧ 𝐴 ≠ {∅}) → 𝐴 = ∅)
Theorem	exmid1dc 4230*	A convenience theorem for proving that something implies EXMID. Think of this as an alternative to using a proposition, as in proofs like undifexmid 4223 or ordtriexmid 4554. In this context 𝑥 = {∅} can be thought of as "x is true". (Contributed by Jim Kingdon, 21-Nov-2023.)
⊢ ((𝜑 ∧ 𝑥 ⊆ {∅}) → DECID 𝑥 = {∅})    ⇒   ⊢ (𝜑 → EXMID)
Theorem	exmidn0m 4231*	Excluded middle is equivalent to any set being empty or inhabited. (Contributed by Jim Kingdon, 5-Mar-2023.)
⊢ (EXMID ↔ ∀𝑥(𝑥 = ∅ ∨ ∃𝑦 𝑦 ∈ 𝑥))
Theorem	exmidsssn 4232*	Excluded middle is equivalent to the biconditionalized version of sssnr 3780 for sets. (Contributed by Jim Kingdon, 5-Mar-2023.)
⊢ (EXMID ↔ ∀𝑥∀𝑦(𝑥 ⊆ {𝑦} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝑦})))
Theorem	exmidsssnc 4233*	Excluded middle in terms of subsets of a singleton. This is similar to exmid01 4228 but lets you choose any set as the element of the singleton rather than just ∅. It is similar to exmidsssn 4232 but for a particular set 𝐵 rather than all sets. (Contributed by Jim Kingdon, 29-Jul-2023.)
⊢ (𝐵 ∈ 𝑉 → (EXMID ↔ ∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵}))))
Theorem	exmid0el 4234	Excluded middle is equivalent to decidability of ∅ being an element of an arbitrary set. (Contributed by Jim Kingdon, 18-Jun-2022.)
⊢ (EXMID ↔ ∀𝑥DECID ∅ ∈ 𝑥)
Theorem	exmidel 4235*	Excluded middle is equivalent to decidability of membership for two arbitrary sets. (Contributed by Jim Kingdon, 18-Jun-2022.)
⊢ (EXMID ↔ ∀𝑥∀𝑦DECID 𝑥 ∈ 𝑦)
Theorem	exmidundif 4236*	Excluded middle is equivalent to every subset having a complement. That is, the union of a subset and its relative complement being the whole set. Although special cases such as undifss 3528 and undifdcss 6981 are provable, the full statement is equivalent to excluded middle as shown here. (Contributed by Jim Kingdon, 18-Jun-2022.)
⊢ (EXMID ↔ ∀𝑥∀𝑦(𝑥 ⊆ 𝑦 ↔ (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦))
Theorem	exmidundifim 4237*	Excluded middle is equivalent to every subset having a complement. Variation of exmidundif 4236 with an implication rather than a biconditional. (Contributed by Jim Kingdon, 16-Feb-2023.)
⊢ (EXMID ↔ ∀𝑥∀𝑦(𝑥 ⊆ 𝑦 → (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦))
Theorem	exmid1stab 4238*	If every proposition is stable, excluded middle follows. We are thinking of 𝑥 as a proposition and 𝑥 = {∅} as "𝑥 is true". (Contributed by Jim Kingdon, 28-Nov-2023.)
⊢ ((𝜑 ∧ 𝑥 ⊆ {∅}) → STAB 𝑥 = {∅})    ⇒   ⊢ (𝜑 → EXMID)
2.3.3  Axiom of Pairing
Axiom	ax-pr 4239*	The Axiom of Pairing of IZF set theory. Axiom 2 of [Crosilla] p. "Axioms of CZF and IZF", except (a) unnecessary quantifiers are removed, and (b) Crosilla has a biconditional rather than an implication (but the two are equivalent by bm1.3ii 4151). (Contributed by NM, 14-Nov-2006.)
⊢ ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)
Theorem	zfpair2 4240	Derive the abbreviated version of the Axiom of Pairing from ax-pr 4239. (Contributed by NM, 14-Nov-2006.)
⊢ {𝑥, 𝑦} ∈ V
Theorem	prexg 4241	The Axiom of Pairing using class variables. Theorem 7.13 of [Quine] p. 51, but restricted to classes which exist. For proper classes, see prprc 3729, prprc1 3727, and prprc2 3728. (Contributed by Jim Kingdon, 16-Sep-2018.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V)
Theorem	snelpwi 4242	A singleton of a set belongs to the power class of a class containing the set. (Contributed by Alan Sare, 25-Aug-2011.)
⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ 𝒫 𝐵)
Theorem	snelpw 4243	A singleton of a set belongs to the power class of a class containing the set. (Contributed by NM, 1-Apr-1998.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ 𝒫 𝐵)
Theorem	prelpwi 4244	A pair of two sets belongs to the power class of a class containing those two sets. (Contributed by Thierry Arnoux, 10-Mar-2017.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → {𝐴, 𝐵} ∈ 𝒫 𝐶)
Theorem	rext 4245*	A theorem similar to extensionality, requiring the existence of a singleton. Exercise 8 of [TakeutiZaring] p. 16. (Contributed by NM, 10-Aug-1993.)
⊢ (∀𝑧(𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧) → 𝑥 = 𝑦)
Theorem	sspwb 4246	Classes are subclasses if and only if their power classes are subclasses. Exercise 18 of [TakeutiZaring] p. 18. (Contributed by NM, 13-Oct-1996.)
⊢ (𝐴 ⊆ 𝐵 ↔ 𝒫 𝐴 ⊆ 𝒫 𝐵)
Theorem	unipw 4247	A class equals the union of its power class. Exercise 6(a) of [Enderton] p. 38. (Contributed by NM, 14-Oct-1996.) (Proof shortened by Alan Sare, 28-Dec-2008.)
⊢ ∪ 𝒫 𝐴 = 𝐴
Theorem	pwel 4248	Membership of a power class. Exercise 10 of [Enderton] p. 26. (Contributed by NM, 13-Jan-2007.)
⊢ (𝐴 ∈ 𝐵 → 𝒫 𝐴 ∈ 𝒫 𝒫 ∪ 𝐵)
Theorem	pwtr 4249	A class is transitive iff its power class is transitive. (Contributed by Alan Sare, 25-Aug-2011.) (Revised by Mario Carneiro, 15-Jun-2014.)
⊢ (Tr 𝐴 ↔ Tr 𝒫 𝐴)
Theorem	ssextss 4250*	An extensionality-like principle defining subclass in terms of subsets. (Contributed by NM, 30-Jun-2004.)
⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ⊆ 𝐴 → 𝑥 ⊆ 𝐵))
Theorem	ssext 4251*	An extensionality-like principle that uses the subset instead of the membership relation: two classes are equal iff they have the same subsets. (Contributed by NM, 30-Jun-2004.)
⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ⊆ 𝐴 ↔ 𝑥 ⊆ 𝐵))
Theorem	nssssr 4252*	Negation of subclass relationship. Compare nssr 3240. (Contributed by Jim Kingdon, 17-Sep-2018.)
⊢ (∃𝑥(𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵) → ¬ 𝐴 ⊆ 𝐵)
Theorem	pweqb 4253	Classes are equal if and only if their power classes are equal. Exercise 19 of [TakeutiZaring] p. 18. (Contributed by NM, 13-Oct-1996.)
⊢ (𝐴 = 𝐵 ↔ 𝒫 𝐴 = 𝒫 𝐵)
Theorem	intid 4254*	The intersection of all sets to which a set belongs is the singleton of that set. (Contributed by NM, 5-Jun-2009.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∩ {𝑥 ∣ 𝐴 ∈ 𝑥} = {𝐴}
Theorem	euabex 4255	The abstraction of a wff with existential uniqueness exists. (Contributed by NM, 25-Nov-1994.)
⊢ (∃!𝑥𝜑 → {𝑥 ∣ 𝜑} ∈ V)
Theorem	mss 4256*	An inhabited class (even if proper) has an inhabited subset. (Contributed by Jim Kingdon, 17-Sep-2018.)
⊢ (∃𝑦 𝑦 ∈ 𝐴 → ∃𝑥(𝑥 ⊆ 𝐴 ∧ ∃𝑧 𝑧 ∈ 𝑥))
Theorem	exss 4257*	Restricted existence in a class (even if proper) implies restricted existence in a subset. (Contributed by NM, 23-Aug-2003.)
⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑦(𝑦 ⊆ 𝐴 ∧ ∃𝑥 ∈ 𝑦 𝜑))
Theorem	opexg 4258	An ordered pair of sets is a set. (Contributed by Jim Kingdon, 11-Jan-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ⟨𝐴, 𝐵⟩ ∈ V)
Theorem	opex 4259	An ordered pair of sets is a set. (Contributed by Jim Kingdon, 24-Sep-2018.) (Revised by Mario Carneiro, 24-May-2019.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ⟨𝐴, 𝐵⟩ ∈ V
Theorem	otexg 4260	An ordered triple of sets is a set. (Contributed by Jim Kingdon, 19-Sep-2018.)
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → ⟨𝐴, 𝐵, 𝐶⟩ ∈ V)
Theorem	elop 4261	An ordered pair has two elements. Exercise 3 of [TakeutiZaring] p. 15. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐴 ∈ ⟨𝐵, 𝐶⟩ ↔ (𝐴 = {𝐵} ∨ 𝐴 = {𝐵, 𝐶}))
Theorem	opi1 4262	One of the two elements in an ordered pair. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ {𝐴} ∈ ⟨𝐴, 𝐵⟩
Theorem	opi2 4263	One of the two elements of an ordered pair. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ {𝐴, 𝐵} ∈ ⟨𝐴, 𝐵⟩
2.3.4  Ordered pair theorem
Theorem	opm 4264*	An ordered pair is inhabited iff the arguments are sets. (Contributed by Jim Kingdon, 21-Sep-2018.)
⊢ (∃𝑥 𝑥 ∈ ⟨𝐴, 𝐵⟩ ↔ (𝐴 ∈ V ∧ 𝐵 ∈ V))
Theorem	opnzi 4265	An ordered pair is nonempty if the arguments are sets (it is also inhabited; see opm 4264). (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ⟨𝐴, 𝐵⟩ ≠ ∅
Theorem	opth1 4266	Equality of the first members of equal ordered pairs. (Contributed by NM, 28-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐴 = 𝐶)
Theorem	opth 4267	The ordered pair theorem. If two ordered pairs are equal, their first elements are equal and their second elements are equal. Exercise 6 of [TakeutiZaring] p. 16. Note that 𝐶 and 𝐷 are not required to be sets due our specific ordered pair definition. (Contributed by NM, 28-May-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	opthg 4268	Ordered pair theorem. 𝐶 and 𝐷 are not required to be sets under our specific ordered pair definition. (Contributed by NM, 14-Oct-2005.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
Theorem	opthg2 4269	Ordered pair theorem. (Contributed by NM, 14-Oct-2005.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
Theorem	opth2 4270	Ordered pair theorem. (Contributed by NM, 21-Sep-2014.)
⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	otth2 4271	Ordered triple theorem, with triple express with ordered pairs. (Contributed by NM, 1-May-1995.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝑅 ∈ V    ⇒   ⊢ (⟨⟨𝐴, 𝐵⟩, 𝑅⟩ = ⟨⟨𝐶, 𝐷⟩, 𝑆⟩ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ∧ 𝑅 = 𝑆))
Theorem	otth 4272	Ordered triple theorem. (Contributed by NM, 25-Sep-2014.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝑅 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵, 𝑅⟩ = ⟨𝐶, 𝐷, 𝑆⟩ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ∧ 𝑅 = 𝑆))
Theorem	eqvinop 4273*	A variable introduction law for ordered pairs. Analog of Lemma 15 of [Monk2] p. 109. (Contributed by NM, 28-May-1995.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (𝐴 = ⟨𝐵, 𝐶⟩ ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ ⟨𝑥, 𝑦⟩ = ⟨𝐵, 𝐶⟩))
Theorem	copsexg 4274*	Substitution of class 𝐴 for ordered pair ⟨𝑥, 𝑦⟩. (Contributed by NM, 27-Dec-1996.) (Revised by Andrew Salmon, 11-Jul-2011.)
⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
Theorem	copsex2t 4275*	Closed theorem form of copsex2g 4276. (Contributed by NM, 17-Feb-2013.)
⊢ ((∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜓))
Theorem	copsex2g 4276*	Implicit substitution inference for ordered pairs. (Contributed by NM, 28-May-1995.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜓))
Theorem	copsex4g 4277*	An implicit substitution inference for 2 ordered pairs. (Contributed by NM, 5-Aug-1995.)
⊢ (((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆)) → (∃𝑥∃𝑦∃𝑧∃𝑤((⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑧, 𝑤⟩) ∧ 𝜑) ↔ 𝜓))
Theorem	0nelop 4278	A property of ordered pairs. (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ ¬ ∅ ∈ ⟨𝐴, 𝐵⟩
Theorem	opeqex 4279	Equivalence of existence implied by equality of ordered pairs. (Contributed by NM, 28-May-2008.)
⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐷 ∈ V)))
Theorem	opcom 4280	An ordered pair commutes iff its members are equal. (Contributed by NM, 28-May-2009.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐵, 𝐴⟩ ↔ 𝐴 = 𝐵)
Theorem	moop2 4281*	"At most one" property of an ordered pair. (Contributed by NM, 11-Apr-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ 𝐵 ∈ V    ⇒   ⊢ ∃*𝑥 𝐴 = ⟨𝐵, 𝑥⟩
Theorem	opeqsn 4282	Equivalence for an ordered pair equal to a singleton. (Contributed by NM, 3-Jun-2008.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩ = {𝐶} ↔ (𝐴 = 𝐵 ∧ 𝐶 = {𝐴}))
Theorem	opeqpr 4283	Equivalence for an ordered pair equal to an unordered pair. (Contributed by NM, 3-Jun-2008.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩ = {𝐶, 𝐷} ↔ ((𝐶 = {𝐴} ∧ 𝐷 = {𝐴, 𝐵}) ∨ (𝐶 = {𝐴, 𝐵} ∧ 𝐷 = {𝐴})))
Theorem	euotd 4284*	Prove existential uniqueness for an ordered triple. (Contributed by Mario Carneiro, 20-May-2015.)
⊢ (𝜑 → 𝐴 ∈ V)    &   ⊢ (𝜑 → 𝐵 ∈ V)    &   ⊢ (𝜑 → 𝐶 ∈ V)    &   ⊢ (𝜑 → (𝜓 ↔ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶)))    ⇒   ⊢ (𝜑 → ∃!𝑥∃𝑎∃𝑏∃𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓))
Theorem	uniop 4285	The union of an ordered pair. Theorem 65 of [Suppes] p. 39. (Contributed by NM, 17-Aug-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ∪ ⟨𝐴, 𝐵⟩ = {𝐴, 𝐵}
Theorem	uniopel 4286	Ordered pair membership is inherited by class union. (Contributed by NM, 13-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩ ∈ 𝐶 → ∪ ⟨𝐴, 𝐵⟩ ∈ ∪ 𝐶)
2.3.5  Ordered-pair class abstractions (cont.)
Theorem	opabid 4287	The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 14-Apr-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜑)
Theorem	opabidw 4288*	The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. Version of opabid 4287 with a disjoint variable condition. (Contributed by NM, 14-Apr-1995.) (Revised by GG, 26-Jan-2024.)
⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜑)
Theorem	elopab 4289*	Membership in a class abstraction of ordered pairs. (Contributed by NM, 24-Mar-1998.)
⊢ (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
Theorem	opelopabsbALT 4290*	The law of concretion in terms of substitutions. Less general than opelopabsb 4291, but having a much shorter proof. (Contributed by NM, 30-Sep-2002.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝑤 / 𝑦][𝑧 / 𝑥]𝜑)
Theorem	opelopabsb 4291*	The law of concretion in terms of substitutions. (Contributed by NM, 30-Sep-2002.) (Revised by Mario Carneiro, 18-Nov-2016.)
⊢ (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑)
Theorem	brabsb 4292*	The law of concretion in terms of substitutions. (Contributed by NM, 17-Mar-2008.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}    ⇒   ⊢ (𝐴𝑅𝐵 ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑)
Theorem	opelopabt 4293*	Closed theorem form of opelopab 4303. (Contributed by NM, 19-Feb-2013.)
⊢ ((∀𝑥∀𝑦(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥∀𝑦(𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜒))
Theorem	opelopabga 4294*	The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 19-Dec-2013.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜓))
Theorem	brabga 4295*	The law of concretion for a binary relation. (Contributed by Mario Carneiro, 19-Dec-2013.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    &   ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴𝑅𝐵 ↔ 𝜓))
Theorem	opelopab2a 4296*	Ordered pair membership in an ordered pair class abstraction. (Contributed by Mario Carneiro, 19-Dec-2013.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ 𝜑)} ↔ 𝜓))
Theorem	opelopaba 4297*	The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 19-Dec-2013.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜓)
Theorem	braba 4298*	The law of concretion for a binary relation. (Contributed by NM, 19-Dec-2013.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    &   ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}    ⇒   ⊢ (𝐴𝑅𝐵 ↔ 𝜓)
Theorem	opelopabg 4299*	The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro, 19-Dec-2013.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜒))
Theorem	brabg 4300*	The law of concretion for a binary relation. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 19-Dec-2013.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝑅𝐵 ↔ 𝜒))