Theorem opabn1stprc

Description: An ordered-pair class abstraction which does not depend on the first abstraction variable is a proper class. There must be, however, at least one set which satisfies the restricting wff. (Contributed by AV, 27-Dec-2020)

	Ref	Expression
Assertion	opabn1stprc	⊢ ( ∃ 𝑦 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∉ V )

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑥 ∈ V
2	1	biantrur	⊢ ( 𝜑 ↔ ( 𝑥 ∈ V ∧ 𝜑 ) )
3	2	opabbii	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝜑 ) }
4	3	dmeqi	⊢ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝜑 ) }
5		id	⊢ ( ∃ 𝑦 𝜑 → ∃ 𝑦 𝜑 )
6	5	ralrimivw	⊢ ( ∃ 𝑦 𝜑 → ∀ 𝑥 ∈ V ∃ 𝑦 𝜑 )
7		dmopab3	⊢ ( ∀ 𝑥 ∈ V ∃ 𝑦 𝜑 ↔ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝜑 ) } = V )
8	6 7	sylib	⊢ ( ∃ 𝑦 𝜑 → dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝜑 ) } = V )
9	4 8	eqtrid	⊢ ( ∃ 𝑦 𝜑 → dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = V )
10		vprc	⊢ ¬ V ∈ V
11	10	a1i	⊢ ( ∃ 𝑦 𝜑 → ¬ V ∈ V )
12	9 11	eqneltrd	⊢ ( ∃ 𝑦 𝜑 → ¬ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∈ V )
13		dmexg	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∈ V → dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∈ V )
14	12 13	nsyl	⊢ ( ∃ 𝑦 𝜑 → ¬ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∈ V )
15		df-nel	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∉ V ↔ ¬ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∈ V )
16	14 15	sylibr	⊢ ( ∃ 𝑦 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∉ V )