Theorem equsexvw 2034

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1567  ∃wex 1808

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809

This theorem is used by:  equvinv  2058  cleljust  2151  sbelx  2288  cleljustab  2743  axsepgfromrep  5254  dfid3  5558  opeliunxp  5727  opeliun2xp  5728  imai  6075  coi1  6263  opabex3d  7960  opabex3rd  7961  opabex3  7962  fsplit  8110  mapsnend  9031  elirrv  9557  elirrvOLD  9558  dfac5lem1  10114  dfac5lem3  10116  dffix2  36403  sscoid  36411  elfuns  36413  pmapglb  40572  polval2N  40708  tfsconcat0i  44100