Description: Elementhood of a preimage. (Contributed by Thierry Arnoux, 21-Jan-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | orvcval.1 | ⊢ ( 𝜑 → Fun 𝑋 ) | |
orvcval.2 | ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 ) | ||
orvcval.3 | ⊢ ( 𝜑 → 𝐴 ∈ 𝑊 ) | ||
Assertion | elorvc | ⊢ ( ( 𝜑 ∧ 𝑧 ∈ dom 𝑋 ) → ( 𝑧 ∈ ( 𝑋 ∘RV/𝑐 𝑅 𝐴 ) ↔ ( 𝑋 ‘ 𝑧 ) 𝑅 𝐴 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orvcval.1 | ⊢ ( 𝜑 → Fun 𝑋 ) | |
2 | orvcval.2 | ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 ) | |
3 | orvcval.3 | ⊢ ( 𝜑 → 𝐴 ∈ 𝑊 ) | |
4 | 1 2 3 | orvcval2 | ⊢ ( 𝜑 → ( 𝑋 ∘RV/𝑐 𝑅 𝐴 ) = { 𝑧 ∈ dom 𝑋 ∣ ( 𝑋 ‘ 𝑧 ) 𝑅 𝐴 } ) |
5 | 4 | eleq2d | ⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝑋 ∘RV/𝑐 𝑅 𝐴 ) ↔ 𝑧 ∈ { 𝑧 ∈ dom 𝑋 ∣ ( 𝑋 ‘ 𝑧 ) 𝑅 𝐴 } ) ) |
6 | rabid | ⊢ ( 𝑧 ∈ { 𝑧 ∈ dom 𝑋 ∣ ( 𝑋 ‘ 𝑧 ) 𝑅 𝐴 } ↔ ( 𝑧 ∈ dom 𝑋 ∧ ( 𝑋 ‘ 𝑧 ) 𝑅 𝐴 ) ) | |
7 | 5 6 | bitrdi | ⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝑋 ∘RV/𝑐 𝑅 𝐴 ) ↔ ( 𝑧 ∈ dom 𝑋 ∧ ( 𝑋 ‘ 𝑧 ) 𝑅 𝐴 ) ) ) |
8 | 7 | baibd | ⊢ ( ( 𝜑 ∧ 𝑧 ∈ dom 𝑋 ) → ( 𝑧 ∈ ( 𝑋 ∘RV/𝑐 𝑅 𝐴 ) ↔ ( 𝑋 ‘ 𝑧 ) 𝑅 𝐴 ) ) |