Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Richard Penner
Exploring Topology via Seifert and Threlfall
Generic Pseudoclosure Spaces, Pseudointerior Spaces, and Pseudoneighborhoods
brovmptimex2
Metamath Proof Explorer
Description: If a binary relation holds and the relation is the value of a binary
operation built with maps-to, then the arguments to that operation are
sets. (Contributed by RP , 22-May-2021)
Ref
Expression
Hypotheses
brovmptimex.mpt
⊢ 𝐹 = ( 𝑥 ∈ 𝐸 , 𝑦 ∈ 𝐺 ↦ 𝐻 )
brovmptimex.br
⊢ ( 𝜑 → 𝐴 𝑅 𝐵 )
brovmptimex.ov
⊢ ( 𝜑 → 𝑅 = ( 𝐶 𝐹 𝐷 ) )
Assertion
brovmptimex2
⊢ ( 𝜑 → 𝐷 ∈ V )
Proof
Step
Hyp
Ref
Expression
1
brovmptimex.mpt
⊢ 𝐹 = ( 𝑥 ∈ 𝐸 , 𝑦 ∈ 𝐺 ↦ 𝐻 )
2
brovmptimex.br
⊢ ( 𝜑 → 𝐴 𝑅 𝐵 )
3
brovmptimex.ov
⊢ ( 𝜑 → 𝑅 = ( 𝐶 𝐹 𝐷 ) )
4
1 2 3
brovmptimex
⊢ ( 𝜑 → ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) )
5
4
simprd
⊢ ( 𝜑 → 𝐷 ∈ V )