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

Theorem equsexvw 2002
Description: Version of equsexv 2266 with a disjoint variable condition, and of equsex 2421 with two disjoint variable conditions, which requires fewer axioms. See also the dual form equsalvw 2001. (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 1840 . . 3 (∀𝑥(𝑥 = 𝑦 → ¬ 𝜑) ↔ ¬ ∃𝑥(𝑥 = 𝑦𝜑))
2 equsalvw.1 . . . . 5 (𝑥 = 𝑦 → (𝜑𝜓))
32notbid 318 . . . 4 (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
43equsalvw 2001 . . 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 1535  wex 1776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777
This theorem is referenced by:  equvinv  2026  cleljust  2115  sbelx  2251  cleljustab  2715  sbhypfOLD  3545  axsepgfromrep  5300  dfid3  5586  opeliunxp  5756  imai  6094  coi1  6284  opabex3d  7989  opabex3rd  7990  opabex3  7991  fsplit  8141  mapsnend  9075  dfac5lem1  10161  dfac5lem3  10163  dffix2  35887  sscoid  35895  elfuns  35897  pmapglb  39753  polval2N  39889  tfsconcat0i  43335  opeliun2xp  48178
  Copyright terms: Public domain W3C validator