Description: Sethood condition for the restricted converse epsilon relation. (Contributed by Peter Mazsa, 24-Sep-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | cnvepresex | ⊢ ( 𝐴 ∈ 𝑉 → ( ◡ E ↾ 𝐴 ) ∈ V ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnvepres | ⊢ ( ◡ E ↾ 𝐴 ) = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) } | |
2 | id | ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ 𝑉 ) | |
3 | abid2 | ⊢ { 𝑦 ∣ 𝑦 ∈ 𝑥 } = 𝑥 | |
4 | vex | ⊢ 𝑥 ∈ V | |
5 | 3 4 | eqeltri | ⊢ { 𝑦 ∣ 𝑦 ∈ 𝑥 } ∈ V |
6 | 5 | a1i | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝐴 ) → { 𝑦 ∣ 𝑦 ∈ 𝑥 } ∈ V ) |
7 | 2 6 | opabex3d | ⊢ ( 𝐴 ∈ 𝑉 → { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) } ∈ V ) |
8 | 1 7 | eqeltrid | ⊢ ( 𝐴 ∈ 𝑉 → ( ◡ E ↾ 𝐴 ) ∈ V ) |