Theorem cbvexvw 2039

Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvexv 2406 for a version with fewer disjoint variable conditions but requiring more axioms. (Contributed by NM, 19-Apr-2017.)

Hypothesis

Ref	Expression
cbvalvw.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
cbvexvw	⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)

Distinct variable groups:   𝑥,𝑦   𝜓,𝑥   𝜑,𝑦

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem cbvexvw

Step	Hyp	Ref	Expression
1		cbvalvw.1	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
2	1	notbid 318	. . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
3	2	cbvalvw 2038	. . 3 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓)
4	3	notbii 320	. 2 ⊢ (¬ ∀𝑥 ¬ 𝜑 ↔ ¬ ∀𝑦 ¬ 𝜓)
5		df-ex 1782	. 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
6		df-ex 1782	. 2 ⊢ (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓)
7	4, 5, 6	3bitr4i 303	1 ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206  ∀wal 1540  ∃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 1912  ax-6 1969  ax-7 2010

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782

This theorem is referenced by:  cbvex2vw  2043  mojust  2539  mo4  2567  eujust  2572  cbveuvw  2606  iseqsetvlem  2800  cbvrexvw  3217  euind  3684  reuind  3713  cbvopab1v  5178  cbvopab2v  5179  bm1.3iiOLD  5249  reusv2lem2  5346  axprg  5383  relop  5807  dmcoss  5932  dmcossOLD  5933  fv3  6860  exfo  7059  cbvoprab3v  7460  zfun  7691  suppimacnv  8126  frrlem1  8238  ac6sfi  9196  brwdom2  9490  ttrclss  9641  ttrclselem2  9647  aceq1  10039  aceq0  10040  aceq3lem  10042  dfac4  10044  kmlem2  10074  kmlem13  10085  axdc4lem  10377  zfac  10382  zfcndun  10538  zfcndac  10542  sup2  12110  supmul  12126  climmo  15492  summo  15652  prodmo  15871  gsumval3eu  19845  elpt  23528  gsumwrd2dccatlem  33170  1arithidomlem1  33627  1arithidom  33629  bnj1185  34968  fineqvac  35291  axreg  35302  axregscl  35303  tz9.1regs  35309  satf0op  35590  sat1el2xp  35592  cbvrexvw2  36440  cbvoprab1vw  36450  cbvoprab2vw  36451  cbvoprab13vw  36454  bj-bm1.3ii  37306  wl-ax12v2cl  37755  fdc  37990  sn-sup2  42855  cpcoll2d  44609  axc11next  44756  fnchoice  45383  ichexmpl1  47823