P. 48 of Theorem List - New Foundations Explorer

Home	New Foundations Explorer Theorem List (p. 48 of 64)	< Previous Next >
		Bad symbols? Try the GIF version.
Mirrors > Metamath Home Page > NFE Home Page > Theorem List Contents This page: Page List

**Theorem List for New Foundations Explorer -** 4701-4800 *Has distinct variable group(s)
Type	Label	Description
Statement

Theorem	brabga 4701*	The law of concretion for a binary relation. (Contributed by Mario Carneiro, 19-Dec-2013.)
⊢ ((x = A ∧ y = B) → (φ ↔ ψ)) & ⊢ R = {⟨x, y⟩ ∣ φ} ⇒ ⊢ ((A ∈ V ∧ B ∈ W) → (ARB ↔ ψ))

Theorem	opelopab2a 4702*	Ordered pair membership in an ordered pair class abstraction. (Contributed by Mario Carneiro, 19-Dec-2013.)
⊢ ((x = A ∧ y = B) → (φ ↔ ψ)) ⇒ ⊢ ((A ∈ C ∧ B ∈ D) → (⟨A, B⟩ ∈ {⟨x, y⟩ ∣ ((x ∈ C ∧ y ∈ D) ∧ φ)} ↔ ψ))

Theorem	opelopaba 4703*	The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 19-Dec-2013.)
⊢ A ∈ V & ⊢ B ∈ V & ⊢ ((x = A ∧ y = B) → (φ ↔ ψ)) ⇒ ⊢ (⟨A, B⟩ ∈ {⟨x, y⟩ ∣ φ} ↔ ψ)

Theorem	braba 4704*	The law of concretion for a binary relation. (Contributed by NM, 19-Dec-2013.)
⊢ A ∈ V & ⊢ B ∈ V & ⊢ ((x = A ∧ y = B) → (φ ↔ ψ)) & ⊢ R = {⟨x, y⟩ ∣ φ} ⇒ ⊢ (ARB ↔ ψ)

Theorem	opelopabg 4705*	The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 28-May-1995.) (Revised by set.mm contributors, 19-Dec-2013.)
⊢ (x = A → (φ ↔ ψ)) & ⊢ (y = B → (ψ ↔ χ)) ⇒ ⊢ ((A ∈ V ∧ B ∈ W) → (⟨A, B⟩ ∈ {⟨x, y⟩ ∣ φ} ↔ χ))

Theorem	brabg 4706*	The law of concretion for a binary relation. (Contributed by NM, 16-Aug-1999.) (Revised by set.mm contributors, 19-Dec-2013.)
⊢ (x = A → (φ ↔ ψ)) & ⊢ (y = B → (ψ ↔ χ)) & ⊢ R = {⟨x, y⟩ ∣ φ} ⇒ ⊢ ((A ∈ C ∧ B ∈ D) → (ARB ↔ χ))

Theorem	opelopab2 4707*	Ordered pair membership in an ordered pair class abstraction. (Contributed by NM, 14-Oct-2007.) (Revised by set.mm contributors, 19-Dec-2013.)
⊢ (x = A → (φ ↔ ψ)) & ⊢ (y = B → (ψ ↔ χ)) ⇒ ⊢ ((A ∈ C ∧ B ∈ D) → (⟨A, B⟩ ∈ {⟨x, y⟩ ∣ ((x ∈ C ∧ y ∈ D) ∧ φ)} ↔ χ))

Theorem	opelopab 4708*	The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 16-May-1995.)
⊢ A ∈ V & ⊢ B ∈ V & ⊢ (x = A → (φ ↔ ψ)) & ⊢ (y = B → (ψ ↔ χ)) ⇒ ⊢ (⟨A, B⟩ ∈ {⟨x, y⟩ ∣ φ} ↔ χ)

Theorem	brab 4709*	The law of concretion for a binary relation. (Contributed by NM, 16-Aug-1999.)
⊢ A ∈ V & ⊢ B ∈ V & ⊢ (x = A → (φ ↔ ψ)) & ⊢ (y = B → (ψ ↔ χ)) & ⊢ R = {⟨x, y⟩ ∣ φ} ⇒ ⊢ (ARB ↔ χ)

Theorem	opelopabaf 4710*	The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopab 4708 uses bound-variable hypotheses in place of distinct variable conditions." (Contributed by Mario Carneiro, 19-Dec-2013.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
⊢ Ⅎxψ & ⊢ Ⅎyψ & ⊢ A ∈ V & ⊢ B ∈ V & ⊢ ((x = A ∧ y = B) → (φ ↔ ψ)) ⇒ ⊢ (⟨A, B⟩ ∈ {⟨x, y⟩ ∣ φ} ↔ ψ)

Theorem	opelopabf 4711*	The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopab 4708 uses bound-variable hypotheses in place of distinct variable conditions." (Contributed by NM, 19-Dec-2008.)
⊢ Ⅎxψ & ⊢ Ⅎyχ & ⊢ A ∈ V & ⊢ B ∈ V & ⊢ (x = A → (φ ↔ ψ)) & ⊢ (y = B → (ψ ↔ χ)) ⇒ ⊢ (⟨A, B⟩ ∈ {⟨x, y⟩ ∣ φ} ↔ χ)

Theorem	ssopab2 4712	Equivalence of ordered pair abstraction subclass and implication. (Contributed by NM, 27-Dec-1996.) (Revised by Mario Carneiro, 19-May-2013.)
⊢ (∀x∀y(φ → ψ) → {⟨x, y⟩ ∣ φ} ⊆ {⟨x, y⟩ ∣ ψ})

Theorem	ssopab2b 4713	Equivalence of ordered pair abstraction subclass and implication. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
⊢ ({⟨x, y⟩ ∣ φ} ⊆ {⟨x, y⟩ ∣ ψ} ↔ ∀x∀y(φ → ψ))

Theorem	ssopab2i 4714	Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 5-Apr-1995.)
⊢ (φ → ψ) ⇒ ⊢ {⟨x, y⟩ ∣ φ} ⊆ {⟨x, y⟩ ∣ ψ}

Theorem	ssopab2dv 4715*	Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 19-Jan-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
⊢ (φ → (ψ → χ)) ⇒ ⊢ (φ → {⟨x, y⟩ ∣ ψ} ⊆ {⟨x, y⟩ ∣ χ})

Theorem	opabn0 4716	Nonempty ordered pair class abstraction. (Contributed by NM, 10-Oct-2007.)
⊢ ({⟨x, y⟩ ∣ φ} ≠ ∅ ↔ ∃x∃yφ)

2.3.5 Set construction functions

Syntax	c1st 4717	Extend the definition of a class to include the first member an ordered pair function.
class 1^st

Syntax	cswap 4718	Extend the definition of a class to include the swap function.
class Swap

Syntax	csset 4719	Extend the definition of a class to include the subset relationship.
class S

Syntax	csi 4720	Extend the definition of a class to include the singleton image.
class SI A

Syntax	ccom 4721	Extend the definition of a class to include the composition of two classes.
class (A ∘ B)

Syntax	cima 4722	Extend the definition of a class to include the image of one class under another.
class (A “ B)

Definition	df-1st 4723*	Define a function that extracts the first member, or abscissa, of an ordered pair. (Contributed by SF, 5-Jan-2015.)
⊢ 1^st = {⟨x, y⟩ ∣ ∃z x = ⟨y, z⟩}

Definition	df-swap 4724*	Define a function that swaps the two elements of an ordered pair. (Contributed by SF, 5-Jan-2015.)
⊢ Swap = {⟨x, y⟩ ∣ ∃z∃w(x = ⟨z, w⟩ ∧ y = ⟨w, z⟩)}

Definition	df-sset 4725*	Define a relationship that holds between subsets. (Contributed by SF, 5-Jan-2015.)
⊢ S = {⟨x, y⟩ ∣ x ⊆ y}

Definition	df-co 4726*	Define the composition of two classes. (Contributed by SF, 5-Jan-2015.)
⊢ (A ∘ B) = {⟨x, y⟩ ∣ ∃z(xBz ∧ zAy)}

Definition	df-ima 4727*	Define the image of one class under another. (Contributed by SF, 5-Jan-2015.)
⊢ (A “ B) = {x ∣ ∃y ∈ B yAx}

