Metamath Proof Explorer


Theorem dral1vOLD

Description: Obsolete version of dral1v as of 18-Nov-2024. (Contributed by NM, 24-Nov-1994) (Revised by BJ, 17-Jun-2019) Base the proof on ax12v . (Revised by Wolf Lammen, 30-Mar-2024) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

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