Theorem fnwe2val

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

	Ref	Expression
Hypotheses	fnwe2.su	⊢ ( 𝑧 = ( 𝐹 ‘ 𝑥 ) → 𝑆 = 𝑈 )
	fnwe2.t	⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐹 ‘ 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 𝑈 𝑦 ) ) }
Assertion	fnwe2val	⊢ ( 𝑎 𝑇 𝑏 ↔ ( ( 𝐹 ‘ 𝑎 ) 𝑅 ( 𝐹 ‘ 𝑏 ) ∨ ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ∧ 𝑎 ⦋ ( 𝐹 ‘ 𝑎 ) / 𝑧 ⦌ 𝑆 𝑏 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fnwe2.su	⊢ ( 𝑧 = ( 𝐹 ‘ 𝑥 ) → 𝑆 = 𝑈 )
2		fnwe2.t	⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐹 ‘ 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 𝑈 𝑦 ) ) }
3		vex	⊢ 𝑎 ∈ V
4		vex	⊢ 𝑏 ∈ V
5		fveq2	⊢ ( 𝑥 = 𝑎 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑎 ) )
6		fveq2	⊢ ( 𝑦 = 𝑏 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑏 ) )
7	5 6	breqan12d	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑎 ) 𝑅 ( 𝐹 ‘ 𝑏 ) ) )
8	5 6	eqeqan12d	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) )
9		simpl	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → 𝑥 = 𝑎 )
10		fvex	⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
11	10 1	csbie	⊢ ⦋ ( 𝐹 ‘ 𝑥 ) / 𝑧 ⦌ 𝑆 = 𝑈
12	5	csbeq1d	⊢ ( 𝑥 = 𝑎 → ⦋ ( 𝐹 ‘ 𝑥 ) / 𝑧 ⦌ 𝑆 = ⦋ ( 𝐹 ‘ 𝑎 ) / 𝑧 ⦌ 𝑆 )
13	11 12	eqtr3id	⊢ ( 𝑥 = 𝑎 → 𝑈 = ⦋ ( 𝐹 ‘ 𝑎 ) / 𝑧 ⦌ 𝑆 )
14	13	adantr	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → 𝑈 = ⦋ ( 𝐹 ‘ 𝑎 ) / 𝑧 ⦌ 𝑆 )
15		simpr	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → 𝑦 = 𝑏 )
16	9 14 15	breq123d	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( 𝑥 𝑈 𝑦 ↔ 𝑎 ⦋ ( 𝐹 ‘ 𝑎 ) / 𝑧 ⦌ 𝑆 𝑏 ) )
17	8 16	anbi12d	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 𝑈 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ∧ 𝑎 ⦋ ( 𝐹 ‘ 𝑎 ) / 𝑧 ⦌ 𝑆 𝑏 ) ) )
18	7 17	orbi12d	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐹 ‘ 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 𝑈 𝑦 ) ) ↔ ( ( 𝐹 ‘ 𝑎 ) 𝑅 ( 𝐹 ‘ 𝑏 ) ∨ ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ∧ 𝑎 ⦋ ( 𝐹 ‘ 𝑎 ) / 𝑧 ⦌ 𝑆 𝑏 ) ) ) )
19	3 4 18 2	braba	⊢ ( 𝑎 𝑇 𝑏 ↔ ( ( 𝐹 ‘ 𝑎 ) 𝑅 ( 𝐹 ‘ 𝑏 ) ∨ ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ∧ 𝑎 ⦋ ( 𝐹 ‘ 𝑎 ) / 𝑧 ⦌ 𝑆 𝑏 ) ) )