Definition	df-si 4728*	Define the singleton image of a class. (Contributed by SF, 5-Jan-2015.)
⊢ SI A = {⟨x, y⟩ ∣ ∃z∃w(x = {z} ∧ y = {w} ∧ zAw)}

Theorem	el1st 4729*	Membership in 1^st. (Contributed by SF, 5-Jan-2015.)
⊢ (A ∈ 1^st ↔ ∃x∃y A = ⟨⟨x, y⟩, x⟩)

Theorem	br1stg 4730	The binary relationship over the 1^st function. (Contributed by SF, 5-Jan-2015.)
⊢ ((A ∈ V ∧ B ∈ W) → (⟨A, B⟩1^st C ↔ A = C))

Theorem	setconslem1 4731*	Lemma for the set construction theorems. (Contributed by SF, 6-Jan-2015.)
⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ (⟪{A}, B⟫ ∈ ( S_k ∘_k SI_k ^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V)))) ↔ ∃x ∈ B A = Phi x)

Theorem	setconslem2 4732*	Lemma for the set construction theorems. (Contributed by SF, 6-Jan-2015.)
⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ (⟪{A}, B⟫ ∈ (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ((^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V))) ∘_k S_k ) ∪ ({{0_c}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ↔ ∃x ∈ B A = ( Phi x ∪ {0_c}))

Theorem	setconslem3 4733	Lemma for set construction functions. Set up a mapping between Kuratowski and Quine ordered pairs. (Contributed by SF, 7-Jan-2015.)
⊢ A ∈ V & ⊢ B ∈ V & ⊢ C ∈ V ⇒ ⊢ (⟪{{A}}, ⟪B, C⟫⟫ ∈ ∼ (( Ins3_k SI_k SI_k S_k ⊕ Ins2_k ( Ins3_k ( S_k ∘_k SI_k ^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V)))) ∪ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ((^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V))) ∘_k S_k ) ∪ ({{0_c}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) ↔ A = ⟨B, C⟩)

Theorem	setconslem4 4734*	Lemma for set construction functions. Create a mapping between the two types of ordered pair abstractions. (Contributed by SF, 7-Jan-2015.)
⊢ ⋃₁⋃₁((((V ×_k V) ×_k V) ∩ ^◡_k ∼ (( Ins3_k SI_k SI_k S_k ⊕ Ins2_k ( Ins3_k ( S_k ∘_k SI_k ^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V)))) ∪ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ((^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V))) ∘_k S_k ) ∪ ({{0_c}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c)) “_k A) = {⟨x, y⟩ ∣ ⟪x, y⟫ ∈ A}

