Description: The R -preimage of an element of the base set in a set-like relation is a set. (Contributed by Mario Carneiro, 19-Nov-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | seex | ⊢ ( ( 𝑅 Se 𝐴 ∧ 𝐵 ∈ 𝐴 ) → { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑅 𝐵 } ∈ V ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-se | ⊢ ( 𝑅 Se 𝐴 ↔ ∀ 𝑦 ∈ 𝐴 { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑅 𝑦 } ∈ V ) | |
2 | breq2 | ⊢ ( 𝑦 = 𝐵 → ( 𝑥 𝑅 𝑦 ↔ 𝑥 𝑅 𝐵 ) ) | |
3 | 2 | rabbidv | ⊢ ( 𝑦 = 𝐵 → { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑅 𝑦 } = { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑅 𝐵 } ) |
4 | 3 | eleq1d | ⊢ ( 𝑦 = 𝐵 → ( { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑅 𝑦 } ∈ V ↔ { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑅 𝐵 } ∈ V ) ) |
5 | 4 | rspccva | ⊢ ( ( ∀ 𝑦 ∈ 𝐴 { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑅 𝑦 } ∈ V ∧ 𝐵 ∈ 𝐴 ) → { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑅 𝐵 } ∈ V ) |
6 | 1 5 | sylanb | ⊢ ( ( 𝑅 Se 𝐴 ∧ 𝐵 ∈ 𝐴 ) → { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑅 𝐵 } ∈ V ) |