Theorem frins2f

Description: Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 6-Feb-2011) (Revised by Mario Carneiro, 11-Dec-2016)

	Ref	Expression
Hypotheses	frins2f.1	⊢ 𝑅 Fr 𝐴
	frins2f.2	⊢ 𝑅 Se 𝐴
	frins2f.3	⊢ Ⅎ 𝑦 𝜓
	frins2f.4	⊢ ( 𝑦 = 𝑧 → ( 𝜑 ↔ 𝜓 ) )
	frins2f.5	⊢ ( 𝑦 ∈ 𝐴 → ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑦 ) 𝜓 → 𝜑 ) )
Assertion	frins2f	⊢ ( 𝑦 ∈ 𝐴 → 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		frins2f.1	⊢ 𝑅 Fr 𝐴
2		frins2f.2	⊢ 𝑅 Se 𝐴
3		frins2f.3	⊢ Ⅎ 𝑦 𝜓
4		frins2f.4	⊢ ( 𝑦 = 𝑧 → ( 𝜑 ↔ 𝜓 ) )
5		frins2f.5	⊢ ( 𝑦 ∈ 𝐴 → ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑦 ) 𝜓 → 𝜑 ) )
6	5 3 4	frins2fg	⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) → ∀ 𝑦 ∈ 𝐴 𝜑 )
7	1 2 6	mp2an	⊢ ∀ 𝑦 ∈ 𝐴 𝜑
8	7	rspec	⊢ ( 𝑦 ∈ 𝐴 → 𝜑 )