Theorem cbvexvw 2070

Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvexv 2431 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 321	. . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
3	2	cbvalvw 2069	. . 3 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓)
4	3	notbii 323	. 2 ⊢ (¬ ∀𝑥 ¬ 𝜑 ↔ ¬ ∀𝑦 ¬ 𝜓)
5		df-ex 1813	. 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
6		df-ex 1813	. 2 ⊢ (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓)
7	4, 5, 6	3bitr4i 306	1 ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209  ∀wal 1568  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813

This theorem is used by:  cbvex2vw  2074  mojust  2564  mo4  2592  eujust  2597  cbveuvw  2631  iseqsetvlem  2824  cbvrexvw  3242  euind  3682  reuind  3711  cbvopab1v  5183  cbvopab2v  5184  reusv2lem2  5361  axprg  5395  relop  5828  dmcoss  5957  dmcossOLD  5958  fv3  6895  exfo  7097  cbvoprab3v  7504  zfun  7741  suppimacnv  8175  frrlem1  8288  ac6sfi  9259  brwdom2  9551  ttrclss  9705  ttrclselem2  9711  aceq1  10177  aceq0  10178  aceq3lem  10180  dfac4  10182  kmlem2  10211  kmlem13  10222  axdc4lem  10514  zfac  10519  zfcndun  10681  zfcndac  10685  sup2  12254  supmul  12270  climmo  15704  summo  15863  prodmo  16083  gsumval3eu  20098  elpt  23871  gsumwrd2dccatlem  33620  1arithidomlem1  34049  1arithidom  34051  bnj1185  35406  axprALT2  35713  fineqvac  35757  axreg  35768  axregscl  35769  tz9.1regs  35775  satf0op  36111  sat1el2xp  36113  cbvrexvw2  36986  cbvoprab1vw  36996  cbvoprab2vw  36997  cbvoprab13vw  37000  mh-regprimbi  37303  bj-bm1.3ii  37947  wl-ax12v2cl  38397  wl-dfclel  38406  fdc  38647  sn-sup2  43523  cpcoll2d  45202  axc11next  45349  fnchoice  45989  ichexmpl1  48495  cbvals  50845