Theorem ov2gf

Description: The value of an operation class abstraction. A version of ovmpog using bound-variable hypotheses. (Contributed by NM, 17-Aug-2006) (Revised by Mario Carneiro, 19-Dec-2013)

	Ref	Expression
Hypotheses	ov2gf.a	$$⊢\underset{\_}{Ⅎ}xA$$
	ov2gf.c	$$⊢\underset{\_}{Ⅎ}yA$$
	ov2gf.d	$$⊢\underset{\_}{Ⅎ}yB$$
	ov2gf.1	$$⊢\underset{\_}{Ⅎ}xG$$
	ov2gf.2	$$⊢\underset{\_}{Ⅎ}yS$$
	ov2gf.3	$$⊢x=A\to R=G$$
	ov2gf.4	$$⊢y=B\to G=S$$
	ov2gf.5	$$⊢F=\left(x\in C,y\in D⟼R\right)$$
Assertion	ov2gf	$$⊢\left(A\in C\wedge B\in D\wedge S\in H\right)\to AFB=S$$

Proof

Step	Hyp	Ref	Expression
1		ov2gf.a	$$⊢\underset{\_}{Ⅎ}xA$$
2		ov2gf.c	$$⊢\underset{\_}{Ⅎ}yA$$
3		ov2gf.d	$$⊢\underset{\_}{Ⅎ}yB$$
4		ov2gf.1	$$⊢\underset{\_}{Ⅎ}xG$$
5		ov2gf.2	$$⊢\underset{\_}{Ⅎ}yS$$
6		ov2gf.3	$$⊢x=A\to R=G$$
7		ov2gf.4	$$⊢y=B\to G=S$$
8		ov2gf.5	$$⊢F=\left(x\in C,y\in D⟼R\right)$$
9		elex	$$⊢S\in H\to S\in \mathrm{V}$$
10	4	nfel1	$$⊢ℲxG\in \mathrm{V}$$
11		nfmpo1	$$⊢\underset{\_}{Ⅎ}x\left(x\in C,y\in D⟼R\right)$$
12	8 11	nfcxfr	$$⊢\underset{\_}{Ⅎ}xF$$
13		nfcv	$$⊢\underset{\_}{Ⅎ}xy$$
14	1 12 13	nfov	$$⊢\underset{\_}{Ⅎ}x\left(AFy\right)$$
15	14 4	nfeq	$$⊢ℲxAFy=G$$
16	10 15	nfim	$$⊢Ⅎx\left(G\in \mathrm{V}\to AFy=G\right)$$
17	5	nfel1	$$⊢ℲyS\in \mathrm{V}$$
18		nfmpo2	$$⊢\underset{\_}{Ⅎ}y\left(x\in C,y\in D⟼R\right)$$
19	8 18	nfcxfr	$$⊢\underset{\_}{Ⅎ}yF$$
20	2 19 3	nfov	$$⊢\underset{\_}{Ⅎ}y\left(AFB\right)$$
21	20 5	nfeq	$$⊢ℲyAFB=S$$
22	17 21	nfim	$$⊢Ⅎy\left(S\in \mathrm{V}\to AFB=S\right)$$
23	6	eleq1d	$$⊢x=A\to \left(R\in \mathrm{V}\leftrightarrow G\in \mathrm{V}\right)$$
24		oveq1	$$⊢x=A\to xFy=AFy$$
25	24 6	eqeq12d	$$⊢x=A\to \left(xFy=R\leftrightarrow AFy=G\right)$$
26	23 25	imbi12d	$$⊢x=A\to \left(\left(R\in \mathrm{V}\to xFy=R\right)\leftrightarrow \left(G\in \mathrm{V}\to AFy=G\right)\right)$$
27	7	eleq1d	$$⊢y=B\to \left(G\in \mathrm{V}\leftrightarrow S\in \mathrm{V}\right)$$
28		oveq2	$$⊢y=B\to AFy=AFB$$
29	28 7	eqeq12d	$$⊢y=B\to \left(AFy=G\leftrightarrow AFB=S\right)$$
30	27 29	imbi12d	$$⊢y=B\to \left(\left(G\in \mathrm{V}\to AFy=G\right)\leftrightarrow \left(S\in \mathrm{V}\to AFB=S\right)\right)$$
31	8	ovmpt4g	$$⊢\left(x\in C\wedge y\in D\wedge R\in \mathrm{V}\right)\to xFy=R$$
32	31	3expia	$$⊢\left(x\in C\wedge y\in D\right)\to \left(R\in \mathrm{V}\to xFy=R\right)$$
33	1 2 3 16 22 26 30 32	vtocl2gaf	$$⊢\left(A\in C\wedge B\in D\right)\to \left(S\in \mathrm{V}\to AFB=S\right)$$
34	9 33	syl5	$$⊢\left(A\in C\wedge B\in D\right)\to \left(S\in H\to AFB=S\right)$$
35	34	3impia	$$⊢\left(A\in C\wedge B\in D\wedge S\in H\right)\to AFB=S$$