Theorem oprabex

Description: Existence of an operation class abstraction. (Contributed by NM, 19-Oct-2004)

	Ref	Expression
Hypotheses	oprabex.1	|- A e. _V
	oprabex.2	|- B e. _V
	oprabex.3	|- ( ( x e. A /\ y e. B ) -> E* z ph )
	oprabex.4	|- F = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ph ) }
Assertion	oprabex	|- F e. _V

Proof

Step	Hyp	Ref	Expression
1		oprabex.1	|- A e. _V
2		oprabex.2	|- B e. _V
3		oprabex.3	|- ( ( x e. A /\ y e. B ) -> E* z ph )
4		oprabex.4	|- F = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ph ) }
5		moanimv	|- ( E* z ( ( x e. A /\ y e. B ) /\ ph ) <-> ( ( x e. A /\ y e. B ) -> E* z ph ) )
6	3 5	mpbir	|- E* z ( ( x e. A /\ y e. B ) /\ ph )
7	6	funoprab	|- Fun { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ph ) }
8	1 2	xpex	|- ( A X. B ) e. _V
9		dmoprabss	|- dom { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ph ) } C_ ( A X. B )
10	8 9	ssexi	|- dom { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ph ) } e. _V
11		funex	|- ( ( Fun { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ph ) } /\ dom { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ph ) } e. _V ) -> { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ph ) } e. _V )
12	7 10 11	mp2an	|- { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ph ) } e. _V
13	4 12	eqeltri	|- F e. _V