This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dral1v

Description: Formula-building lemma for use with the Distinctor Reduction Theorem. Version of dral1 with a disjoint variable condition, which does not require ax-13 . Remark: the corresponding versions for dral2 and drex2 are instances of albidv and exbidv respectively. (Contributed by NM, 24-Nov-1994) (Revised by BJ, 17-Jun-2019) Base the proof on ax12v . (Revised by Wolf Lammen, 30-Mar-2024) Avoid ax-10 . (Revised by GG, 18-Nov-2024)

Ref Expression
Hypothesis dral1v.1 ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion dral1v ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 𝜑 ↔ ∀ 𝑦 𝜓 ) )

Proof

Step Hyp Ref Expression
1 dral1v.1 ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2 hbaev ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑥 ∀ 𝑥 𝑥 = 𝑦 )
3 2 1 albidh ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 𝜑 ↔ ∀ 𝑥 𝜓 ) )
4 axc11v ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 𝜓 → ∀ 𝑦 𝜓 ) )
5 axc11rv ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑦 𝜓 → ∀ 𝑥 𝜓 ) )
6 4 5 impbid ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 𝜓 ↔ ∀ 𝑦 𝜓 ) )
7 3 6 bitrd ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 𝜑 ↔ ∀ 𝑦 𝜓 ) )