Metamath Proof Explorer

Theorem dftr2c

Description: Variant of dftr2 with commuted quantifiers, useful for shortening proofs and avoiding ax-11 . (Contributed by BTernaryTau, 28-Dec-2024)

Ref Expression
Assertion dftr2c 
|- ( Tr A <-> A. y A. x ( ( x e. y /\ y e. A ) -> x e. A ) )

Proof

Step Hyp Ref Expression
1 dftr2 
 |-  ( Tr A <-> A. x A. y ( ( x e. y /\ y e. A ) -> x e. A ) )
2 elequ1 
 |-  ( x = z -> ( x e. y <-> z e. y ) )
3 2 anbi1d 
 |-  ( x = z -> ( ( x e. y /\ y e. A ) <-> ( z e. y /\ y e. A ) ) )
4 eleq1w 
 |-  ( x = z -> ( x e. A <-> z e. A ) )
5 3 4 imbi12d 
 |-  ( x = z -> ( ( ( x e. y /\ y e. A ) -> x e. A ) <-> ( ( z e. y /\ y e. A ) -> z e. A ) ) )
6 elequ2 
 |-  ( y = z -> ( x e. y <-> x e. z ) )
7 eleq1w 
 |-  ( y = z -> ( y e. A <-> z e. A ) )
8 6 7 anbi12d 
 |-  ( y = z -> ( ( x e. y /\ y e. A ) <-> ( x e. z /\ z e. A ) ) )
9 8 imbi1d 
 |-  ( y = z -> ( ( ( x e. y /\ y e. A ) -> x e. A ) <-> ( ( x e. z /\ z e. A ) -> x e. A ) ) )
10 5 9 alcomw 
 |-  ( A. x A. y ( ( x e. y /\ y e. A ) -> x e. A ) <-> A. y A. x ( ( x e. y /\ y e. A ) -> x e. A ) )
11 1 10 bitri 
 |-  ( Tr A <-> A. y A. x ( ( x e. y /\ y e. A ) -> x e. A ) )