Metamath Proof Explorer

Theorem op1steq

Description: Two ways of expressing that an element is the first member of an ordered pair. (Contributed by NM, 22-Sep-2013) (Revised by Mario Carneiro, 23-Feb-2014)

Ref Expression
Assertion op1steq ⊢ A ∈ V × W → 1 st ⁡ A = B ↔ ∃ x A = B x

Proof

Step Hyp Ref Expression
1 xpss ⊢ V × W ⊆ V × V
2 1 sseli ⊢ A ∈ V × W → A ∈ V × V
3 eqid ⊢ 2 nd ⁡ A = 2 nd ⁡ A
4 eqopi ⊢ A ∈ V × V ∧ 1 st ⁡ A = B ∧ 2 nd ⁡ A = 2 nd ⁡ A → A = B 2 nd ⁡ A
5 3 4 mpanr2 ⊢ A ∈ V × V ∧ 1 st ⁡ A = B → A = B 2 nd ⁡ A
6 fvex ⊢ 2 nd ⁡ A ∈ V
7 opeq2 ⊢ x = 2 nd ⁡ A → B x = B 2 nd ⁡ A
8 7 eqeq2d ⊢ x = 2 nd ⁡ A → A = B x ↔ A = B 2 nd ⁡ A
9 6 8 spcev ⊢ A = B 2 nd ⁡ A → ∃ x A = B x
10 5 9 syl ⊢ A ∈ V × V ∧ 1 st ⁡ A = B → ∃ x A = B x
11 10 ex ⊢ A ∈ V × V → 1 st ⁡ A = B → ∃ x A = B x
12 eqop ⊢ A ∈ V × V → A = B x ↔ 1 st ⁡ A = B ∧ 2 nd ⁡ A = x
13 simpl ⊢ 1 st ⁡ A = B ∧ 2 nd ⁡ A = x → 1 st ⁡ A = B
14 12 13 biimtrdi ⊢ A ∈ V × V → A = B x → 1 st ⁡ A = B
15 14 exlimdv ⊢ A ∈ V × V → ∃ x A = B x → 1 st ⁡ A = B
16 11 15 impbid ⊢ A ∈ V × V → 1 st ⁡ A = B ↔ ∃ x A = B x
17 2 16 syl ⊢ A ∈ V × W → 1 st ⁡ A = B ↔ ∃ x A = B x