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

Theorem equsexvw 2009
Description: Version of equsexv 2260 with a disjoint variable condition, and of equsex 2418 with two disjoint variable conditions, which requires fewer axioms. See also the dual form equsalvw 2008. (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 1846 . . 3 (∀𝑥(𝑥 = 𝑦 → ¬ 𝜑) ↔ ¬ ∃𝑥(𝑥 = 𝑦𝜑))
2 equsalvw.1 . . . . 5 (𝑥 = 𝑦 → (𝜑𝜓))
32notbid 318 . . . 4 (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
43equsalvw 2008 . . 3 (∀𝑥(𝑥 = 𝑦 → ¬ 𝜑) ↔ ¬ 𝜓)
51, 4bitr3i 277 . 2 (¬ ∃𝑥(𝑥 = 𝑦𝜑) ↔ ¬ 𝜓)
65con4bii 321 1 (∃𝑥(𝑥 = 𝑦𝜑) ↔ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  wal 1540  wex 1782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783
This theorem is referenced by:  equvinv  2033  cleljust  2116  sbelx  2246  cleljustab  2713  sbhypfOLD  3539  axsepgfromrep  5296  dfid3  5576  opeliunxp  5741  imai  6070  coi1  6258  opabex3d  7947  opabex3rd  7948  opabex3  7949  fsplit  8098  mapsnend  9032  dfac5lem1  10114  dfac5lem3  10116  dffix2  34815  sscoid  34823  elfuns  34825  pmapglb  38579  polval2N  38715  tfsconcat0i  42028  opeliun2xp  46910
  Copyright terms: Public domain W3C validator