Theorem bnj106

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj106.1	⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
	bnj106.2	⊢ 𝐹 ∈ V
Assertion	bnj106	⊢ ( [ 𝐹 / 𝑓 ] [ 1o / 𝑛 ] 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )

Proof

Step	Hyp	Ref	Expression
1		bnj106.1	⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
2		bnj106.2	⊢ 𝐹 ∈ V
3		bnj105	⊢ 1o ∈ V
4	1 3	bnj92	⊢ ( [ 1o / 𝑛 ] 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
5	4	sbcbii	⊢ ( [ 𝐹 / 𝑓 ] [ 1o / 𝑛 ] 𝜓 ↔ [ 𝐹 / 𝑓 ] ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
6		fveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ suc 𝑖 ) = ( 𝐹 ‘ suc 𝑖 ) )
7		fveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑖 ) )
8	7	bnj1113	⊢ ( 𝑓 = 𝐹 → ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
9	6 8	eqeq12d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ↔ ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
10	9	imbi2d	⊢ ( 𝑓 = 𝐹 → ( ( suc 𝑖 ∈ 1o → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ( suc 𝑖 ∈ 1o → ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
11	10	ralbidv	⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
12	2 11	sbcie	⊢ ( [ 𝐹 / 𝑓 ] ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
13	5 12	bitri	⊢ ( [ 𝐹 / 𝑓 ] [ 1o / 𝑛 ] 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )