Metamath Proof Explorer

Theorem elpreqpr

Description: Equality and membership rule for pairs. (Contributed by Scott Fenton, 7-Dec-2020)

Ref Expression
Assertion elpreqpr ⊢ A ∈ B C → ∃ x B C = A x

Proof

Step Hyp Ref Expression
1 elpri ⊢ A ∈ B C → A = B ∨ A = C
2 elex ⊢ A ∈ B C → A ∈ V
3 elpreqprlem ⊢ B ∈ V → ∃ x B C = B x
4 eleq1 ⊢ A = B → A ∈ V ↔ B ∈ V
5 preq1 ⊢ A = B → A x = B x
6 5 eqeq2d ⊢ A = B → B C = A x ↔ B C = B x
7 6 exbidv ⊢ A = B → ∃ x B C = A x ↔ ∃ x B C = B x
8 4 7 imbi12d ⊢ A = B → A ∈ V → ∃ x B C = A x ↔ B ∈ V → ∃ x B C = B x
9 3 8 mpbiri ⊢ A = B → A ∈ V → ∃ x B C = A x
10 9 imp ⊢ A = B ∧ A ∈ V → ∃ x B C = A x
11 elpreqprlem ⊢ C ∈ V → ∃ x C B = C x
12 prcom ⊢ C B = B C
13 12 eqeq1i ⊢ C B = C x ↔ B C = C x
14 13 exbii ⊢ ∃ x C B = C x ↔ ∃ x B C = C x
15 11 14 sylib ⊢ C ∈ V → ∃ x B C = C x
16 eleq1 ⊢ A = C → A ∈ V ↔ C ∈ V
17 preq1 ⊢ A = C → A x = C x
18 17 eqeq2d ⊢ A = C → B C = A x ↔ B C = C x
19 18 exbidv ⊢ A = C → ∃ x B C = A x ↔ ∃ x B C = C x
20 16 19 imbi12d ⊢ A = C → A ∈ V → ∃ x B C = A x ↔ C ∈ V → ∃ x B C = C x
21 15 20 mpbiri ⊢ A = C → A ∈ V → ∃ x B C = A x
22 21 imp ⊢ A = C ∧ A ∈ V → ∃ x B C = A x
23 10 22 jaoian ⊢ A = B ∨ A = C ∧ A ∈ V → ∃ x B C = A x
24 1 2 23 syl2anc ⊢ A ∈ B C → ∃ x B C = A x