Metamath Proof Explorer


Theorem seex

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 )

Proof

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 )