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 y x x y y A x A

Proof

Step Hyp Ref Expression
1 dftr2 Tr A x y x y y A x A
2 elequ1 x = z x y z y
3 2 anbi1d x = z x y y A z y y A
4 eleq1w x = z x A z A
5 3 4 imbi12d x = z x y y A x A z y y A z A
6 elequ2 y = z x y x z
7 eleq1w y = z y A z A
8 6 7 anbi12d y = z x y y A x z z A
9 8 imbi1d y = z x y y A x A x z z A x A
10 5 9 alcomw x y x y y A x A y x x y y A x A
11 1 10 bitri Tr A y x x y y A x A