P. 46 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 4501-4600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	tfinltfin 4501	Ordering rule for the finite T operation. Corollary to theorem X.1.33 of [Rosser] p. 529. (Contributed by SF, 1-Feb-2015.)
|- ((M e. Nn /\ N e. Nn ) -> (<<M, N>> e. <fin <-> << Tfin M, Tfin N>> e. <fin ))
Theorem	tfinlefin 4502	Ordering rule for the finite T operation. Theorem X.1.33 of [Rosser] p. 529. (Contributed by SF, 2-Feb-2015.)
|- ((M e. Nn /\ N e. Nn ) -> (<<M, N>> e. <_fin <-> << Tfin M, Tfin N>> e. <_fin ))
Theorem	evenfinex 4503	The set of all even naturals exists. (Contributed by SF, 20-Jan-2015.)
|- Evenfin e. _V
Theorem	oddfinex 4504	The set of all odd naturals exists. (Contributed by SF, 20-Jan-2015.)
|- Oddfin e. _V
Theorem	0ceven 4505	Cardinal zero is even. (Contributed by SF, 20-Jan-2015.)
|- 0c e. Evenfin
Theorem	evennn 4506	An even finite cardinal is a finite cardinal. (Contributed by SF, 20-Jan-2015.)
|- (A e. Evenfin -> A e. Nn )
Theorem	oddnn 4507	An odd finite cardinal is a finite cardinal. (Contributed by SF, 20-Jan-2015.)
|- (A e. Oddfin -> A e. Nn )
Theorem	evennnul 4508	An even number is nonempty. (Contributed by SF, 22-Jan-2015.)
|- (A e. Evenfin -> A =/= (/))
Theorem	oddnnul 4509	An odd number is nonempty. (Contributed by SF, 22-Jan-2015.)
|- (A e. Oddfin -> A =/= (/))
Theorem	sucevenodd 4510	The successor of an even natural is odd. (Contributed by SF, 20-Jan-2015.)
|- ((A e. Evenfin /\ (A +o 1c) =/= (/)) -> (A +o 1c) e. Oddfin )
Theorem	sucoddeven 4511	The successor of an odd natural is even. (Contributed by SF, 22-Jan-2015.)
|- ((A e. Oddfin /\ (A +o 1c) =/= (/)) -> (A +o 1c) e. Evenfin )
Theorem	dfevenfin2 4512*	Alternate definition of even number. (Contributed by SF, 25-Jan-2015.)
|- Evenfin = {x | E.n e. Nn (x = (n +o n) /\ (n +o n) =/= (/))}
Theorem	dfoddfin2 4513*	Alternate definition of odd number. (Contributed by SF, 25-Jan-2015.)
|- Oddfin = {x | E.n e. Nn (x = ((n +o n) +o 1c) /\ ((n +o n) +o 1c) =/= (/))}
Theorem	evenoddnnnul 4514	Every nonempty finite cardinal is either even or odd. Theorem X.1.35 of [Rosser] p. 529. (Contributed by SF, 20-Jan-2015.)
|- ( Evenfin u. Oddfin ) = ( Nn \ {(/)})
Theorem	evenodddisjlem1 4515*	Lemma for evenodddisj 4516. Establish stratification for induction. (Contributed by SF, 25-Jan-2015.)
|- {j | ((j +o j) =/= (/) -> A.n e. Nn (((n +o n) +o 1c) =/= (/) -> (j +o j) =/= ((n +o n) +o 1c)))} e. _V
Theorem	evenodddisj 4516	The even finite cardinals and the odd ones are disjoint. Theorem X.1.36 of [Rosser] p. 529. (Contributed by SF, 22-Jan-2015.)
|- ( Evenfin i^i Oddfin ) = (/)
Theorem	eventfin 4517	If M is even , then so is Tfin M. Theorem X.1.37 of [Rosser] p. 530. (Contributed by SF, 26-Jan-2015.)
|- (M e. Evenfin -> Tfin M e. Evenfin )
Theorem	oddtfin 4518	If M is odd , then so is Tfin M. Theorem X.1.38 of [Rosser] p. 530. (Contributed by SF, 26-Jan-2015.)
|- (M e. Oddfin -> Tfin M e. Oddfin )
Theorem	nnadjoinlem1 4519*	Lemma for nnadjoin 4520. Establish stratification. (Contributed by SF, 29-Jan-2015.)
|- {n | A.l e. n (y e. ∼ U.l -> {x | E.b e. l x = (b u. {y})} e. n)} e. _V
Theorem	nnadjoin 4520*	Adjoining a new element to every member of L does not change its size. Theorem X.1.39 of [Rosser] p. 530. (Contributed by SF, 29-Jan-2015.)
|- ((N e. Nn /\ L e. N /\ X e. ∼ U.L) -> {x | E.b e. L x = (b u. {X})} e. N)
Theorem	nnadjoinpw 4521	Adjoining an element to a power class. Theorem X.1.40 of [Rosser] p. 530. (Contributed by SF, 27-Jan-2015.)
|- (((M e. Nn /\ N e. Nn ) /\ (A e. M /\ X e. ∼ A) /\ ~PA e. N) -> ~P(A u. {X}) e. (N +o N))
Theorem	nnpweqlem1 4522*	Lemma for nnpweq 4523. Establish stratification for induction. (Contributed by SF, 26-Jan-2015.)
|- {m | A.a e. m A.b e. m E.n e. Nn (~Pa e. n /\ ~Pb e. n)} e. _V
Theorem	nnpweq 4523*	If two sets are the same finite size, then so are their power classes. Theorem X.1.41 of [Rosser] p. 530. (Contributed by SF, 26-Jan-2015.)
|- ((M e. Nn /\ A e. M /\ B e. M) -> E.n e. Nn (~PA e. n /\ ~PB e. n))
Theorem	srelk 4524	Binary relationship form of the Sfin relationship. (Contributed by SF, 23-Jan-2015.)
|- A e. _V   &   |- B e. _V   =>   |- (<<A, B>> e. (( Nn X.k Nn ) i^i (( Ins3k (( Ins3k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins2k Sk )"k~P1 ~P1 1c) i^i Ins2k (( Ins3k SIk ∼ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 1c) i^i Ins2k Sk )"k~P1 ~P1 1c))"k~P1 ~P1 ~P1 1c)) <-> Sfin (A, B))
Theorem	srelkex 4525	The expression at the core of srelk 4524 exists. (Contributed by SF, 30-Jan-2015.)
|- (( Nn X.k Nn ) i^i (( Ins3k (( Ins3k SIk ((~P1c X.k _V) \ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 ~P1 1c)) i^i Ins2k Sk )"k~P1 ~P1 1c) i^i Ins2k (( Ins3k SIk ∼ (( Ins3k Sk (+) Ins2k SIk Sk )"k~P1 ~P1 1c) i^i Ins2k Sk )"k~P1 ~P1 1c))"k~P1 ~P1 ~P1 1c)) e. _V
Theorem	sfineq1 4526	Equality theorem for the finite S relationship. (Contributed by SF, 27-Jan-2015.)
|- (A = B -> ( Sfin (A, C) <-> Sfin (B, C)))
Theorem	sfineq2 4527	Equality theorem for the finite S relationship. (Contributed by SF, 27-Jan-2015.)
|- (A = B -> ( Sfin (C, A) <-> Sfin (C, B)))
Theorem	sfin01 4528	Zero and one satisfy Sfin. Theorem X.1.42 of [Rosser] p. 530. (Contributed by SF, 30-Jan-2015.)
|- Sfin (0c, 1c)
Theorem	sfin112 4529	Equality law for the finite S operator. Theorem X.1.43 of [Rosser] p. 530. (Contributed by SF, 27-Jan-2015.)
|- (( Sfin (M, N) /\ Sfin (M, P)) -> N = P)
Theorem	sfindbl 4530*	If the unit power set of a set is in the successor of a finite cardinal, then there is a natural that is smaller than the finite cardinal and whose double is smaller than the successor of the cardinal. Theorem X.1.44 of [Rosser] p. 531. (Contributed by SF, 30-Jan-2015.)
|- ((M e. Nn /\ ~P1 A e. (M +o 1c)) -> E.n e. Nn ( Sfin (M, n) /\ Sfin ((M +o 1c), (n +o n))))
Theorem	sfintfinlem1 4531*	Lemma for sfintfin 4532. Set up induction stratification. (Contributed by SF, 31-Jan-2015.)
|- {m | A.n( Sfin (m, n) -> Sfin ( Tfin m, Tfin n))} e. _V
Theorem	sfintfin 4532	If two numbers obey Sfin, then do their T raisings. Theorem X.1.45 of [Rosser] p. 532. (Contributed by SF, 30-Jan-2015.)
|- ( Sfin (M, N) -> Sfin ( Tfin M, Tfin N))
Theorem	tfinnnlem1 4533*	Lemma for tfinnn 4534. Establish stratification. (Contributed by SF, 30-Jan-2015.)
|- {n | A.y e. n (y C_ Nn -> {a | E.x e. y a = Tfin x} e. Tfin n)} e. _V
Theorem	tfinnn 4534*	T-raising of a set of naturals. Theorem X.1.46 of [Rosser] p. 532. (Contributed by SF, 30-Jan-2015.)
|- ((N e. Nn /\ A C_ Nn /\ A e. N) -> {a | E.x e. A a = Tfin x} e. Tfin N)
Theorem	sfinltfin 4535	Ordering law for finite smaller than. Theorem X.1.47 of [Rosser] p. 532. (Contributed by SF, 30-Jan-2015.)
|- ((( Sfin (M, N) /\ Sfin (P, Q)) /\ <<M, P>> e. <fin ) -> <<N, Q>> e. <fin )
Theorem	sfin111 4536	The finite smaller relationship is one-to-one in its first argument. Theorem X.1.48 of [Rosser] p. 533. (Contributed by SF, 29-Jan-2015.)
|- (( Sfin (M, P) /\ Sfin (N, P)) -> M = N)
Theorem	spfinex 4537	Spfin is a set. (Contributed by SF, 20-Jan-2015.)
|- Spfin e. _V
Theorem	ncvspfin 4538	The cardinality of the universe is in the finite Sp set. Theorem X.1.49 of [Rosser] p. 534. (Contributed by SF, 27-Jan-2015.)
|- Ncfin _V e. Spfin
Theorem	spfinsfincl 4539	If X is in Spfin and Z is smaller than X, then Z is also in Spfin. Theorem X.1.50 of [Rosser] p. 534. (Contributed by SF, 27-Jan-2015.)
|- ((X e. Spfin /\ Sfin (Z, X)) -> Z e. Spfin )
Theorem	spfininduct 4540*	Inductive principle for Spfin. Theorem X.1.51 of [Rosser] p. 534. (Contributed by SF, 27-Jan-2015.)
|- ((B e. V /\ Ncfin _V e. B /\ A.x e. Spfin A.z((x e. B /\ Sfin (z, x)) -> z e. B)) -> Spfin C_ B)
Theorem	vfinspnn 4541	If the universe is finite, then Spfin is a subset of the nonempty naturals. Theorem X.1.53 of [Rosser] p. 534. (Contributed by SF, 27-Jan-2015.)
|- (_V e. Fin -> Spfin C_ ( Nn \ {(/)}))
Theorem	1cvsfin 4542	If the universe is finite, then Ncfin 1c is the base two log of Ncfin _V. Theorem X.1.54 of [Rosser] p. 534. (Contributed by SF, 29-Jan-2015.)
|- (_V e. Fin -> Sfin ( Ncfin 1c, Ncfin _V))
Theorem	1cspfin 4543	If the universe is finite, then the size of 1c is in Spfin. Corollary of Theorem X.1.54 of [Rosser] p. 534. (Contributed by SF, 29-Jan-2015.)
|- (_V e. Fin -> Ncfin 1c e. Spfin )
Theorem	tncveqnc1fin 4544	If the universe is finite, then the T-raising of the size of the universe is equal to the size of 1c. Theorem X.1.55 of [Rosser] p. 534. (Contributed by SF, 29-Jan-2015.)
|- (_V e. Fin -> Tfin Ncfin _V = Ncfin 1c)
Theorem	t1csfin1c 4545	If the universe is finite, then the T-raising of the size of 1c is smaller than the size itself. Corollary of theorem X.1.56 of [Rosser] p. 534. (Contributed by SF, 29-Jan-2015.)
|- (_V e. Fin -> Sfin ( Tfin Ncfin 1c, Ncfin 1c))
Theorem	vfintle 4546	If the universe is finite, then the T-raising of all nonempty naturals are no greater than the size of 1c. Theorem X.1.56 of [Rosser] p. 534. (Contributed by SF, 30-Jan-2015.)
|- ((_V e. Fin /\ N e. Nn /\ N =/= (/)) -> << Tfin N, Ncfin 1c>> e. <_fin )
Theorem	vfin1cltv 4547	If the universe is finite, then 1c is strictly smaller than the universe. Theorem X.1.57 of [Rosser] p. 534. (Contributed by SF, 30-Jan-2015.)
|- (_V e. Fin -> << Ncfin 1c, Ncfin _V>> e. <fin )
Theorem	vfinncvntnn 4548	If the universe is finite, then the size of the universe is not the T-raising of a natural. Theorem X.1.58 of [Rosser] p. 534. (Contributed by SF, 29-Jan-2015.)
|- ((_V e. Fin /\ N e. Nn ) -> Tfin N =/= Ncfin _V)
Theorem	vfinncvntsp 4549*	If the universe is finite, then its size is not a T raising of an element of Spfin. Corollary of theorem X.1.58 of [Rosser] p. 534. (Contributed by SF, 27-Jan-2015.)
|- (_V e. Fin -> -. Ncfin _V e. {a | E.x e. Spfin a = Tfin x})
Theorem	vfinspsslem1 4550*	Lemma for vfinspss 4551. Establish part of the inductive step. (Contributed by SF, 3-Feb-2015.)
|- (((_V e. Fin /\ Tfin n e. Spfin ) /\ (n e. Spfin /\ Sfin (z, Tfin n))) -> E.x e. Spfin z = Tfin x)
Theorem	vfinspss 4551*	If the universe is finite, then Spfin is a subset of its T raisings and the cardinality of the universe. Theorem X.1.59 of [Rosser] p. 534. (Contributed by SF, 29-Jan-2015.)
|- (_V e. Fin -> Spfin C_ ({a | E.x e. Spfin a = Tfin x} u. { Ncfin _V}))
Theorem	vfinspclt 4552	If the universe is finite, then Spfin is closed under T-raising. Theorem X.1.60 of [Rosser] p. 536. (Contributed by SF, 30-Jan-2015.)
|- ((_V e. Fin /\ X e. Spfin ) -> Tfin X e. Spfin )
Theorem	vfinspeqtncv 4553*	If the universe is finite, then Spfin is equal to its T raisings and the cardinality of the universe. Theorem X.1.61 of [Rosser] p. 536. (Contributed by SF, 29-Jan-2015.)
|- (_V e. Fin -> Spfin = ({a | E.x e. Spfin a = Tfin x} u. { Ncfin _V}))
Theorem	vfinncsp 4554	If the universe is finite, then the size of Spfin is equal to the successor of its T-raising. Theorem X.1.62 of [Rosser] p. 536. (Contributed by SF, 20-Jan-2015.)
|- (_V e. Fin -> Ncfin Spfin = ( Tfin Ncfin Spfin +o 1c))
Theorem	vinf 4555	The universe is infinite. Theorem X.1.63 of [Rosser] p. 536. (Contributed by SF, 20-Jan-2015.)
|- -. _V e. Fin
Theorem	nulnnn 4556	The empty class is not a natural. Theorem X.1.65 of [Rosser] p. 536. (Contributed by SF, 20-Jan-2015.)
|- -. (/) e. Nn
Theorem	peano4 4557	The successor operation is one-to-one over the finite cardinals. Theorem X.1.66 of [Rosser] p. 537. (Contributed by SF, 20-Jan-2015.)
|- ((M e. Nn /\ N e. Nn /\ (M +o 1c) = (N +o 1c)) -> M = N)
Theorem	suc11nnc 4558	Successor cancellation law for finite cardinals. (Contributed by SF, 3-Feb-2015.)
|- ((M e. Nn /\ N e. Nn ) -> ((M +o 1c) = (N +o 1c) <-> M = N))
Theorem	addccan2 4559	Cancellation law for natural addition. (Contributed by SF, 3-Feb-2015.)
|- ((M e. Nn /\ N e. Nn /\ P e. Nn ) -> ((M +o N) = (M +o P) <-> N = P))
Theorem	addccan1 4560	Cancellation law for natural addition. (Contributed by SF, 3-Feb-2015.)
|- ((M e. Nn /\ N e. Nn /\ P e. Nn ) -> ((M +o P) = (N +o P) <-> M = N))
2.3  Ordered Pairs, Relationships, and Functions
2.3.1  Ordered Pairs
Syntax	cop 4561	Declare the syntax for an ordered pair.
class <.A, B>.
Syntax	cphi 4562	Declare the syntax for the Phi operation.
class Phi A
Syntax	cproj1 4563	Declare the syntax for the first projection operation.
class Proj1 A
Syntax	cproj2 4564	Declare the syntax for the second projection operation.
class Proj2 A
Definition	df-phi 4565*	Define the phi operator. This operation increments all the naturals in A and leaves all its other members the same. (Contributed by SF, 3-Feb-2015.)
|- Phi A = {y | E.x e. A y = if(x e. Nn , (x +o 1c), x)}
Definition	df-op 4566*	Define the type-level ordered pair. Definition from [Rosser] p. 281. (Contributed by SF, 3-Feb-2015.)
|- <.A, B>. = ({x | E.y e. A x = Phi y} u. {x | E.y e. B x = ( Phi y u. {0c})})
Definition	df-proj1 4567*	Define the first projection operation. This operation recovers the first element of an ordered pair. Definition from [Rosser] p. 281. (Contributed by SF, 3-Feb-2015.)
|- Proj1 A = {x | Phi x e. A}
Definition	df-proj2 4568*	Define the second projection operation. This operation recovers the second element of an ordered pair. Definition from [Rosser] p. 281. (Contributed by SF, 3-Feb-2015.)
|- Proj2 A = {x | ( Phi x u. {0c}) e. A}
Theorem	dfphi2 4569	Express the phi operator in terms of the Kuratowski set construction functions. (Contributed by SF, 3-Feb-2015.)
|- Phi A = (((Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) i^i ( Nn X.k _V)) u. ( _I_kk i^i ( ∼ Nn X.k _V)))"kA)
Theorem	phieq 4570	Equality law for the Phi operation. (Contributed by SF, 3-Feb-2015.)
|- (A = B -> Phi A = Phi B)
Theorem	phiexg 4571	The phi operator preserves sethood. (Contributed by SF, 3-Feb-2015.)
|- (A e. V -> Phi A e. _V)
Theorem	phiex 4572	The phi operator preserves sethood. (Contributed by SF, 3-Feb-2015.)
|- A e. _V   =>   |- Phi A e. _V
Theorem	dfop2lem1 4573*	Lemma for dfop2 4575 and dfproj22 4577. (Contributed by SF, 2-Jan-2015.)
|- (<<x, y>> e. ∼ (( Ins2k Sk (+) Ins3k ((`'kImagek((Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) i^i ( Nn X.k _V)) u. ( _I_kk i^i ( ∼ Nn X.k _V))) o.k Sk ) u. ({{0c}} X.k _V)))"k~P1 ~P1 1c) <-> y = ( Phi x u. {0c}))
Theorem	dfop2lem2 4574*	Lemma for dfop2 4575. (Contributed by SF, 2-Jan-2015.)
|- ( ∼ (( Ins2k Sk (+) Ins3k ((`'kImagek((Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) i^i ( Nn X.k _V)) u. ( _I_kk i^i ( ∼ Nn X.k _V))) o.k Sk ) u. ({{0c}} X.k _V)))"k~P1 ~P1 1c)"kB) = {x | E.y e. B x = ( Phi y u. {0c})}
Theorem	dfop2 4575	Express the ordered pair via the set construction functors. (Contributed by SF, 2-Jan-2015.)
|- <.A, B>. = ((Imagek((Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) i^i ( Nn X.k _V)) u. ( _I_kk i^i ( ∼ Nn X.k _V)))"kA) u. ( ∼ (( Ins2k Sk (+) Ins3k ((`'kImagek((Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) i^i ( Nn X.k _V)) u. ( _I_kk i^i ( ∼ Nn X.k _V))) o.k Sk ) u. ({{0c}} X.k _V)))"k~P1 ~P1 1c)"kB))
Theorem	dfproj12 4576	Express the first projection operator via the set construction functors. (Contributed by SF, 2-Jan-2015.)
|- Proj1 A = (`'kImagek((Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) i^i ( Nn X.k _V)) u. ( _I_kk i^i ( ∼ Nn X.k _V)))"kA)
Theorem	dfproj22 4577	Express the second projection operator via the set construction functors. (Contributed by SF, 2-Jan-2015.)
|- Proj2 A = (`'k ∼ (( Ins2k Sk (+) Ins3k ((`'kImagek((Imagek(( Ins3k ∼ (( Ins3k Sk i^i Ins2k Sk )"k~P1 ~P1 1c) \ (( Ins2k Ins2k Sk (+) ( Ins2k Ins3k Sk u. Ins3k SIk SIk Sk ))"k~P1 ~P1 ~P1 ~P1 1c))"k~P1 ~P1 1c) i^i ( Nn X.k _V)) u. ( _I_kk i^i ( ∼ Nn X.k _V))) o.k Sk ) u. ({{0c}} X.k _V)))"k~P1 ~P1 1c)"kA)
Theorem	opeq1 4578	Equality theorem for ordered pairs. (Contributed by SF, 2-Jan-2015.)
|- (A = B -> <.A, C>. = <.B, C>.)
Theorem	opeq2 4579	Equality theorem for ordered pairs. (Contributed by SF, 2-Jan-2015.)
|- (A = B -> <.C, A>. = <.C, B>.)
Theorem	opeq12 4580	Equality theorem for ordered pairs. (Contributed by SF, 2-Jan-2015.)
|- ((A = B /\ C = D) -> <.A, C>. = <.B, D>.)
Theorem	opeq1i 4581	Equality inference for ordered pairs. (Contributed by SF, 16-Dec-2006.)
|- A = B   =>   |- <.A, C>. = <.B, C>.
Theorem	opeq2i 4582	Equality inference for ordered pairs. (Contributed by SF, 16-Dec-2006.)
|- A = B   =>   |- <.C, A>. = <.C, B>.
Theorem	opeq12i 4583	Equality inference for ordered pairs. (The proof was shortened by Eric Schmidt, 4-Apr-2007.) (Contributed by SF, 16-Dec-2006.)
|- A = B   &   |- C = D   =>   |- <.A, C>. = <.B, D>.
Theorem	opeq1d 4584	Equality deduction for ordered pairs. (Contributed by SF, 16-Dec-2006.)
|- (ph -> A = B)   =>   |- (ph -> <.A, C>. = <.B, C>.)
Theorem	opeq2d 4585	Equality deduction for ordered pairs. (Contributed by SF, 16-Dec-2006.)
|- (ph -> A = B)   =>   |- (ph -> <.C, A>. = <.C, B>.)
Theorem	opeq12d 4586	Equality deduction for ordered pairs. (The proof was shortened by Andrew Salmon, 29-Jun-2011.) (Contributed by SF, 16-Dec-2006.) (Revised by SF, 29-Jun-2011.)
|- (ph -> A = B)   &   |- (ph -> C = D)   =>   |- (ph -> <.A, C>. = <.B, D>.)
Theorem	opexg 4587	An ordered pair of two sets is a set. (Contributed by SF, 2-Jan-2015.)
|- ((A e. V /\ B e. W) -> <.A, B>. e. _V)
Theorem	opex 4588	An ordered pair of two sets is a set. (Contributed by SF, 5-Jan-2015.)
|- A e. _V   &   |- B e. _V   =>   |- <.A, B>. e. _V
Theorem	proj1eq 4589	Equality theorem for first projection operator. (Contributed by SF, 2-Jan-2015.)
|- (A = B -> Proj1 A = Proj1 B)
Theorem	proj2eq 4590	Equality theorem for second projection operator. (Contributed by SF, 2-Jan-2015.)
|- (A = B -> Proj2 A = Proj2 B)
Theorem	proj1exg 4591	The first projection of a set is a set. (Contributed by SF, 2-Jan-2015.)
|- (A e. V -> Proj1 A e. _V)
Theorem	proj2exg 4592	The second projection of a set is a set. (Contributed by SF, 2-Jan-2015.)
|- (A e. V -> Proj2 A e. _V)
Theorem	proj1ex 4593	The first projection of a set is a set. (Contributed by Scott Fenton, 16-Apr-2021.)
|- A e. _V   =>   |- Proj1 A e. _V
Theorem	proj2ex 4594	The second projection of a set is a set. (Contributed by Scott Fenton, 16-Apr-2021.)
|- A e. _V   =>   |- Proj2 A e. _V
Theorem	phi11lem1 4595	Lemma for phi11 4596. (Contributed by SF, 3-Feb-2015.)
|- ( Phi A = Phi B -> A C_ B)
Theorem	phi11 4596	The phi operator is one-to-one. Theorem X.2.2 of [Rosser] p. 282. (Contributed by SF, 3-Feb-2015.)
|- (A = B <-> Phi A = Phi B)
Theorem	0cnelphi 4597	Cardinal zero is not a member of a phi operation. Theorem X.2.3 of [Rosser] p. 282. (Contributed by SF, 3-Feb-2015.)
|- -. 0c e. Phi A
Theorem	phi011lem1 4598	Lemma for phi011 4599. (Contributed by SF, 3-Feb-2015.)
|- (( Phi A u. {0c}) = ( Phi B u. {0c}) -> Phi A C_ Phi B)
Theorem	phi011 4599	( Phi A u. {0c}) is one-to-one. Theorem X.2.4 of [Rosser] p. 282. (Contributed by SF, 3-Feb-2015.)
|- (A = B <-> ( Phi A u. {0c}) = ( Phi B u. {0c}))
Theorem	proj1op 4600	The first projection operator applied to an ordered pair yields its first member. Theorem X.2.7 of [Rosser] p. 282. (Contributed by SF, 3-Feb-2015.)
|- Proj1 <.A, B>. = A