This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ∃ y φ → x y | φ ∉ V

Proof

Step Hyp Ref Expression
1 vex ⊢ x ∈ V
2 1 biantrur ⊢ φ ↔ x ∈ V ∧ φ
3 2 opabbii ⊢ x y | φ = x y | x ∈ V ∧ φ
4 3 dmeqi ⊢ dom ⁡ x y | φ = dom ⁡ x y | x ∈ V ∧ φ
5 id ⊢ ∃ y φ → ∃ y φ
6 5 ralrimivw ⊢ ∃ y φ → ∀ x ∈ V ∃ y φ
7 dmopab3 ⊢ ∀ x ∈ V ∃ y φ ↔ dom ⁡ x y | x ∈ V ∧ φ = V
8 6 7 sylib ⊢ ∃ y φ → dom ⁡ x y | x ∈ V ∧ φ = V
9 4 8 eqtrid ⊢ ∃ y φ → dom ⁡ x y | φ = V
10 vprc ⊢ ¬ V ∈ V
11 10 a1i ⊢ ∃ y φ → ¬ V ∈ V
12 9 11 eqneltrd ⊢ ∃ y φ → ¬ dom ⁡ x y | φ ∈ V
13 dmexg ⊢ x y | φ ∈ V → dom ⁡ x y | φ ∈ V
14 12 13 nsyl ⊢ ∃ y φ → ¬ x y | φ ∈ V
15 df-nel ⊢ x y | φ ∉ V ↔ ¬ x y | φ ∈ V
16 14 15 sylibr ⊢ ∃ y φ → x y | φ ∉ V