This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem equsexvw

Description: Version of equsexv with a disjoint variable condition, and of equsex with two disjoint variable conditions, which requires fewer axioms. See also the dual form equsalvw . (Contributed by BJ, 31-May-2019) (Proof shortened by Wolf Lammen, 23-Oct-2023)

		Ref	Expression
	Hypothesis	equsalvw.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
	Assertion	equsexvw	⊢ ( ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) ↔ 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		equsalvw.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2		alinexa	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → ¬ 𝜑 ) ↔ ¬ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) )
3	1	notbid	⊢ ( 𝑥 = 𝑦 → ( ¬ 𝜑 ↔ ¬ 𝜓 ) )
4	3	equsalvw	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → ¬ 𝜑 ) ↔ ¬ 𝜓 )
5	2 4	bitr3i	⊢ ( ¬ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) ↔ ¬ 𝜓 )
6	5	con4bii	⊢ ( ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) ↔ 𝜓 )