Metamath Proof Explorer

Theorem drnf1v

Description: Formula-building lemma for use with the Distinctor Reduction Theorem. Version of drnf1 with a disjoint variable condition, which does not require ax-13 . (Contributed by Mario Carneiro, 4-Oct-2016) (Revised by BJ, 17-Jun-2019)

Ref Expression
Hypothesis dral1v.1 ⊢ ∀ x x = y → φ ↔ ψ
Assertion drnf1v ⊢ ∀ x x = y → Ⅎ x φ ↔ Ⅎ y ψ

Proof

Step Hyp Ref Expression
1 dral1v.1 ⊢ ∀ x x = y → φ ↔ ψ
2 1 dral1v ⊢ ∀ x x = y → ∀ x φ ↔ ∀ y ψ
3 1 2 imbi12d ⊢ ∀ x x = y → φ → ∀ x φ ↔ ψ → ∀ y ψ
4 3 dral1v ⊢ ∀ x x = y → ∀ x φ → ∀ x φ ↔ ∀ y ψ → ∀ y ψ
5 nf5 ⊢ Ⅎ x φ ↔ ∀ x φ → ∀ x φ
6 nf5 ⊢ Ⅎ y ψ ↔ ∀ y ψ → ∀ y ψ
7 4 5 6 3bitr4g ⊢ ∀ x x = y → Ⅎ x φ ↔ Ⅎ y ψ