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	⊢ ( 𝐴 ∈ { 𝐵 , 𝐶 } → ∃ 𝑥 { 𝐵 , 𝐶 } = { 𝐴 , 𝑥 } )