Theorem opabbrfexd

Description: A collection of ordered pairs, the second component being a function, is a set. (Contributed by AV, 15-Jan-2021)

	Ref	Expression
Hypotheses	opabresexd.x	⊢ ( ( 𝜑 ∧ 𝑥 𝑅 𝑦 ) → 𝑥 ∈ 𝐶 )
	opabresexd.y	⊢ ( ( 𝜑 ∧ 𝑥 𝑅 𝑦 ) → 𝑦 : 𝐴 ⟶ 𝐵 )
	opabresexd.a	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐴 ∈ 𝑈 )
	opabresexd.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐵 ∈ 𝑉 )
	opabresexd.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
Assertion	opabbrfexd	⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 𝑅 𝑦 } ∈ V )

Proof

Step	Hyp	Ref	Expression
1		opabresexd.x	⊢ ( ( 𝜑 ∧ 𝑥 𝑅 𝑦 ) → 𝑥 ∈ 𝐶 )
2		opabresexd.y	⊢ ( ( 𝜑 ∧ 𝑥 𝑅 𝑦 ) → 𝑦 : 𝐴 ⟶ 𝐵 )
3		opabresexd.a	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐴 ∈ 𝑈 )
4		opabresexd.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐵 ∈ 𝑉 )
5		opabresexd.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
6		pm4.24	⊢ ( 𝑥 𝑅 𝑦 ↔ ( 𝑥 𝑅 𝑦 ∧ 𝑥 𝑅 𝑦 ) )
7	6	opabbii	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 𝑅 𝑦 } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 𝑅 𝑦 ∧ 𝑥 𝑅 𝑦 ) }
8	1 2 3 4 5	opabresexd	⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 𝑅 𝑦 ∧ 𝑥 𝑅 𝑦 ) } ∈ V )
9	7 8	eqeltrid	⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 𝑅 𝑦 } ∈ V )