Description: Existence of an operation class abstraction (special case). (Contributed by FL, 17-May-2010) (Revised by Mario Carneiro, 1-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | mpoexg.1 | ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) | |
Assertion | mpoexg | ⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → 𝐹 ∈ V ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpoexg.1 | ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) | |
2 | elex | ⊢ ( 𝐵 ∈ 𝑆 → 𝐵 ∈ V ) | |
3 | elex | ⊢ ( 𝐵 ∈ V → 𝐵 ∈ V ) | |
4 | 3 | ralrimivw | ⊢ ( 𝐵 ∈ V → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V ) |
5 | 2 4 | syl | ⊢ ( 𝐵 ∈ 𝑆 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V ) |
6 | 1 | mpoexxg | ⊢ ( ( 𝐴 ∈ 𝑅 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V ) → 𝐹 ∈ V ) |
7 | 5 6 | sylan2 | ⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → 𝐹 ∈ V ) |