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

Theorem equsexvw 2011
 Description: Version of equsexv 2266 with a disjoint variable condition, and of equsex 2429 with two disjoint variable conditions, which requires fewer axioms. See also the dual form equsalvw 2010. (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 1844 . . 3 (∀𝑥(𝑥 = 𝑦 → ¬ 𝜑) ↔ ¬ ∃𝑥(𝑥 = 𝑦𝜑))
2 equsalvw.1 . . . . 5 (𝑥 = 𝑦 → (𝜑𝜓))
32notbid 321 . . . 4 (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
43equsalvw 2010 . . 3 (∀𝑥(𝑥 = 𝑦 → ¬ 𝜑) ↔ ¬ 𝜓)
51, 4bitr3i 280 . 2 (¬ ∃𝑥(𝑥 = 𝑦𝜑) ↔ ¬ 𝜓)
65con4bii 324 1 (∃𝑥(𝑥 = 𝑦𝜑) ↔ 𝜓)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1536  ∃wex 1781 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782 This theorem is referenced by:  equvinv  2036  cleljust  2120  sbelx  2252  cleljustab  2738  sbhypf  3471  axsepgfromrep  5170  dfid3  5435  opeliunxp  5592  imai  5918  coi1  6096  opabex3d  7675  opabex3rd  7676  opabex3  7677  fsplit  7822  fsplitOLD  7823  mapsnend  8612  dfac5lem1  9588  dfac5lem3  9590  dffix2  33782  sscoid  33790  elfuns  33792  pmapglb  37372  polval2N  37508  opeliun2xp  45129
 Copyright terms: Public domain W3C validator