This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - start with the Axiom of Extensionality Unordered and ordered pairs elpr2
Description: A member of a pair of sets is one or the other of them, and conversely.
Exercise 1 of TakeutiZaring p. 15. (Contributed by NM , 14-Oct-2005)
(Proof shortened by JJ , 23-Jul-2021)
Ref
Expression
Hypotheses
elpr2.1 ⊢ 𝐵 ∈ V
elpr2.2 ⊢ 𝐶 ∈ V
Assertion
elpr2 ⊢ ( 𝐴 ∈ { 𝐵 , 𝐶 } ↔ ( 𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ) )
Proof
Step
Hyp
Ref
Expression
1
elpr2.1 ⊢ 𝐵 ∈ V
2
elpr2.2 ⊢ 𝐶 ∈ V
3
elpr2g ⊢ ( ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) → ( 𝐴 ∈ { 𝐵 , 𝐶 } ↔ ( 𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ) ) )
4
1 2 3
mp2an ⊢ ( 𝐴 ∈ { 𝐵 , 𝐶 } ↔ ( 𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ) )