Theorem cbvexvw 2070

Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvexv 2436 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  2569  mo4  2597  eujust  2602  cbveuvw  2636  iseqsetvlem  2829  cbvrexvw  3247  euind  3690  reuind  3719  cbvopab1v  5194  cbvopab2v  5195  bm1.3iiOLD  5270  reusv2lem2  5375  axprg  5413  relop  5841  dmcoss  5970  dmcossOLD  5971  fv3  6906  exfo  7107  cbvoprab3v  7515  zfun  7746  suppimacnv  8179  frrlem1  8292  ac6sfi  9254  brwdom2  9545  ttrclss  9699  ttrclselem2  9705  aceq1  10120  aceq0  10121  aceq3lem  10123  dfac4  10125  kmlem2  10154  kmlem13  10165  axdc4lem  10457  zfac  10462  zfcndun  10618  zfcndac  10622  sup2  12189  supmul  12205  climmo  15634  summo  15794  prodmo  16016  gsumval3eu  20005  elpt  23766  gsumwrd2dccatlem  33428  1arithidomlem1  33856  1arithidom  33858  bnj1185  35212  axprALT2  35527  fineqvac  35552  axreg  35563  axregscl  35564  tz9.1regs  35570  satf0op  35889  sat1el2xp  35891  cbvrexvw2  36779  cbvoprab1vw  36789  cbvoprab2vw  36790  cbvoprab13vw  36793  mh-regprimbi  37096  bj-bm1.3ii  37740  wl-ax12v2cl  38192  wl-dfclel  38201  fdc  38436  sn-sup2  43305  cpcoll2d  45009  axc11next  45156  fnchoice  45789  ichexmpl1  48258  cbvals  50623