Theorem elpr2OLD

Description: Obsolete version of elpr2 as of 25-May-2024. (Contributed by NM, 14-Oct-2005) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	elpr2.1	⊢ 𝐵 ∈ V
	elpr2.2	⊢ 𝐶 ∈ V
Assertion	elpr2OLD	⊢ ( 𝐴 ∈ { 𝐵 , 𝐶 } ↔ ( 𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		elpr2.1	⊢ 𝐵 ∈ V
2		elpr2.2	⊢ 𝐶 ∈ V
3		elex	⊢ ( 𝐴 ∈ { 𝐵 , 𝐶 } → 𝐴 ∈ V )
4		eleq1	⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∈ V ↔ 𝐵 ∈ V ) )
5	1 4	mpbiri	⊢ ( 𝐴 = 𝐵 → 𝐴 ∈ V )
6		eleq1	⊢ ( 𝐴 = 𝐶 → ( 𝐴 ∈ V ↔ 𝐶 ∈ V ) )
7	2 6	mpbiri	⊢ ( 𝐴 = 𝐶 → 𝐴 ∈ V )
8	5 7	jaoi	⊢ ( ( 𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ) → 𝐴 ∈ V )
9		elprg	⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ { 𝐵 , 𝐶 } ↔ ( 𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ) ) )
10	3 8 9	pm5.21nii	⊢ ( 𝐴 ∈ { 𝐵 , 𝐶 } ↔ ( 𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ) )