Metamath Proof Explorer


Theorem elorvc

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/𝑐 𝑅 𝐴 ) ↔ ( 𝑋𝑧 ) 𝑅 𝐴 ) )

Proof

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/𝑐 𝑅 𝐴 ) ↔ ( 𝑋𝑧 ) 𝑅 𝐴 ) )