Theorem fnwe2val

Description: Lemma for fnwe2 . Substitute variables. (Contributed by Stefan O'Rear, 19-Jan-2015)

	Ref	Expression
Hypotheses	fnwe2.su	$$⊢z=F\left(x\right)\to S=U$$
	fnwe2.t	$$⊢T=\left\{⟨x,y⟩|\left(F\left(x\right)RF\left(y\right)\vee \left(F\left(x\right)=F\left(y\right)\wedge xUy\right)\right)\right\}$$
Assertion	fnwe2val	$$⊢aTb\leftrightarrow \left(F\left(a\right)RF\left(b\right)\vee \left(F\left(a\right)=F\left(b\right)\wedge a⦋F\left(a\right)/z⦌Sb\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		fnwe2.su	$$⊢z=F\left(x\right)\to S=U$$
2		fnwe2.t	$$⊢T=\left\{⟨x,y⟩|\left(F\left(x\right)RF\left(y\right)\vee \left(F\left(x\right)=F\left(y\right)\wedge xUy\right)\right)\right\}$$
3		vex	$$⊢a\in \mathrm{V}$$
4		vex	$$⊢b\in \mathrm{V}$$
5		fveq2	$$⊢x=a\to F\left(x\right)=F\left(a\right)$$
6		fveq2	$$⊢y=b\to F\left(y\right)=F\left(b\right)$$
7	5 6	breqan12d	$$⊢\left(x=a\wedge y=b\right)\to \left(F\left(x\right)RF\left(y\right)\leftrightarrow F\left(a\right)RF\left(b\right)\right)$$
8	5 6	eqeqan12d	$$⊢\left(x=a\wedge y=b\right)\to \left(F\left(x\right)=F\left(y\right)\leftrightarrow F\left(a\right)=F\left(b\right)\right)$$
9		simpl	$$⊢\left(x=a\wedge y=b\right)\to x=a$$
10		fvex	$$⊢F\left(x\right)\in \mathrm{V}$$
11	10 1	csbie	$$⊢⦋F\left(x\right)/z⦌S=U$$
12	5	csbeq1d	$$⊢x=a\to ⦋F\left(x\right)/z⦌S=⦋F\left(a\right)/z⦌S$$
13	11 12	syl5eqr	$$⊢x=a\to U=⦋F\left(a\right)/z⦌S$$
14	13	adantr	$$⊢\left(x=a\wedge y=b\right)\to U=⦋F\left(a\right)/z⦌S$$
15		simpr	$$⊢\left(x=a\wedge y=b\right)\to y=b$$
16	9 14 15	breq123d	$$⊢\left(x=a\wedge y=b\right)\to \left(xUy\leftrightarrow a⦋F\left(a\right)/z⦌Sb\right)$$
17	8 16	anbi12d	$$⊢\left(x=a\wedge y=b\right)\to \left(\left(F\left(x\right)=F\left(y\right)\wedge xUy\right)\leftrightarrow \left(F\left(a\right)=F\left(b\right)\wedge a⦋F\left(a\right)/z⦌Sb\right)\right)$$
18	7 17	orbi12d	$$⊢\left(x=a\wedge y=b\right)\to \left(\left(F\left(x\right)RF\left(y\right)\vee \left(F\left(x\right)=F\left(y\right)\wedge xUy\right)\right)\leftrightarrow \left(F\left(a\right)RF\left(b\right)\vee \left(F\left(a\right)=F\left(b\right)\wedge a⦋F\left(a\right)/z⦌Sb\right)\right)\right)$$
19	3 4 18 2	braba	$$⊢aTb\leftrightarrow \left(F\left(a\right)RF\left(b\right)\vee \left(F\left(a\right)=F\left(b\right)\wedge a⦋F\left(a\right)/z⦌Sb\right)\right)$$