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