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

Metamath Proof Explorer

Theorem elpreqpr

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

Ref Expression
Assertion elpreqpr ( 𝐴 ∈ { 𝐵 , 𝐶 } → ∃ 𝑥 { 𝐵 , 𝐶 } = { 𝐴 , 𝑥 } )

Proof

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