Theorem equsexvw 2033

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1566  ∃wex 1807

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1808

This theorem is referenced by:  equvinv  2057  cleljust  2150  sbelx  2287  cleljustab  2742  axsepgfromrep  5254  dfid3  5559  opeliunxp  5728  opeliun2xp  5729  imai  6076  coi1  6264  opabex3d  7961  opabex3rd  7962  opabex3  7963  fsplit  8111  mapsnend  9032  elirrv  9558  elirrvOLD  9559  dfac5lem1  10106  dfac5lem3  10108  dffix2  36349  sscoid  36357  elfuns  36359  pmapglb  40490  polval2N  40626  tfsconcat0i  44020