Description: Membership in the class of all transitive sets. (Contributed by Scott Fenton, 31-Mar-2012)
Ref | Expression | ||
---|---|---|---|
Hypothesis | eltrans.1 | ⊢ 𝐴 ∈ V | |
Assertion | eltrans | ⊢ ( 𝐴 ∈ Trans ↔ Tr 𝐴 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eltrans.1 | ⊢ 𝐴 ∈ V | |
2 | df-trans | ⊢ Trans = ( V ∖ ran ( ( E ∘ E ) ∖ E ) ) | |
3 | 2 | eleq2i | ⊢ ( 𝐴 ∈ Trans ↔ 𝐴 ∈ ( V ∖ ran ( ( E ∘ E ) ∖ E ) ) ) |
4 | 1 | dftr6 | ⊢ ( Tr 𝐴 ↔ 𝐴 ∈ ( V ∖ ran ( ( E ∘ E ) ∖ E ) ) ) |
5 | 3 4 | bitr4i | ⊢ ( 𝐴 ∈ Trans ↔ Tr 𝐴 ) |