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	syl5ibr	⊢ ( ¬ 𝐶 ∈ V → ( 𝐵 ∈ 𝑉 → ∃ 𝑥 { 𝐵 , 𝐶 } = { 𝐵 , 𝑥 } ) )
16	6 15	pm2.61i	⊢ ( 𝐵 ∈ 𝑉 → ∃ 𝑥 { 𝐵 , 𝐶 } = { 𝐵 , 𝑥 } )