Theorem dral1-o

Description: Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of Megill p. 448 (p. 16 of preprint). Version of dral1 using ax-c11 . (Contributed by NM, 24-Nov-1994) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		dral1-o.1	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2		hbae-o	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑥 ∀ 𝑥 𝑥 = 𝑦 )
3	1	biimpd	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝜑 → 𝜓 ) )
4	2 3	alimdh	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 𝜑 → ∀ 𝑥 𝜓 ) )
5		ax-c11	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 𝜓 → ∀ 𝑦 𝜓 ) )
6	4 5	syld	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 𝜑 → ∀ 𝑦 𝜓 ) )
7		hbae-o	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑦 ∀ 𝑥 𝑥 = 𝑦 )
8	1	biimprd	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝜓 → 𝜑 ) )
9	7 8	alimdh	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑦 𝜓 → ∀ 𝑦 𝜑 ) )
10		ax-c11	⊢ ( ∀ 𝑦 𝑦 = 𝑥 → ( ∀ 𝑦 𝜑 → ∀ 𝑥 𝜑 ) )
11	10	aecoms-o	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑦 𝜑 → ∀ 𝑥 𝜑 ) )
12	9 11	syld	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑦 𝜓 → ∀ 𝑥 𝜑 ) )
13	6 12	impbid	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 𝜑 ↔ ∀ 𝑦 𝜓 ) )