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	ordsuc 4201	The successor of an ordinal class is ordinal. (Contributed by NM, 3-Apr-1995.) (Constructive proof by Mario Carneiro and Jim Kingdon, 20-Jul-2019.)
⊢ (Ord A ↔ Ord suc A)
Theorem	nlimsucg 4202	A successor is not a limit ordinal. (Contributed by NM, 25-Mar-1995.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (A ∈ 𝑉 → ¬ Lim suc A)
Theorem	ordpwsucss 4203	The collection of ordinals in the power class of an ordinal is a superset of its successor. We can think of (𝒫 A ∩ On) as another possible definition of successor, which would be equivalent to df-suc 4033 given excluded middle. It is an ordinal, and has some successor-like properties. For example, if A ∈ On then both ∪ suc A = A (onunisuci 4095) and ∪ {x ∈ On ∣ x ⊆ A} = A (onuniss2 4163). Constructively (𝒫 A ∩ On) and suc A cannot be shown to be equivalent (as proved at ordpwsucexmid 4206). (Contributed by Jim Kingdon, 21-Jul-2019.)
⊢ (Ord A → suc A ⊆ (𝒫 A ∩ On))
Theorem	onnmin 4204	No member of a set of ordinal numbers belongs to its minimum. (Contributed by NM, 2-Feb-1997.) (Constructive proof by Mario Carneiro and Jim Kingdon, 21-Jul-2019.)
⊢ ((A ⊆ On ∧ B ∈ A) → ¬ B ∈ ∩ A)
Theorem	ssnel 4205	Relationship between subset and elementhood. In the context of ordinals this can be seen as an ordering law. (Contributed by Jim Kingdon, 22-Jul-2019.)
⊢ (A ⊆ B → ¬ B ∈ A)
Theorem	ordpwsucexmid 4206*	The subset in ordpwsucss 4203 cannot be equality. That is, strengthening it to equality implies excluded middle. (Contributed by Jim Kingdon, 30-Jul-2019.)
⊢ ∀x ∈ On suc x = (𝒫 x ∩ On)    ⇒   ⊢ (φ ∨ ¬ φ)
Theorem	onpsssuc 4207	An ordinal number is a proper subset of its successor. (Contributed by Stefan O'Rear, 18-Nov-2014.)
⊢ (A ∈ On → A ⊊ suc A)
2.5.3  Transfinite induction
Theorem	tfi 4208*	The Principle of Transfinite Induction. Theorem 7.17 of [TakeutiZaring] p. 39. This principle states that if A is a class of ordinal numbers with the property that every ordinal number included in A also belongs to A, then every ordinal number is in A. (Contributed by NM, 18-Feb-2004.)
⊢ ((A ⊆ On ∧ ∀x ∈ On (x ⊆ A → x ∈ A)) → A = On)
Theorem	tfis 4209*	Transfinite Induction Schema. If all ordinal numbers less than a given number x have a property (induction hypothesis), then all ordinal numbers have the property (conclusion). Exercise 25 of [Enderton] p. 200. (Contributed by NM, 1-Aug-1994.) (Revised by Mario Carneiro, 20-Nov-2016.)
⊢ (x ∈ On → (∀y ∈ x [y / x]φ → φ))    ⇒   ⊢ (x ∈ On → φ)
Theorem	tfis2f 4210*	Transfinite Induction Schema, using implicit substitution. (Contributed by NM, 18-Aug-1994.)
⊢ Ⅎxψ    &   ⊢ (x = y → (φ ↔ ψ))    &   ⊢ (x ∈ On → (∀y ∈ x ψ → φ))    ⇒   ⊢ (x ∈ On → φ)
Theorem	tfis2 4211*	Transfinite Induction Schema, using implicit substitution. (Contributed by NM, 18-Aug-1994.)
⊢ (x = y → (φ ↔ ψ))    &   ⊢ (x ∈ On → (∀y ∈ x ψ → φ))    ⇒   ⊢ (x ∈ On → φ)
Theorem	tfis3 4212*	Transfinite Induction Schema, using implicit substitution. (Contributed by NM, 4-Nov-2003.)
⊢ (x = y → (φ ↔ ψ))    &   ⊢ (x = A → (φ ↔ χ))    &   ⊢ (x ∈ On → (∀y ∈ x ψ → φ))    ⇒   ⊢ (A ∈ On → χ)
Theorem	tfisi 4213*	A transfinite induction scheme in "implicit" form where the induction is done on an object derived from the object of interest. (Contributed by Stefan O'Rear, 24-Aug-2015.)
⊢ (φ → A ∈ 𝑉)    &   ⊢ (φ → 𝑇 ∈ On)    &   ⊢ ((φ ∧ (𝑅 ∈ On ∧ 𝑅 ⊆ 𝑇) ∧ ∀y(𝑆 ∈ 𝑅 → χ)) → ψ)    &   ⊢ (x = y → (ψ ↔ χ))    &   ⊢ (x = A → (ψ ↔ θ))    &   ⊢ (x = y → 𝑅 = 𝑆)    &   ⊢ (x = A → 𝑅 = 𝑇)    ⇒   ⊢ (φ → θ)
2.6  IZF Set Theory - add the Axiom of Infinity
2.6.1  Introduce the Axiom of Infinity
Axiom	ax-iinf 4214*	Axiom of Infinity. Axiom 5 of [Crosilla] p. "Axioms of CZF and IZF". (Contributed by Jim Kingdon, 16-Nov-2018.)
⊢ ∃x(∅ ∈ x ∧ ∀y(y ∈ x → suc y ∈ x))
Theorem	zfinf2 4215*	A standard version of the Axiom of Infinity, using definitions to abbreviate. Axiom Inf of [BellMachover] p. 472. (Contributed by NM, 30-Aug-1993.)
⊢ ∃x(∅ ∈ x ∧ ∀y ∈ x suc y ∈ x)
2.6.2  The natural numbers (i.e. finite ordinals)
Syntax	com 4216	Extend class notation to include the class of natural numbers.
class 𝜔
Definition	df-iom 4217*	Define the class of natural numbers as the smallest inductive set, which is valid provided we assume the Axiom of Infinity. Definition 6.3 of [Eisenberg] p. 82. Note: the natural numbers 𝜔 are a subset of the ordinal numbers df-on 4030. Later, when we define complex numbers, we will be able to also define a subset of the complex numbers with analogous properties and operations, but they will be different sets. (Contributed by NM, 6-Aug-1994.)
⊢ 𝜔 = ∩ {x ∣ (∅ ∈ x ∧ ∀y ∈ x suc y ∈ x)}
Theorem	dfom3 4218*	Another name for df-iom 4217. (Contributed by NM, 6-Aug-1994.)
⊢ 𝜔 = ∩ {x ∣ (∅ ∈ x ∧ ∀y ∈ x suc y ∈ x)}
Theorem	omex 4219	The existence of omega (the class of natural numbers). Axiom 7 of [TakeutiZaring] p. 43. (Contributed by NM, 6-Aug-1994.)
⊢ 𝜔 ∈ V
2.6.3  Peano's postulates
Theorem	peano1 4220	Zero is a natural number. One of Peano's 5 postulates for arithmetic. Proposition 7.30(1) of [TakeutiZaring] p. 42. (Contributed by NM, 15-May-1994.)
⊢ ∅ ∈ 𝜔
Theorem	peano2 4221	The successor of any natural number is a natural number. One of Peano's 5 postulates for arithmetic. Proposition 7.30(2) of [TakeutiZaring] p. 42. (Contributed by NM, 3-Sep-2003.)
⊢ (A ∈ 𝜔 → suc A ∈ 𝜔)
Theorem	peano3 4222	The successor of any natural number is not zero. One of Peano's 5 postulates for arithmetic. Proposition 7.30(3) of [TakeutiZaring] p. 42. (Contributed by NM, 3-Sep-2003.)
⊢ (A ∈ 𝜔 → suc A ≠ ∅)
Theorem	peano4 4223	Two natural numbers are equal iff their successors are equal, i.e. the successor function is one-to-one. One of Peano's 5 postulates for arithmetic. Proposition 7.30(4) of [TakeutiZaring] p. 43. (Contributed by NM, 3-Sep-2003.)
⊢ ((A ∈ 𝜔 ∧ B ∈ 𝜔) → (suc A = suc B ↔ A = B))
Theorem	peano5 4224*	The induction postulate: any class containing zero and closed under the successor operation contains all natural numbers. One of Peano's 5 postulates for arithmetic. Proposition 7.30(5) of [TakeutiZaring] p. 43. The more traditional statement of mathematical induction as a theorem schema, with a basis and an induction hypothesis, is derived from this theorem as theorem findes 4229. (Contributed by NM, 18-Feb-2004.)
⊢ ((∅ ∈ A ∧ ∀x ∈ 𝜔 (x ∈ A → suc x ∈ A)) → 𝜔 ⊆ A)
2.6.4  Finite induction (for finite ordinals)
Theorem	find 4225*	The Principle of Finite Induction (mathematical induction). Corollary 7.31 of [TakeutiZaring] p. 43. The simpler hypothesis shown here was suggested in an email from "Colin" on 1-Oct-2001. The hypothesis states that A is a set of natural numbers, zero belongs to A, and given any member of A the member's successor also belongs to A. The conclusion is that every natural number is in A. (Contributed by NM, 22-Feb-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ (A ⊆ 𝜔 ∧ ∅ ∈ A ∧ ∀x ∈ A suc x ∈ A)    ⇒   ⊢ A = 𝜔
Theorem	finds 4226*	Principle of Finite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last two are the basis and the induction hypothesis. Theorem Schema 22 of [Suppes] p. 136. (Contributed by NM, 14-Apr-1995.)
⊢ (x = ∅ → (φ ↔ ψ))    &   ⊢ (x = y → (φ ↔ χ))    &   ⊢ (x = suc y → (φ ↔ θ))    &   ⊢ (x = A → (φ ↔ τ))    &   ⊢ ψ    &   ⊢ (y ∈ 𝜔 → (χ → θ))    ⇒   ⊢ (A ∈ 𝜔 → τ)
Theorem	finds2 4227*	Principle of Finite Induction (inference schema), using implicit substitutions. The first three hypotheses establish the substitutions we need. The last two are the basis and the induction hypothesis. Theorem Schema 22 of [Suppes] p. 136. (Contributed by NM, 29-Nov-2002.)
⊢ (x = ∅ → (φ ↔ ψ))    &   ⊢ (x = y → (φ ↔ χ))    &   ⊢ (x = suc y → (φ ↔ θ))    &   ⊢ (τ → ψ)    &   ⊢ (y ∈ 𝜔 → (τ → (χ → θ)))    ⇒   ⊢ (x ∈ 𝜔 → (τ → φ))
Theorem	finds1 4228*	Principle of Finite Induction (inference schema), using implicit substitutions. The first three hypotheses establish the substitutions we need. The last two are the basis and the induction hypothesis. Theorem Schema 22 of [Suppes] p. 136. (Contributed by NM, 22-Mar-2006.)
⊢ (x = ∅ → (φ ↔ ψ))    &   ⊢ (x = y → (φ ↔ χ))    &   ⊢ (x = suc y → (φ ↔ θ))    &   ⊢ ψ    &   ⊢ (y ∈ 𝜔 → (χ → θ))    ⇒   ⊢ (x ∈ 𝜔 → φ)
Theorem	findes 4229	Finite induction with explicit substitution. The first hypothesis is the basis and the second is the induction hypothesis. Theorem Schema 22 of [Suppes] p. 136. (Contributed by Raph Levien, 9-Jul-2003.)
⊢ [∅ / x]φ    &   ⊢ (x ∈ 𝜔 → (φ → [suc x / x]φ))    ⇒   ⊢ (x ∈ 𝜔 → φ)
2.6.5  The Natural Numbers (continued)
Theorem	nn0suc 4230*	A natural number is either 0 or a successor. Similar theorems for arbitrary sets or real numbers will not be provable (without the law of the excluded middle), but equality of natural numbers is decidable. (Contributed by NM, 27-May-1998.)
⊢ (A ∈ 𝜔 → (A = ∅ ∨ ∃x ∈ 𝜔 A = suc x))
Theorem	elnn 4231	A member of a natural number is a natural number. (Contributed by NM, 21-Jun-1998.)
⊢ ((A ∈ B ∧ B ∈ 𝜔) → A ∈ 𝜔)
Theorem	ordom 4232	Omega is ordinal. Theorem 7.32 of [TakeutiZaring] p. 43. (Contributed by NM, 18-Oct-1995.)
⊢ Ord 𝜔
Theorem	omelon2 4233	Omega is an ordinal number. (Contributed by Mario Carneiro, 30-Jan-2013.)
⊢ (𝜔 ∈ V → 𝜔 ∈ On)
Theorem	omelon 4234	Omega is an ordinal number. (Contributed by NM, 10-May-1998.) (Revised by Mario Carneiro, 30-Jan-2013.)
⊢ 𝜔 ∈ On
Theorem	nnon 4235	A natural number is an ordinal number. (Contributed by NM, 27-Jun-1994.)
⊢ (A ∈ 𝜔 → A ∈ On)
Theorem	nnoni 4236	A natural number is an ordinal number. (Contributed by NM, 27-Jun-1994.)
⊢ A ∈ 𝜔    ⇒   ⊢ A ∈ On
Theorem	nnord 4237	A natural number is ordinal. (Contributed by NM, 17-Oct-1995.)
⊢ (A ∈ 𝜔 → Ord A)
Theorem	omsson 4238	Omega is a subset of On. (Contributed by NM, 13-Jun-1994.)
⊢ 𝜔 ⊆ On
Theorem	limom 4239	Omega is a limit ordinal. Theorem 2.8 of [BellMachover] p. 473. (Contributed by NM, 26-Mar-1995.) (Proof rewritten by Jim Kingdon, 5-Jan-2019.)
⊢ Lim 𝜔
Theorem	peano2b 4240	A class belongs to omega iff its successor does. (Contributed by NM, 3-Dec-1995.)
⊢ (A ∈ 𝜔 ↔ suc A ∈ 𝜔)
Theorem	nnsuc 4241*	A nonzero natural number is a successor. (Contributed by NM, 18-Feb-2004.)
⊢ ((A ∈ 𝜔 ∧ A ≠ ∅) → ∃x ∈ 𝜔 A = suc x)
Theorem	nndceq0 4242	A natural number is either zero or nonzero. Decidable equality for natural numbers is a special case of the law of the excluded middle which holds in most constructive set theories including ours. (Contributed by Jim Kingdon, 5-Jan-2019.)
⊢ (A ∈ 𝜔 → DECID A = ∅)
Theorem	0elnn 4243	A natural number is either the empty set or has the empty set as an element. (Contributed by Jim Kingdon, 23-Aug-2019.)
⊢ (A ∈ 𝜔 → (A = ∅ ∨ ∅ ∈ A))
Theorem	nn0eln0 4244	A natural number is nonempty iff it contains the empty set. Although in constructive mathematics it is generally more natural to work with inhabited sets and ignore the whole concept of nonempty sets, in the specific case of natural numbers this theorem may be helpful in converting proofs which were written assuming excluded middle. (Contributed by Jim Kingdon, 28-Aug-2019.)
⊢ (A ∈ 𝜔 → (∅ ∈ A ↔ A ≠ ∅))
Theorem	nnregexmid 4245*	If inhabited sets of natural numbers always have minimal elements, excluded middle follows. The argument is essentially the same as regexmid 4179 and the larger lesson is that although natural numbers may behave "non-constructively" even in a constructive set theory (for example see nndceq 5964 or nntri3or 5961), sets of natural numbers are a different animal. (Contributed by Jim Kingdon, 6-Sep-2019.)
⊢ ((x ⊆ 𝜔 ∧ ∃y y ∈ x) → ∃y(y ∈ x ∧ ∀z(z ∈ y → ¬ z ∈ x)))    ⇒   ⊢ (φ ∨ ¬ φ)
2.6.6  Relations
Syntax	cxp 4246	Extend the definition of a class to include the cross product.
class (A × B)
Syntax	ccnv 4247	Extend the definition of a class to include the converse of a class.
class ◡A
Syntax	cdm 4248	Extend the definition of a class to include the domain of a class.
class dom A
Syntax	crn 4249	Extend the definition of a class to include the range of a class.
class ran A
Syntax	cres 4250	Extend the definition of a class to include the restriction of a class. (Read: The restriction of A to B.)
class (A ↾ B)
Syntax	cima 4251	Extend the definition of a class to include the image of a class. (Read: The image of B under A.)
class (A “ B)
Syntax	ccom 4252	Extend the definition of a class to include the composition of two classes. (Read: The composition of A and B.)
class (A ∘ B)
Syntax	wrel 4253	Extend the definition of a wff to include the relation predicate. (Read: A is a relation.)
wff Rel A
Definition	df-xp 4254*	Define the cross product of two classes. Definition 9.11 of [Quine] p. 64. For example, ( { 1 , 5 } × { 2 , 7 } ) = ( { ⟨ 1 , 2 ⟩, ⟨ 1 , 7 ⟩ } ∪ { ⟨ 5 , 2 ⟩, ⟨ 5 , 7 ⟩ } ) . Another example is that the set of rational numbers are defined in using the cross-product ( Z × N ) ; the left- and right-hand sides of the cross-product represent the top (integer) and bottom (natural) numbers of a fraction. (Contributed by NM, 4-Jul-1994.)
⊢ (A × B) = {⟨x, y⟩ ∣ (x ∈ A ∧ y ∈ B)}
Definition	df-rel 4255	Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 4675 and dfrel3 4682. (Contributed by NM, 1-Aug-1994.)
⊢ (Rel A ↔ A ⊆ (V × V))
Definition	df-cnv 4256*	Define the converse of a class. Definition 9.12 of [Quine] p. 64. The converse of a binary relation swaps its arguments, i.e., if A ∈ V and B ∈ V then (A◡𝑅B ↔ B𝑅A), as proven in brcnv 4421 (see df-br 3718 and df-rel 4255 for more on relations). For example, ◡ { ⟨ 2 , 6 ⟩, ⟨ 3 , 9 ⟩ } = { ⟨ 6 , 2 ⟩, ⟨ 9 , 3 ⟩ } . We use Quine's breve accent (smile) notation. Like Quine, we use it as a prefix, which eliminates the need for parentheses. Many authors use the postfix superscript "to the minus one." "Converse" is Quine's terminology; some authors call it "inverse," especially when the argument is a function. (Contributed by NM, 4-Jul-1994.)
⊢ ◡A = {⟨x, y⟩ ∣ yAx}
Definition	df-co 4257*	Define the composition of two classes. Definition 6.6(3) of [TakeutiZaring] p. 24. Note that Definition 7 of [Suppes] p. 63 reverses A and B, uses a slash instead of ∘, and calls the operation "relative product." (Contributed by NM, 4-Jul-1994.)
⊢ (A ∘ B) = {⟨x, y⟩ ∣ ∃z(xBz ∧ zAy)}
Definition	df-dm 4258*	Define the domain of a class. Definition 3 of [Suppes] p. 59. For example, F = { ⟨ 2 , 6 ⟩, ⟨ 3 , 9 ⟩ } → dom F = { 2 , 3 } . Contrast with range (defined in df-rn 4259). For alternate definitions see dfdm2 4756, dfdm3 4425, and dfdm4 4430. The notation "dom " is used by Enderton; other authors sometimes use script D. (Contributed by NM, 1-Aug-1994.)
⊢ dom A = {x ∣ ∃y xAy}
Definition	df-rn 4259	Define the range of a class. For example, F = { ⟨ 2 , 6 ⟩, ⟨ 3 , 9 ⟩ } -> ran F = { 6 , 9 } . Contrast with domain (defined in df-dm 4258). For alternate definitions, see dfrn2 4426, dfrn3 4427, and dfrn4 4685. The notation "ran " is used by Enderton; other authors sometimes use script R or script W. (Contributed by NM, 1-Aug-1994.)
⊢ ran A = dom ◡A
Definition	df-res 4260	Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example ( F = { ⟨ 2 , 6 ⟩, ⟨ 3 , 9 ⟩ } ∧ B = { 1 , 2 } ) -> ( F ↾ B ) = { ⟨ 2 , 6 ⟩ } . (Contributed by NM, 2-Aug-1994.)
⊢ (A ↾ B) = (A ∩ (B × V))
Definition	df-ima 4261	Define the image of a class (as restricted by another class). Definition 6.6(2) of [TakeutiZaring] p. 24. For example, ( F = { ⟨ 2 , 6 ⟩, ⟨ 3 , 9 ⟩ } /\ B = { 1 , 2 } ) -> ( F “ B ) = { 6 } . Contrast with restriction (df-res 4260) and range (df-rn 4259). For an alternate definition, see dfima2 4574. (Contributed by NM, 2-Aug-1994.)
⊢ (A “ B) = ran (A ↾ B)
Theorem	xpeq1 4262	Equality theorem for cross product. (Contributed by NM, 4-Jul-1994.)
⊢ (A = B → (A × 𝐶) = (B × 𝐶))
Theorem	xpeq2 4263	Equality theorem for cross product. (Contributed by NM, 5-Jul-1994.)
⊢ (A = B → (𝐶 × A) = (𝐶 × B))
Theorem	elxpi 4264*	Membership in a cross product. Uses fewer axioms than elxp 4265. (Contributed by NM, 4-Jul-1994.)
⊢ (A ∈ (B × 𝐶) → ∃x∃y(A = ⟨x, y⟩ ∧ (x ∈ B ∧ y ∈ 𝐶)))
Theorem	elxp 4265*	Membership in a cross product. (Contributed by NM, 4-Jul-1994.)
⊢ (A ∈ (B × 𝐶) ↔ ∃x∃y(A = ⟨x, y⟩ ∧ (x ∈ B ∧ y ∈ 𝐶)))
Theorem	elxp2 4266*	Membership in a cross product. (Contributed by NM, 23-Feb-2004.)
⊢ (A ∈ (B × 𝐶) ↔ ∃x ∈ B ∃y ∈ 𝐶 A = ⟨x, y⟩)
Theorem	xpeq12 4267	Equality theorem for cross product. (Contributed by FL, 31-Aug-2009.)
⊢ ((A = B ∧ 𝐶 = 𝐷) → (A × 𝐶) = (B × 𝐷))
Theorem	xpeq1i 4268	Equality inference for cross product. (Contributed by NM, 21-Dec-2008.)
⊢ A = B    ⇒   ⊢ (A × 𝐶) = (B × 𝐶)
Theorem	xpeq2i 4269	Equality inference for cross product. (Contributed by NM, 21-Dec-2008.)
⊢ A = B    ⇒   ⊢ (𝐶 × A) = (𝐶 × B)
Theorem	xpeq12i 4270	Equality inference for cross product. (Contributed by FL, 31-Aug-2009.)
⊢ A = B    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (A × 𝐶) = (B × 𝐷)
Theorem	xpeq1d 4271	Equality deduction for cross product. (Contributed by Jeff Madsen, 17-Jun-2010.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (A × 𝐶) = (B × 𝐶))
Theorem	xpeq2d 4272	Equality deduction for cross product. (Contributed by Jeff Madsen, 17-Jun-2010.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → (𝐶 × A) = (𝐶 × B))
Theorem	xpeq12d 4273	Equality deduction for cross product. (Contributed by NM, 8-Dec-2013.)
⊢ (φ → A = B)    &   ⊢ (φ → 𝐶 = 𝐷)    ⇒   ⊢ (φ → (A × 𝐶) = (B × 𝐷))
Theorem	nfxp 4274	Bound-variable hypothesis builder for cross product. (Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ ℲxA    &   ⊢ ℲxB    ⇒   ⊢ Ⅎx(A × B)
Theorem	0nelxp 4275	The empty set is not a member of a cross product. (Contributed by NM, 2-May-1996.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ ¬ ∅ ∈ (A × B)
Theorem	0nelelxp 4276	A member of a cross product (ordered pair) doesn't contain the empty set. (Contributed by NM, 15-Dec-2008.)
⊢ (𝐶 ∈ (A × B) → ¬ ∅ ∈ 𝐶)
Theorem	opelxp 4277	Ordered pair membership in a cross product. (Contributed by NM, 15-Nov-1994.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ (⟨A, B⟩ ∈ (𝐶 × 𝐷) ↔ (A ∈ 𝐶 ∧ B ∈ 𝐷))
Theorem	brxp 4278	Binary relation on a cross product. (Contributed by NM, 22-Apr-2004.)
⊢ (A(𝐶 × 𝐷)B ↔ (A ∈ 𝐶 ∧ B ∈ 𝐷))
Theorem	opelxpi 4279	Ordered pair membership in a cross product (implication). (Contributed by NM, 28-May-1995.)
⊢ ((A ∈ 𝐶 ∧ B ∈ 𝐷) → ⟨A, B⟩ ∈ (𝐶 × 𝐷))
Theorem	opelxp1 4280	The first member of an ordered pair of classes in a cross product belongs to first cross product argument. (Contributed by NM, 28-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ (⟨A, B⟩ ∈ (𝐶 × 𝐷) → A ∈ 𝐶)
Theorem	opelxp2 4281	The second member of an ordered pair of classes in a cross product belongs to second cross product argument. (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ (⟨A, B⟩ ∈ (𝐶 × 𝐷) → B ∈ 𝐷)
Theorem	otelxp1 4282	The first member of an ordered triple of classes in a cross product belongs to first cross product argument. (Contributed by NM, 28-May-2008.)
⊢ (⟨⟨A, B⟩, 𝐶⟩ ∈ ((𝑅 × 𝑆) × 𝑇) → A ∈ 𝑅)
Theorem	rabxp 4283*	Membership in a class builder restricted to a cross product. (Contributed by NM, 20-Feb-2014.)
⊢ (x = ⟨y, z⟩ → (φ ↔ ψ))    ⇒   ⊢ {x ∈ (A × B) ∣ φ} = {⟨y, z⟩ ∣ (y ∈ A ∧ z ∈ B ∧ ψ)}
Theorem	brrelex12 4284	A true binary relation on a relation implies the arguments are sets. (This is a property of our ordered pair definition.) (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ ((Rel 𝑅 ∧ A𝑅B) → (A ∈ V ∧ B ∈ V))
Theorem	brrelex 4285	A true binary relation on a relation implies the first argument is a set. (This is a property of our ordered pair definition.) (Contributed by NM, 18-May-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ ((Rel 𝑅 ∧ A𝑅B) → A ∈ V)
Theorem	brrelex2 4286	A true binary relation on a relation implies the second argument is a set. (This is a property of our ordered pair definition.) (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ ((Rel 𝑅 ∧ A𝑅B) → B ∈ V)
Theorem	brrelexi 4287	The first argument of a binary relation exists. (An artifact of our ordered pair definition.) (Contributed by NM, 4-Jun-1998.)
⊢ Rel 𝑅    ⇒   ⊢ (A𝑅B → A ∈ V)
Theorem	brrelex2i 4288	The second argument of a binary relation exists. (An artifact of our ordered pair definition.) (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ Rel 𝑅    ⇒   ⊢ (A𝑅B → B ∈ V)
Theorem	nprrel 4289	No proper class is related to anything via any relation. (Contributed by Roy F. Longton, 30-Jul-2005.)
⊢ Rel 𝑅    &   ⊢ ¬ A ∈ V    ⇒   ⊢ ¬ A𝑅B
Theorem	fconstmpt 4290*	Representation of a constant function using the mapping operation. (Note that x cannot appear free in B.) (Contributed by NM, 12-Oct-1999.) (Revised by Mario Carneiro, 16-Nov-2013.)
⊢ (A × {B}) = (x ∈ A ↦ B)
Theorem	vtoclr 4291*	Variable to class conversion of transitive relation. (Contributed by NM, 9-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ Rel 𝑅    &   ⊢ ((x𝑅y ∧ y𝑅z) → x𝑅z)    ⇒   ⊢ ((A𝑅B ∧ B𝑅𝐶) → A𝑅𝐶)
Theorem	opelvvg 4292	Ordered pair membership in the universal class of ordered pairs. (Contributed by Mario Carneiro, 3-May-2015.)
⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊) → ⟨A, B⟩ ∈ (V × V))
Theorem	opelvv 4293	Ordered pair membership in the universal class of ordered pairs. (Contributed by NM, 22-Aug-2013.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ ⟨A, B⟩ ∈ (V × V)
Theorem	opthprc 4294	Justification theorem for an ordered pair definition that works for any classes, including proper classes. This is a possible definition implied by the footnote in [Jech] p. 78, which says, "The sophisticated reader will not object to our use of a pair of classes." (Contributed by NM, 28-Sep-2003.)
⊢ (((A × {∅}) ∪ (B × {{∅}})) = ((𝐶 × {∅}) ∪ (𝐷 × {{∅}})) ↔ (A = 𝐶 ∧ B = 𝐷))
Theorem	brel 4295	Two things in a binary relation belong to the relation's domain. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ 𝑅 ⊆ (𝐶 × 𝐷)    ⇒   ⊢ (A𝑅B → (A ∈ 𝐶 ∧ B ∈ 𝐷))
Theorem	brab2a 4296*	Ordered pair membership in an ordered pair class abstraction. (Contributed by Mario Carneiro, 9-Nov-2015.)
⊢ ((x = A ∧ y = B) → (φ ↔ ψ))    &   ⊢ 𝑅 = {⟨x, y⟩ ∣ ((x ∈ 𝐶 ∧ y ∈ 𝐷) ∧ φ)}    ⇒   ⊢ (A𝑅B ↔ ((A ∈ 𝐶 ∧ B ∈ 𝐷) ∧ ψ))
Theorem	elxp3 4297*	Membership in a cross product. (Contributed by NM, 5-Mar-1995.)
⊢ (A ∈ (B × 𝐶) ↔ ∃x∃y(⟨x, y⟩ = A ∧ ⟨x, y⟩ ∈ (B × 𝐶)))
Theorem	opeliunxp 4298	Membership in a union of cross products. (Contributed by Mario Carneiro, 29-Dec-2014.) (Revised by Mario Carneiro, 1-Jan-2017.)
⊢ (⟨x, 𝐶⟩ ∈ ∪ x ∈ A ({x} × B) ↔ (x ∈ A ∧ 𝐶 ∈ B))
Theorem	xpundi 4299	Distributive law for cross product over union. Theorem 103 of [Suppes] p. 52. (Contributed by NM, 12-Aug-2004.)
⊢ (A × (B ∪ 𝐶)) = ((A × B) ∪ (A × 𝐶))
Theorem	xpundir 4300	Distributive law for cross product over union. Similar to Theorem 103 of [Suppes] p. 52. (Contributed by NM, 30-Sep-2002.)
⊢ ((A ∪ B) × 𝐶) = ((A × 𝐶) ∪ (B × 𝐶))