Metamath Proof Explorer


Theorem oprabex

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

Ref Expression
Hypotheses oprabex.1 𝐴 ∈ V
oprabex.2 𝐵 ∈ V
oprabex.3 ( ( 𝑥𝐴𝑦𝐵 ) → ∃* 𝑧 𝜑 )
oprabex.4 𝐹 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥𝐴𝑦𝐵 ) ∧ 𝜑 ) }
Assertion oprabex 𝐹 ∈ V

Proof

Step Hyp Ref Expression
1 oprabex.1 𝐴 ∈ V
2 oprabex.2 𝐵 ∈ V
3 oprabex.3 ( ( 𝑥𝐴𝑦𝐵 ) → ∃* 𝑧 𝜑 )
4 oprabex.4 𝐹 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥𝐴𝑦𝐵 ) ∧ 𝜑 ) }
5 moanimv ( ∃* 𝑧 ( ( 𝑥𝐴𝑦𝐵 ) ∧ 𝜑 ) ↔ ( ( 𝑥𝐴𝑦𝐵 ) → ∃* 𝑧 𝜑 ) )
6 3 5 mpbir ∃* 𝑧 ( ( 𝑥𝐴𝑦𝐵 ) ∧ 𝜑 )
7 6 funoprab Fun { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥𝐴𝑦𝐵 ) ∧ 𝜑 ) }
8 1 2 xpex ( 𝐴 × 𝐵 ) ∈ V
9 dmoprabss dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥𝐴𝑦𝐵 ) ∧ 𝜑 ) } ⊆ ( 𝐴 × 𝐵 )
10 8 9 ssexi dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥𝐴𝑦𝐵 ) ∧ 𝜑 ) } ∈ V
11 funex ( ( Fun { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥𝐴𝑦𝐵 ) ∧ 𝜑 ) } ∧ dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥𝐴𝑦𝐵 ) ∧ 𝜑 ) } ∈ V ) → { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥𝐴𝑦𝐵 ) ∧ 𝜑 ) } ∈ V )
12 7 10 11 mp2an { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥𝐴𝑦𝐵 ) ∧ 𝜑 ) } ∈ V
13 4 12 eqeltri 𝐹 ∈ V