Description: Membership in an initial segment. The idiom (`' A " { B } ) , meaning { x | x A B } ` , is used to specify an initial segment in (for example) Definition 6.21 of TakeutiZaring p. 30. (Contributed by NM, 28-Apr-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011)
Ref | Expression | ||
---|---|---|---|
Hypothesis | eliniseg.1 | ⊢ 𝐶 ∈ V | |
Assertion | eliniseg | ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐶 ∈ ( ◡ 𝐴 “ { 𝐵 } ) ↔ 𝐶 𝐴 𝐵 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eliniseg.1 | ⊢ 𝐶 ∈ V | |
2 | elimasng | ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ V ) → ( 𝐶 ∈ ( ◡ 𝐴 “ { 𝐵 } ) ↔ 〈 𝐵 , 𝐶 〉 ∈ ◡ 𝐴 ) ) | |
3 | df-br | ⊢ ( 𝐵 ◡ 𝐴 𝐶 ↔ 〈 𝐵 , 𝐶 〉 ∈ ◡ 𝐴 ) | |
4 | 2 3 | bitr4di | ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ V ) → ( 𝐶 ∈ ( ◡ 𝐴 “ { 𝐵 } ) ↔ 𝐵 ◡ 𝐴 𝐶 ) ) |
5 | brcnvg | ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ V ) → ( 𝐵 ◡ 𝐴 𝐶 ↔ 𝐶 𝐴 𝐵 ) ) | |
6 | 4 5 | bitrd | ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ V ) → ( 𝐶 ∈ ( ◡ 𝐴 “ { 𝐵 } ) ↔ 𝐶 𝐴 𝐵 ) ) |
7 | 1 6 | mpan2 | ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐶 ∈ ( ◡ 𝐴 “ { 𝐵 } ) ↔ 𝐶 𝐴 𝐵 ) ) |