Metamath Proof Explorer

Theorem eltrans

Description: Membership in the class of all transitive sets. (Contributed by Scott Fenton, 31-Mar-2012)

Ref Expression
Hypothesis eltrans.1 ⊢ A ∈ V
Assertion eltrans ⊢ A ∈ 𝖳𝗋𝖺𝗇𝗌 ↔ Tr ⁡ A

Proof

Step Hyp Ref Expression
1 eltrans.1 ⊢ A ∈ V
2 df-trans ⊢ 𝖳𝗋𝖺𝗇𝗌 = V ∖ ran ⁡ E ∘ E ∖ E
3 2 eleq2i ⊢ A ∈ 𝖳𝗋𝖺𝗇𝗌 ↔ A ∈ V ∖ ran ⁡ E ∘ E ∖ E
4 1 dftr6 ⊢ Tr ⁡ A ↔ A ∈ V ∖ ran ⁡ E ∘ E ∖ E
5 3 4 bitr4i ⊢ A ∈ 𝖳𝗋𝖺𝗇𝗌 ↔ Tr ⁡ A