Theorem	setconslem5 4735	Lemma for set construction theorems. The big expression in the middle of setconslem4 4734 forms a set. (Contributed by SF, 7-Jan-2015.)
⊢ ∼ (( Ins3_k SI_k SI_k S_k ⊕ Ins2_k ( Ins3_k ( S_k ∘_k SI_k ^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V)))) ∪ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ((^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V))) ∘_k S_k ) ∪ ({{0_c}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) ∈ V

Theorem	setconslem6 4736*	Lemma for the set construction functions. Invert the expression from setconslem4 4734. (Contributed by SF, 7-Jan-2015.)
⊢ (((V ×_k (V ×_k V)) ∩ ∼ (( Ins3_k SI_k SI_k S_k ⊕ Ins2_k ( Ins3_k ( S_k ∘_k SI_k ^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V)))) ∪ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ((^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V))) ∘_k S_k ) ∪ ({{0_c}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁A) = {z ∣ ∃x∃y(z = ⟪x, y⟫ ∧ ⟨x, y⟩ ∈ A)}

Theorem	setconslem7 4737	Lemma for the set construction theorems. Reorganized version of setconslem3 4733. (Contributed by SF, 4-Feb-2015.)
⊢ A ∈ V & ⊢ B ∈ V & ⊢ C ∈ V ⇒ ⊢ (⟪{{C}}, ⟪A, B⟫⟫ ∈ ∼ (( Ins2_k Ins3_k S_k ⊕ ( Ins2_k Ins2_k ( S_k ∘_k SI_k ^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V)))) ∪ Ins3_k SI_k SI_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ((^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V))) ∘_k S_k ) ∪ ({{0_c}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) ↔ A = ⟨B, C⟩)

Theorem	df1st2 4738	Express the 1^st function via the set construction functions. (Contributed by SF, 4-Feb-2015.)
⊢ 1^st = ⋃₁⋃₁((((V ×_k V) ×_k V) ∩ ^◡_k ∼ (( Ins3_k SI_k SI_k S_k ⊕ Ins2_k ( Ins3_k ( S_k ∘_k SI_k ^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V)))) ∪ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ((^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V))) ∘_k S_k ) ∪ ({{0_c}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ( ∼ (( Ins2_k Ins3_k S_k ⊕ ( Ins2_k Ins2_k ( S_k ∘_k SI_k ^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V)))) ∪ Ins3_k SI_k SI_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ((^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V))) ∘_k S_k ) ∪ ({{0_c}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁1_c))

Theorem	1stex 4739	The 1^st function is a set. (Contributed by SF, 6-Jan-2015.)
⊢ 1^st ∈ V

Theorem	elswap 4740*	Membership in the Swap function. (Contributed by SF, 6-Jan-2015.)
⊢ (A ∈ Swap ↔ ∃x∃y A = ⟨⟨x, y⟩, ⟨y, x⟩⟩)

Theorem	dfswap2 4741	Express the Swap function via set construction operators. (Contributed by SF, 6-Jan-2015.)
⊢ Swap = (( ∼ (( Ins2_k Ins2_k S_k ⊕ ((( Ins2_k ( Ins2_k Ins3_k ( S_k ∘_k SI_k ^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V)))) ∪ Ins3_k SI_k SI_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ((^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V))) ∘_k S_k ) ∪ ({{0_c}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) ∩ Ins3_k SI_k SI_k SI_k SI_k SI_k Image_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V)))) “_k ℘₁℘₁℘₁℘₁℘₁℘₁1_c) ∪ (( Ins2_k ( Ins3_k SI_k SI_k ( S_k ∘_k SI_k ^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V)))) ∪ Ins2_k Ins3_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ((^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V))) ∘_k S_k ) ∪ ({{0_c}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c)) ∩ Ins3_k SI_k SI_k SI_k SI_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ((^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V))) ∘_k S_k ) ∪ ({{0_c}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁℘₁℘₁℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c) “_k ℘₁1_c) “_k V)

Theorem	swapex 4742	The Swap function is a set. (Contributed by SF, 6-Jan-2015.)
⊢ Swap ∈ V

Theorem	dfsset2 4743	Express the S relationship via the set construction functors. (Contributed by SF, 7-Jan-2015.)
⊢ S = ⋃₁⋃₁((((V ×_k V) ×_k V) ∩ ^◡_k ∼ (( Ins3_k SI_k SI_k S_k ⊕ Ins2_k ( Ins3_k ( S_k ∘_k SI_k ^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V)))) ∪ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ((^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V))) ∘_k S_k ) ∪ ({{0_c}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c)) “_k S_k )

Theorem	ssetex 4744	The subset relationship is a set. (Contributed by SF, 6-Jan-2015.)
⊢ S ∈ V

