Theorem elovmpt3rab

Description: Implications for the value of an operation defined by the maps-to notation with a class abstraction as a result having an element. (Contributed by AV, 17-Jul-2018) (Revised by AV, 16-May-2019)

	Ref	Expression
Hypothesis	elovmpt3rab.o	⊢ 𝑂 = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑧 ∈ 𝑀 ↦ { 𝑎 ∈ 𝑁 ∣ 𝜑 } ) )
Assertion	elovmpt3rab	⊢ ( ( 𝑀 ∈ 𝑈 ∧ 𝑁 ∈ 𝑇 ) → ( 𝐴 ∈ ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) → ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝑍 ∈ 𝑀 ∧ 𝐴 ∈ 𝑁 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		elovmpt3rab.o	⊢ 𝑂 = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑧 ∈ 𝑀 ↦ { 𝑎 ∈ 𝑁 ∣ 𝜑 } ) )
2		eqidd	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → 𝑀 = 𝑀 )
3		eqidd	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → 𝑁 = 𝑁 )
4	1 2 3	elovmpt3rab1	⊢ ( ( 𝑀 ∈ 𝑈 ∧ 𝑁 ∈ 𝑇 ) → ( 𝐴 ∈ ( ( 𝑋 𝑂 𝑌 ) ‘ 𝑍 ) → ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ ( 𝑍 ∈ 𝑀 ∧ 𝐴 ∈ 𝑁 ) ) ) )