Theorem opabbrfex0d

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

	Ref	Expression
Hypotheses	opabresex0d.x	⊢ ( ( 𝜑 ∧ 𝑥 𝑅 𝑦 ) → 𝑥 ∈ 𝐶 )
	opabresex0d.t	⊢ ( ( 𝜑 ∧ 𝑥 𝑅 𝑦 ) → 𝜃 )
	opabresex0d.y	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → { 𝑦 ∣ 𝜃 } ∈ 𝑉 )
	opabresex0d.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
Assertion	opabbrfex0d	⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 𝑅 𝑦 } ∈ V )

Proof

Step	Hyp	Ref	Expression
1		opabresex0d.x	⊢ ( ( 𝜑 ∧ 𝑥 𝑅 𝑦 ) → 𝑥 ∈ 𝐶 )
2		opabresex0d.t	⊢ ( ( 𝜑 ∧ 𝑥 𝑅 𝑦 ) → 𝜃 )
3		opabresex0d.y	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → { 𝑦 ∣ 𝜃 } ∈ 𝑉 )
4		opabresex0d.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
5		pm4.24	⊢ ( 𝑥 𝑅 𝑦 ↔ ( 𝑥 𝑅 𝑦 ∧ 𝑥 𝑅 𝑦 ) )
6	5	opabbii	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 𝑅 𝑦 } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 𝑅 𝑦 ∧ 𝑥 𝑅 𝑦 ) }
7	1 2 3 4	opabresex0d	⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 𝑅 𝑦 ∧ 𝑥 𝑅 𝑦 ) } ∈ V )
8	6 7	eqeltrid	⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 𝑅 𝑦 } ∈ V )