# Metamath Proof Explorer

## Theorem trel

Description: In a transitive class, the membership relation is transitive. (Contributed by NM, 19-Apr-1994) (Proof shortened by Andrew Salmon, 9-Jul-2011)

Ref Expression
Assertion trel ${⊢}\mathrm{Tr}{A}\to \left(\left({B}\in {C}\wedge {C}\in {A}\right)\to {B}\in {A}\right)$

### Proof

Step Hyp Ref Expression
1 dftr2 ${⊢}\mathrm{Tr}{A}↔\forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({y}\in {x}\wedge {x}\in {A}\right)\to {y}\in {A}\right)$
2 eleq12 ${⊢}\left({y}={B}\wedge {x}={C}\right)\to \left({y}\in {x}↔{B}\in {C}\right)$
3 eleq1 ${⊢}{x}={C}\to \left({x}\in {A}↔{C}\in {A}\right)$
4 3 adantl ${⊢}\left({y}={B}\wedge {x}={C}\right)\to \left({x}\in {A}↔{C}\in {A}\right)$
5 2 4 anbi12d ${⊢}\left({y}={B}\wedge {x}={C}\right)\to \left(\left({y}\in {x}\wedge {x}\in {A}\right)↔\left({B}\in {C}\wedge {C}\in {A}\right)\right)$
6 eleq1 ${⊢}{y}={B}\to \left({y}\in {A}↔{B}\in {A}\right)$
7 6 adantr ${⊢}\left({y}={B}\wedge {x}={C}\right)\to \left({y}\in {A}↔{B}\in {A}\right)$
8 5 7 imbi12d ${⊢}\left({y}={B}\wedge {x}={C}\right)\to \left(\left(\left({y}\in {x}\wedge {x}\in {A}\right)\to {y}\in {A}\right)↔\left(\left({B}\in {C}\wedge {C}\in {A}\right)\to {B}\in {A}\right)\right)$
9 8 spc2gv ${⊢}\left({B}\in {C}\wedge {C}\in {A}\right)\to \left(\forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({y}\in {x}\wedge {x}\in {A}\right)\to {y}\in {A}\right)\to \left(\left({B}\in {C}\wedge {C}\in {A}\right)\to {B}\in {A}\right)\right)$
10 9 pm2.43b ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({y}\in {x}\wedge {x}\in {A}\right)\to {y}\in {A}\right)\to \left(\left({B}\in {C}\wedge {C}\in {A}\right)\to {B}\in {A}\right)$
11 1 10 sylbi ${⊢}\mathrm{Tr}{A}\to \left(\left({B}\in {C}\wedge {C}\in {A}\right)\to {B}\in {A}\right)$