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

Metamath Proof Explorer

Theorem elpreqprlem

Description: Lemma for elpreqpr . (Contributed by Scott Fenton, 7-Dec-2020) (Revised by AV, 9-Dec-2020)

Ref Expression
Assertion elpreqprlem ( 𝐵 ∈ 𝑉 → ∃ 𝑥 { 𝐵 , 𝐶 } = { 𝐵 , 𝑥 } )

Proof

Step Hyp Ref Expression
1 eqid ⊢ { 𝐵 , 𝐶 } = { 𝐵 , 𝐶 }
2 preq2 ⊢ ( 𝑥 = 𝐶 → { 𝐵 , 𝑥 } = { 𝐵 , 𝐶 } )
3 2 eqeq2d ⊢ ( 𝑥 = 𝐶 → ( { 𝐵 , 𝐶 } = { 𝐵 , 𝑥 } ↔ { 𝐵 , 𝐶 } = { 𝐵 , 𝐶 } ) )
4 3 spcegv ⊢ ( 𝐶 ∈ V → ( { 𝐵 , 𝐶 } = { 𝐵 , 𝐶 } → ∃ 𝑥 { 𝐵 , 𝐶 } = { 𝐵 , 𝑥 } ) )
5 1 4 mpi ⊢ ( 𝐶 ∈ V → ∃ 𝑥 { 𝐵 , 𝐶 } = { 𝐵 , 𝑥 } )
6 5 a1d ⊢ ( 𝐶 ∈ V → ( 𝐵 ∈ 𝑉 → ∃ 𝑥 { 𝐵 , 𝐶 } = { 𝐵 , 𝑥 } ) )
7 dfsn2 ⊢ { 𝐵 } = { 𝐵 , 𝐵 }
8 preq2 ⊢ ( 𝑥 = 𝐵 → { 𝐵 , 𝑥 } = { 𝐵 , 𝐵 } )
9 8 eqeq2d ⊢ ( 𝑥 = 𝐵 → ( { 𝐵 } = { 𝐵 , 𝑥 } ↔ { 𝐵 } = { 𝐵 , 𝐵 } ) )
10 9 spcegv ⊢ ( 𝐵 ∈ 𝑉 → ( { 𝐵 } = { 𝐵 , 𝐵 } → ∃ 𝑥 { 𝐵 } = { 𝐵 , 𝑥 } ) )
11 7 10 mpi ⊢ ( 𝐵 ∈ 𝑉 → ∃ 𝑥 { 𝐵 } = { 𝐵 , 𝑥 } )
12 prprc2 ⊢ ( ¬ 𝐶 ∈ V → { 𝐵 , 𝐶 } = { 𝐵 } )
13 12 eqeq1d ⊢ ( ¬ 𝐶 ∈ V → ( { 𝐵 , 𝐶 } = { 𝐵 , 𝑥 } ↔ { 𝐵 } = { 𝐵 , 𝑥 } ) )
14 13 exbidv ⊢ ( ¬ 𝐶 ∈ V → ( ∃ 𝑥 { 𝐵 , 𝐶 } = { 𝐵 , 𝑥 } ↔ ∃ 𝑥 { 𝐵 } = { 𝐵 , 𝑥 } ) )
15 11 14 imbitrrid ⊢ ( ¬ 𝐶 ∈ V → ( 𝐵 ∈ 𝑉 → ∃ 𝑥 { 𝐵 , 𝐶 } = { 𝐵 , 𝑥 } ) )
16 6 15 pm2.61i ⊢ ( 𝐵 ∈ 𝑉 → ∃ 𝑥 { 𝐵 , 𝐶 } = { 𝐵 , 𝑥 } )