Theorem drex1v

Description: Formula-building lemma for use with the Distinctor Reduction Theorem. Version of drex1 with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 27-Feb-2005) (Revised by BJ, 17-Jun-2019)

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

Proof

Step	Hyp	Ref	Expression
1		dral1v.1	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2	1	notbid	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ¬ 𝜑 ↔ ¬ 𝜓 ) )
3	2	dral1v	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 ¬ 𝜑 ↔ ∀ 𝑦 ¬ 𝜓 ) )
4	3	notbid	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ¬ ∀ 𝑥 ¬ 𝜑 ↔ ¬ ∀ 𝑦 ¬ 𝜓 ) )
5		df-ex	⊢ ( ∃ 𝑥 𝜑 ↔ ¬ ∀ 𝑥 ¬ 𝜑 )
6		df-ex	⊢ ( ∃ 𝑦 𝜓 ↔ ¬ ∀ 𝑦 ¬ 𝜓 )
7	4 5 6	3bitr4g	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑥 𝜑 ↔ ∃ 𝑦 𝜓 ) )