Theorem equsexvw 2008

Description: Version of equsexv 2259 with a disjoint variable condition, and of equsex 2417 with two disjoint variable conditions, which requires fewer axioms. See also the dual form equsalvw 2007. (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 1845	. . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → ¬ 𝜑) ↔ ¬ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
2		equsalvw.1	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	2	notbid 317	. . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
4	3	equsalvw 2007	. . 3 ⊢ (∀𝑥(𝑥 = 𝑦 → ¬ 𝜑) ↔ ¬ 𝜓)
5	1, 4	bitr3i 276	. 2 ⊢ (¬ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ¬ 𝜓)
6	5	con4bii 320	1 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396  ∀wal 1539  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782

This theorem is referenced by:  equvinv  2032  cleljust  2115  sbelx  2245  cleljustab  2712  sbhypfOLD  3539  axsepgfromrep  5296  dfid3  5576  opeliunxp  5741  imai  6070  coi1  6258  opabex3d  7948  opabex3rd  7949  opabex3  7950  fsplit  8099  mapsnend  9032  dfac5lem1  10114  dfac5lem3  10116  dffix2  34865  sscoid  34873  elfuns  34875  pmapglb  38629  polval2N  38765  tfsconcat0i  42080  opeliun2xp  46961