Theorem cbvexvw 2033

Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvexv 2403 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 2032	. . 3 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓)
4	3	notbii 320	. 2 ⊢ (¬ ∀𝑥 ¬ 𝜑 ↔ ¬ ∀𝑦 ¬ 𝜓)
5		df-ex 1776	. 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
6		df-ex 1776	. 2 ⊢ (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓)
7	4, 5, 6	3bitr4i 303	1 ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206  ∀wal 1534  ∃wex 1775

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004

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

This theorem is referenced by:  cbvex2vw  2037  mojust  2536  mo4  2563  eujust  2568  cbveuvw  2602  iseqsetvlem  2802  cbvrexvw  3235  cbvrexdva2OLD  3347  euind  3732  reuind  3761  cbvopab1v  5226  cbvopab2v  5228  bm1.3iiOLD  5307  reusv2lem2  5404  relop  5863  dmcoss  5987  fv3  6924  exfo  7124  cbvoprab3v  7524  zfun  7754  suppimacnv  8197  frrlem1  8309  wfrlem1OLD  8346  ac6sfi  9317  brwdom2  9610  ttrclss  9757  ttrclselem2  9763  aceq1  10154  aceq0  10155  aceq3lem  10157  dfac4  10159  kmlem2  10189  kmlem13  10200  axdc4lem  10492  zfac  10497  zfcndun  10652  zfcndac  10656  sup2  12221  supmul  12237  climmo  15589  summo  15749  prodmo  15968  gsumval3eu  19936  elpt  23595  gsumwrd2dccatlem  33051  1arithidomlem1  33542  1arithidom  33544  bnj1185  34785  fineqvac  35089  satf0op  35361  sat1el2xp  35363  cbvrexvw2  36209  cbvoprab1vw  36219  cbvoprab2vw  36220  cbvoprab13vw  36223  bj-bm1.3ii  37046  wl-ax12v2cl  37486  fdc  37731  sn-sup2  42477  cpcoll2d  44254  axc11next  44401  fnchoice  44966  ichexmpl1  47393