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 ⊢ B ∈ V → ∃ x B C = B x

Proof

Step Hyp Ref Expression
1 eqid ⊢ B C = B C
2 preq2 ⊢ x = C → B x = B C
3 2 eqeq2d ⊢ x = C → B C = B x ↔ B C = B C
4 3 spcegv ⊢ C ∈ V → B C = B C → ∃ x B C = B x
5 1 4 mpi ⊢ C ∈ V → ∃ x B C = B x
6 5 a1d ⊢ C ∈ V → B ∈ V → ∃ x B C = B x
7 dfsn2 ⊢ B = B B
8 preq2 ⊢ x = B → B x = B B
9 8 eqeq2d ⊢ x = B → B = B x ↔ B = B B
10 9 spcegv ⊢ B ∈ V → B = B B → ∃ x B = B x
11 7 10 mpi ⊢ B ∈ V → ∃ x B = B x
12 prprc2 ⊢ ¬ C ∈ V → B C = B
13 12 eqeq1d ⊢ ¬ C ∈ V → B C = B x ↔ B = B x
14 13 exbidv ⊢ ¬ C ∈ V → ∃ x B C = B x ↔ ∃ x B = B x
15 11 14 imbitrrid ⊢ ¬ C ∈ V → B ∈ V → ∃ x B C = B x
16 6 15 pm2.61i ⊢ B ∈ V → ∃ x B C = B x