MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  equsexvw Structured version   Visualization version   GIF version

Theorem equsexvw 2004
Description: Version of equsexv 2268 with a disjoint variable condition, and of equsex 2423 with two disjoint variable conditions, which requires fewer axioms. See also the dual form equsalvw 2003. (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
StepHypRef Expression
1 alinexa 1843 . . 3 (∀𝑥(𝑥 = 𝑦 → ¬ 𝜑) ↔ ¬ ∃𝑥(𝑥 = 𝑦𝜑))
2 equsalvw.1 . . . . 5 (𝑥 = 𝑦 → (𝜑𝜓))
32notbid 318 . . . 4 (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
43equsalvw 2003 . . 3 (∀𝑥(𝑥 = 𝑦 → ¬ 𝜑) ↔ ¬ 𝜓)
51, 4bitr3i 277 . 2 (¬ ∃𝑥(𝑥 = 𝑦𝜑) ↔ ¬ 𝜓)
65con4bii 321 1 (∃𝑥(𝑥 = 𝑦𝜑) ↔ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wal 1538  wex 1779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780
This theorem is referenced by:  equvinv  2028  cleljust  2117  sbelx  2253  cleljustab  2717  sbhypfOLD  3545  axsepgfromrep  5294  dfid3  5581  opeliunxp  5752  opeliun2xp  5753  imai  6092  coi1  6282  opabex3d  7990  opabex3rd  7991  opabex3  7992  fsplit  8142  mapsnend  9076  dfac5lem1  10163  dfac5lem3  10165  dffix2  35906  sscoid  35914  elfuns  35916  pmapglb  39772  polval2N  39908  tfsconcat0i  43358
  Copyright terms: Public domain W3C validator