Description: Membership in a predecessor class. (Contributed by Scott Fenton, 4-Feb-2011)
Ref | Expression | ||
---|---|---|---|
Hypothesis | elpred.1 | ⊢ 𝑌 ∈ V | |
Assertion | elpred | ⊢ ( 𝑋 ∈ 𝐷 → ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ ( 𝑌 ∈ 𝐴 ∧ 𝑌 𝑅 𝑋 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elpred.1 | ⊢ 𝑌 ∈ V | |
2 | df-pred | ⊢ Pred ( 𝑅 , 𝐴 , 𝑋 ) = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) | |
3 | 2 | elin2 | ⊢ ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ∈ ( ◡ 𝑅 “ { 𝑋 } ) ) ) |
4 | 1 | eliniseg | ⊢ ( 𝑋 ∈ 𝐷 → ( 𝑌 ∈ ( ◡ 𝑅 “ { 𝑋 } ) ↔ 𝑌 𝑅 𝑋 ) ) |
5 | 4 | anbi2d | ⊢ ( 𝑋 ∈ 𝐷 → ( ( 𝑌 ∈ 𝐴 ∧ 𝑌 ∈ ( ◡ 𝑅 “ { 𝑋 } ) ) ↔ ( 𝑌 ∈ 𝐴 ∧ 𝑌 𝑅 𝑋 ) ) ) |
6 | 3 5 | syl5bb | ⊢ ( 𝑋 ∈ 𝐷 → ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ ( 𝑌 ∈ 𝐴 ∧ 𝑌 𝑅 𝑋 ) ) ) |