Theorem	dfima2 4745	Express the image functor in terms of the set construction functions. (Contributed by SF, 7-Jan-2015.)
⊢ (A “ B) = ((((V ×_k (V ×_k V)) ∩ ∼ (( Ins3_k SI_k SI_k S_k ⊕ Ins2_k ( Ins3_k ( S_k ∘_k SI_k ^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V)))) ∪ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ((^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V))) ∘_k S_k ) ∪ ({{0_c}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁A) “_k B)

Theorem	imaexg 4746	The image of a set under a set is a set. (Contributed by SF, 7-Jan-2015.)
⊢ ((A ∈ V ∧ B ∈ W) → (A “ B) ∈ V)

Theorem	imaex 4747	The image of a set under a set is a set. (Contributed by SF, 7-Jan-2015.)
⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ (A “ B) ∈ V

Theorem	dfco1 4748	Express Quine composition via Kuratowski composition. (Contributed by SF, 7-Jan-2015.)
⊢ (A ∘ B) = ⋃₁⋃₁((((V ×_k V) ×_k V) ∩ ^◡_k ∼ (( Ins3_k SI_k SI_k S_k ⊕ Ins2_k ( Ins3_k ( S_k ∘_k SI_k ^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V)))) ∪ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ((^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V))) ∘_k S_k ) ∪ ({{0_c}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ((((V ×_k (V ×_k V)) ∩ ∼ (( Ins3_k SI_k SI_k S_k ⊕ Ins2_k ( Ins3_k ( S_k ∘_k SI_k ^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V)))) ∪ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ((^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V))) ∘_k S_k ) ∪ ({{0_c}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁A) ∘_k (((V ×_k (V ×_k V)) ∩ ∼ (( Ins3_k SI_k SI_k S_k ⊕ Ins2_k ( Ins3_k ( S_k ∘_k SI_k ^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V)))) ∪ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ((^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V))) ∘_k S_k ) ∪ ({{0_c}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁B)))

Theorem	coexg 4749	The composition of two sets is a set. (Contributed by SF, 7-Jan-2015.)
⊢ ((A ∈ V ∧ B ∈ W) → (A ∘ B) ∈ V)

Theorem	coex 4750	The composition of two sets is a set. (Contributed by SF, 7-Jan-2015.)
⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ (A ∘ B) ∈ V

Theorem	dfsi2 4751	Express singleton image in terms of the Kuratowski singleton image. (Contributed by SF, 7-Jan-2015.)
⊢ SI A = ⋃₁⋃₁((((V ×_k V) ×_k V) ∩ ^◡_k ∼ (( Ins3_k SI_k SI_k S_k ⊕ Ins2_k ( Ins3_k ( S_k ∘_k SI_k ^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V)))) ∪ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ((^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V))) ∘_k S_k ) ∪ ({{0_c}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c)) “_k SI_k (((V ×_k (V ×_k V)) ∩ ∼ (( Ins3_k SI_k SI_k S_k ⊕ Ins2_k ( Ins3_k ( S_k ∘_k SI_k ^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V)))) ∪ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ((^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V))) ∘_k S_k ) ∪ ({{0_c}} ×_k V))) “_k ℘₁℘₁1_c)) “_k ℘₁℘₁1_c))) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁A))

Theorem	siexg 4752	The singleton image of a set is a set. (Contributed by SF, 7-Jan-2015.)
⊢ (A ∈ V → SI A ∈ V)

Theorem	siex 4753	The singleton image of a set is a set. (Contributed by SF, 7-Jan-2015.)
⊢ A ∈ V ⇒ ⊢ SI A ∈ V

Theorem	elima 4754*	Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by SF, 19-Apr-2004.)
⊢ (A ∈ (B “ C) ↔ ∃x ∈ C xBA)

Theorem	elima2 4755*	Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by SF, 11-Aug-2004.)
⊢ (A ∈ (B “ C) ↔ ∃x(x ∈ C ∧ xBA))

Theorem	elima3 4756*	Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by SF, 14-Aug-1994.)
⊢ (A ∈ (B “ C) ↔ ∃x(x ∈ C ∧ ⟨x, A⟩ ∈ B))

Theorem	brssetg 4757	Binary relationship form of the subset relationship. (Contributed by SF, 11-Feb-2015.)
⊢ ((A ∈ V ∧ B ∈ W) → (A S B ↔ A ⊆ B))

Theorem	brsset 4758	Binary relationship form of the subset relationship. (Contributed by SF, 11-Feb-2015.)
⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ (A S B ↔ A ⊆ B)

Theorem	brssetsn 4759	Set membership in terms of the subset relationship. (Contributed by SF, 11-Feb-2015.)
⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ ({A} S B ↔ A ∈ B)

Theorem	opelssetsn 4760	Set membership in terms of the subset relationship. (Contributed by SF, 11-Feb-2015.)
⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ (⟨{A}, B⟩ ∈ S ↔ A ∈ B)

Theorem	brsi 4761*	Binary relationship over a singleton image. (Contributed by SF, 11-Feb-2015.)
⊢ (A SI RB ↔ ∃x∃y(A = {x} ∧ B = {y} ∧ xRy))

2.3.6 Epsilon and identity relations

Syntax	cep 4762	Extend class notation to include the epsilon relation.
class E

Syntax	cid 4763	Extend the definition of a class to include identity relation.
class I

Definition	df-eprel 4764*	Define the epsilon relation. Similar to Definition 6.22 of [TakeutiZaring] p. 30. (Contributed by SF, 5-Jan-2015.)
⊢ E = {⟨x, y⟩ ∣ x ∈ y}

Theorem	epelc 4765	The epsilon relation and the membership relation are the same. (Contributed by NM, 13-Aug-1995.)
⊢ B ∈ V ⇒ ⊢ (A E B ↔ A ∈ B)

Theorem	epel 4766	The epsilon relation and the membership relation are the same. (Contributed by NM, 13-Aug-1995.)
⊢ (x E y ↔ x ∈ y)

Definition	df-id 4767*	Define the identity relation. Definition 9.15 of [Quine] p. 64. (Contributed by SF, 5-Jan-2015.)
⊢ I = {⟨x, y⟩ ∣ x = y}

Theorem	dfid3 4768	A stronger version of df-id 4767 that doesn't require x and y to be distinct. Ordinarily, we wouldn't use this as a definition, since non-distinct dummy variables would make soundness verification more difficult (as the proof here shows). The proof can be instructive in showing how distinct variable requirements may be eliminated, a task that is not necessarily obvious. (Contributed by NM, 5-Feb-2008.) (Revised by Mario Carneiro, 18-Nov-2016.)
⊢ I = {⟨x, y⟩ ∣ x = y}

Theorem	dfid2 4769	Alternate definition of the identity relation. (Contributed by NM, 15-Mar-2007.)
⊢ I = {⟨x, x⟩ ∣ x = x}

2.3.7 Functions and relations

Syntax	cxp 4770	Extend the definition of a class to include the cross product.
class (A × B)

Syntax	ccnv 4771	Extend the definition of a class to include the converse of a class.
class ^◡A

Syntax	cdm 4772	Extend the definition of a class to include the domain of a class.
class dom A

Syntax	crn 4773	Extend the definition of a class to include the range of a class.
class ran A

Syntax	cres 4774	Extend the definition of a class to include the restriction of a class. (Read: The restriction of A to B.)
class (A ↾ B)

Syntax	wfun 4775	Extend the definition of a wff to include the function predicate. (Read: A is a function.)
wff Fun A

Syntax	wfn 4776	Extend the definition of a wff to include the function predicate with a domain. (Read: A is a function on B.)
wff A Fn B

Syntax	wf 4777	Extend the definition of a wff to include the function predicate with domain and codomain. (Read: F maps A into B.)
wff F:A–→B

Syntax	wf1 4778	Extend the definition of a wff to include one-to-one functions. (Read: F maps A one-to-one into B.) The notation ("1-1" above the arrow) is from Definition 6.15(5) of [TakeutiZaring] p. 27.
wff F:A–1-1→B

Syntax	wfo 4779	Extend the definition of a wff to include onto functions. (Read: F maps A onto B.) The notation ("onto" below the arrow) is from Definition 6.15(4) of [TakeutiZaring] p. 27.
wff F:A–onto→B

Syntax	wf1o 4780	Extend the definition of a wff to include one-to-one onto functions. (Read: F maps A one-to-one onto B.) The notation ("1-1" above the arrow and "onto" below the arrow) is from Definition 6.15(6) of [TakeutiZaring] p. 27.
wff F:A–1-1-onto→B

Syntax	cfv 4781	Extend the definition of a class to include the value of a function. (Read: The value of F at A, or "F of A.")
class (F ‘A)

Syntax	wiso 4782	Extend the definition of a wff to include the isomorphism property. (Read: H is an R, S isomorphism of A onto B.)
wff H Isom R, S (A, B)

Syntax	c2nd 4783	Extend the definition of a class to include the second function.
class 2^nd

Definition	df-xp 4784*	Define the cross product of two classes. Definition 9.11 of [Quine] p. 64. (Contributed by SF, 5-Jan-2015.)
⊢ (A × B) = {⟨x, y⟩ ∣ (x ∈ A ∧ y ∈ B)}

Definition	df-cnv 4785*	Define the converse of a class. Definition 9.12 of [Quine] p. 64. 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 SF, 5-Jan-2015.)
⊢ ^◡A = {⟨x, y⟩ ∣ yAx}

Definition	df-rn 4786	Define the range of a class. The notation "ran " is used by Enderton; other authors sometimes use script R or script W. (Contributed by SF, 5-Jan-2015.)
⊢ ran A = (A “ V)

