This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iniseg

Description: An idiom that signifies an initial segment of an ordering, used, for example, in Definition 6.21 of TakeutiZaring p. 30. (Contributed by NM, 28-Apr-2004)

Ref Expression
Assertion iniseg ⊢ B ∈ V → A -1 B = x | x A B

Proof

Step Hyp Ref Expression
1 elex ⊢ B ∈ V → B ∈ V
2 vex ⊢ x ∈ V
3 2 eliniseg ⊢ B ∈ V → x ∈ A -1 B ↔ x A B
4 3 eqabdv ⊢ B ∈ V → A -1 B = x | x A B
5 1 4 syl ⊢ B ∈ V → A -1 B = x | x A B