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