Theorem opabex2

Description: Condition for an operation to be a set. (Contributed by Thierry Arnoux, 25-Jun-2019)

	Ref	Expression
Hypotheses	opabex2.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	opabex2.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	opabex2.3	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑥 ∈ 𝐴 )
	opabex2.4	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑦 ∈ 𝐵 )
Assertion	opabex2	⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∈ V )

Proof

Step	Hyp	Ref	Expression
1		opabex2.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		opabex2.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3		opabex2.3	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑥 ∈ 𝐴 )
4		opabex2.4	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑦 ∈ 𝐵 )
5	1 2	xpexd	⊢ ( 𝜑 → ( 𝐴 × 𝐵 ) ∈ V )
6	3 4	opabssxpd	⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ⊆ ( 𝐴 × 𝐵 ) )
7	5 6	ssexd	⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∈ V )