Metamath Proof Explorer


Theorem dral1ALT

Description: Alternate proof of dral1 , shorter but requiring ax-11 . (Contributed by NM, 24-Nov-1994) (Proof shortened by Wolf Lammen, 22-Apr-2018) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step Hyp Ref Expression
1 dral1.1 ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝜑𝜓 ) )
2 1 dral2 ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 𝜑 ↔ ∀ 𝑥 𝜓 ) )
3 axc11 ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 𝜓 → ∀ 𝑦 𝜓 ) )
4 axc11r ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑦 𝜓 → ∀ 𝑥 𝜓 ) )
5 3 4 impbid ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 𝜓 ↔ ∀ 𝑦 𝜓 ) )
6 2 5 bitrd ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 𝜑 ↔ ∀ 𝑦 𝜓 ) )