This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )