Theorem equsexvw 2026

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

Hypothesis

Ref	Expression
equsalvw.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
equsexvw	⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓)

Distinct variable groups:   𝑥,𝑦   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑦)

Proof of Theorem equsexvw

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399  ∀wal 1559  ∃wex 1800

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1801

This theorem is referenced by:  equvinv  2050  cleljust  2152  sbelx  2289  cleljustab  2744  axsepgfromrep  5245  dfid3  5546  opeliunxp  5715  opeliun2xp  5716  imai  6063  coi1  6250  opabex3d  7946  opabex3rd  7947  opabex3  7948  fsplit  8096  mapsnend  9017  elirrv  9543  elirrvOLD  9544  dfac5lem1  10091  dfac5lem3  10093  dffix2  36258  sscoid  36266  elfuns  36268  pmapglb  40399  polval2N  40535  tfsconcat0i  43927