This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - add the Axiom of Infinity Well-Founded Induction frins2
Description: Well-Founded Induction schema, using implicit substitution.
(Contributed by Scott Fenton , 8-Feb-2011) (Revised by Mario Carneiro , 26-Jun-2015)
Ref
Expression
Hypotheses
frins2.1 ⊢ ( 𝑦 ∈ 𝐴 → ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑦 ) 𝜓 → 𝜑 ) )
frins2.3 ⊢ ( 𝑦 = 𝑧 → ( 𝜑 ↔ 𝜓 ) )
Assertion
frins2 ⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) → ∀ 𝑦 ∈ 𝐴 𝜑 )
Proof
Step
Hyp
Ref
Expression
1
frins2.1 ⊢ ( 𝑦 ∈ 𝐴 → ( ∀ 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑦 ) 𝜓 → 𝜑 ) )
2
frins2.3 ⊢ ( 𝑦 = 𝑧 → ( 𝜑 ↔ 𝜓 ) )
3
nfv ⊢ Ⅎ 𝑦 𝜓
4
1 3 2
frins2f ⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) → ∀ 𝑦 ∈ 𝐴 𝜑 )