Theorem opabresex0d

Description: A collection of ordered pairs, the class of all possible second components being a set, with a restriction of a binary relation is a set. (Contributed by Alexander van der Vekens, 1-Nov-2017) (Revised by AV, 1-Jan-2021)

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

Proof

Step	Hyp	Ref	Expression
1		opabresex0d.x	⊢ ( ( 𝜑 ∧ 𝑥 𝑅 𝑦 ) → 𝑥 ∈ 𝐶 )
2		opabresex0d.t	⊢ ( ( 𝜑 ∧ 𝑥 𝑅 𝑦 ) → 𝜃 )
3		opabresex0d.y	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → { 𝑦 ∣ 𝜃 } ∈ 𝑉 )
4		opabresex0d.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
5	1 2	jca	⊢ ( ( 𝜑 ∧ 𝑥 𝑅 𝑦 ) → ( 𝑥 ∈ 𝐶 ∧ 𝜃 ) )
6	5	ex	⊢ ( 𝜑 → ( 𝑥 𝑅 𝑦 → ( 𝑥 ∈ 𝐶 ∧ 𝜃 ) ) )
7	6	alrimivv	⊢ ( 𝜑 → ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → ( 𝑥 ∈ 𝐶 ∧ 𝜃 ) ) )
8	3	elexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → { 𝑦 ∣ 𝜃 } ∈ V )
9	4 8	opabex3d	⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐶 ∧ 𝜃 ) } ∈ V )
10		opabbrex	⊢ ( ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → ( 𝑥 ∈ 𝐶 ∧ 𝜃 ) ) ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐶 ∧ 𝜃 ) } ∈ V ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 𝑅 𝑦 ∧ 𝜓 ) } ∈ V )
11	7 9 10	syl2anc	⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 𝑅 𝑦 ∧ 𝜓 ) } ∈ V )