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 Gino Giotto, 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	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 𝜑 ↔ ∀ 𝑦 𝜓 ) )