Definition	df-dm 4787	Define the domain of a class. The notation "dom " is used by Enderton; other authors sometimes use script D. (Contributed by SF, 5-Jan-2015.)
⊢ dom A = ran ^◡A

Definition	df-res 4788	Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. (Contributed by SF, 5-Jan-2015.)
⊢ (A ↾ B) = (A ∩ (B × V))

Definition	df-fun 4789	Define a function. Definition 10.1 of [Quine] p. 65. For alternate definitions, see dffun2 5119, dffun3 5120, dffun4 5121, dffun5 5122, dffun6 5124, dffun7 5133, dffun8 5134, and dffun9 5135. (Contributed by SF, 5-Jan-2015.) (Revised by Scott Fenton, 14-Apr-2021.)
⊢ (Fun A ↔ (A ∘ ^◡A) ⊆ I )

Definition	df-fn 4790	Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 5224, dffn3 5229, dffn4 5275, and dffn5 5363. (Contributed by SF, 5-Jan-2015.)
⊢ (A Fn B ↔ (Fun A ∧ dom A = B))

Definition	df-f 4791	Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. For alternate definitions, see dff2 5419, dff3 5420, and dff4 5421. (Contributed by SF, 5-Jan-2015.)
⊢ (F:A–→B ↔ (F Fn A ∧ ran F ⊆ B))

Definition	df-f1 4792	Define a one-to-one function. For equivalent definitions see dff12 5257 and dff13 5471. Compare Definition 6.15(5) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow). (Contributed by SF, 5-Jan-2015.)
⊢ (F:A–1-1→B ↔ (F:A–→B ∧ Fun ^◡F))

Definition	df-fo 4793	Define an onto function. Definition 6.15(4) of [TakeutiZaring] p. 27. We use their notation ("onto" under the arrow). For alternate definitions, see dffo2 5273, dffo3 5422, dffo4 5423, and dffo5 5424. (Contributed by SF, 5-Jan-2015.)
⊢ (F:A–onto→B ↔ (F Fn A ∧ ran F = B))

Definition	df-f1o 4794	Define a one-to-one onto function. For equivalent definitions see dff1o2 5291, dff1o3 5292, dff1o4 5294, and dff1o5 5295. Compare Definition 6.15(6) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow and "onto" below the arrow). (Contributed by SF, 5-Jan-2015.)
⊢ (F:A–1-1-onto→B ↔ (F:A–1-1→B ∧ F:A–onto→B))

Definition	df-fv 4795*	Define the value of a function. (Contributed by SF, 5-Jan-2015.)
⊢ (F ‘A) = (℩xAFx)

Definition	df-iso 4796*	Define the isomorphism predicate. We read this as "H is an R, S isomorphism of A onto B." Normally, R and S are ordering relations on A and B respectively. Definition 6.28 of [TakeutiZaring] p. 32, whose notation is the same as ours except that R and S are subscripts. (Contributed by SF, 5-Jan-2015.)
⊢ (H Isom R, S (A, B) ↔ (H:A–1-1-onto→B ∧ ∀x ∈ A ∀y ∈ A (xRy ↔ (H ‘x)S(H ‘y))))

Definition	df-2nd 4797*	Define the 2^nd function. This function extracts the second member of an ordered pair. (Contributed by SF, 5-Jan-2015.)
⊢ 2^nd = {⟨x, y⟩ ∣ ∃z x = ⟨z, y⟩}

Theorem	xpeq1 4798	Equality theorem for cross product. (Contributed by NM, 4-Jul-1994.)
⊢ (A = B → (A × C) = (B × C))

Theorem	xpeq2 4799	Equality theorem for cross product. (Contributed by NM, 5-Jul-1994.)
⊢ (A = B → (C × A) = (C × B))

Theorem	elxpi 4800*	Membership in a cross product. Uses fewer axioms than elxp 4801. (Contributed by NM, 4-Jul-1994.)
⊢ (A ∈ (B × C) → ∃x∃y(A = ⟨x, y⟩ ∧ (x ∈ B ∧ y ∈ C)))

< Previous Next >

Page List Jump to page: Contents 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6338

< Previous Next >