Metamath Proof Explorer

Theorem oprabex

Description: Existence of an operation class abstraction. (Contributed by NM, 19-Oct-2004)

Ref Expression
Hypotheses oprabex.1 ⊢ A ∈ V
oprabex.2 ⊢ B ∈ V
oprabex.3 ⊢ x ∈ A ∧ y ∈ B → ∃* z φ
oprabex.4 ⊢ F = x y z | x ∈ A ∧ y ∈ B ∧ φ
Assertion oprabex ⊢ F ∈ V

Proof

Step Hyp Ref Expression
1 oprabex.1 ⊢ A ∈ V
2 oprabex.2 ⊢ B ∈ V
3 oprabex.3 ⊢ x ∈ A ∧ y ∈ B → ∃* z φ
4 oprabex.4 ⊢ F = x y z | x ∈ A ∧ y ∈ B ∧ φ
5 moanimv ⊢ ∃* z x ∈ A ∧ y ∈ B ∧ φ ↔ x ∈ A ∧ y ∈ B → ∃* z φ
6 3 5 mpbir ⊢ ∃* z x ∈ A ∧ y ∈ B ∧ φ
7 6 funoprab ⊢ Fun ⁡ x y z | x ∈ A ∧ y ∈ B ∧ φ
8 1 2 xpex ⊢ A × B ∈ V
9 dmoprabss ⊢ dom ⁡ x y z | x ∈ A ∧ y ∈ B ∧ φ ⊆ A × B
10 8 9 ssexi ⊢ dom ⁡ x y z | x ∈ A ∧ y ∈ B ∧ φ ∈ V
11 funex ⊢ Fun ⁡ x y z | x ∈ A ∧ y ∈ B ∧ φ ∧ dom ⁡ x y z | x ∈ A ∧ y ∈ B ∧ φ ∈ V → x y z | x ∈ A ∧ y ∈ B ∧ φ ∈ V
12 7 10 11 mp2an ⊢ x y z | x ∈ A ∧ y ∈ B ∧ φ ∈ V
13 4 12 eqeltri ⊢ F ∈ V