Theorem bnj1148

Description: Property of _pred . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Assertion	bnj1148	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → pred ( 𝑋 , 𝐴 , 𝑅 ) ∈ V )

Proof

Step	Hyp	Ref	Expression
1		elisset	⊢ ( 𝑋 ∈ 𝐴 → ∃ 𝑥 𝑥 = 𝑋 )
2	1	adantl	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∃ 𝑥 𝑥 = 𝑋 )
3		bnj93	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → pred ( 𝑥 , 𝐴 , 𝑅 ) ∈ V )
4		eleq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∈ 𝐴 ↔ 𝑋 ∈ 𝐴 ) )
5	4	anbi2d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) )
6		bnj602	⊢ ( 𝑥 = 𝑋 → pred ( 𝑥 , 𝐴 , 𝑅 ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
7	6	eleq1d	⊢ ( 𝑥 = 𝑋 → ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∈ V ↔ pred ( 𝑋 , 𝐴 , 𝑅 ) ∈ V ) )
8	5 7	imbi12d	⊢ ( 𝑥 = 𝑋 → ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → pred ( 𝑥 , 𝐴 , 𝑅 ) ∈ V ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → pred ( 𝑋 , 𝐴 , 𝑅 ) ∈ V ) ) )
9	3 8	mpbii	⊢ ( 𝑥 = 𝑋 → ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → pred ( 𝑋 , 𝐴 , 𝑅 ) ∈ V ) )
10	2 9	bnj593	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∃ 𝑥 ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → pred ( 𝑋 , 𝐴 , 𝑅 ) ∈ V ) )
11	10	bnj937	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → pred ( 𝑋 , 𝐴 , 𝑅 ) ∈ V ) )
12	11	pm2.43i	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → pred ( 𝑋 , 𝐴 , 𝑅 ) ∈ V )