Description: The value of an operation class abstraction (weak version). (Contributed by Mario Carneiro, 29-Dec-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ovidi.2 | ⊢ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) → ∃* 𝑧 𝜑 ) | |
ovidi.3 | ⊢ 𝐹 = { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } | ||
Assertion | ovidi | ⊢ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) → ( 𝜑 → ( 𝑥 𝐹 𝑦 ) = 𝑧 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ovidi.2 | ⊢ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) → ∃* 𝑧 𝜑 ) | |
2 | ovidi.3 | ⊢ 𝐹 = { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } | |
3 | moanimv | ⊢ ( ∃* 𝑧 ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) ↔ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) → ∃* 𝑧 𝜑 ) ) | |
4 | 1 3 | mpbir | ⊢ ∃* 𝑧 ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) |
5 | 4 2 | ovidig | ⊢ ( ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) → ( 𝑥 𝐹 𝑦 ) = 𝑧 ) |
6 | 5 | ex | ⊢ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) → ( 𝜑 → ( 𝑥 𝐹 𝑦 ) = 𝑧 ) ) |