Theorem equsexvw 2007

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1540  ∃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 1912  ax-6 1969

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782

This theorem is referenced by:  equvinv  2031  cleljust  2123  sbelx  2259  cleljustab  2716  axsepgfromrep  5238  dfid3  5521  opeliunxp  5690  opeliun2xp  5691  imai  6032  coi1  6220  opabex3d  7909  opabex3rd  7910  opabex3  7911  fsplit  8059  mapsnend  8975  elirrv  9504  dfac5lem1  10035  dfac5lem3  10037  dffix2  36076  sscoid  36084  elfuns  36086  pmapglb  40065  polval2N  40201  tfsconcat0i  43624