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  3671  reuind  3700  cbvopab1v  5164  cbvopab2v  5165  bm1.3iiOLD  5237  reusv2lem2  5336  axprg  5374  relop  5799  dmcoss  5924  dmcossOLD  5925  fv3  6852  exfo  7051  cbvoprab3v  7452  zfun  7683  suppimacnv  8117  frrlem1  8229  ac6sfi  9187  brwdom2  9481  ttrclss  9632  ttrclselem2  9638  aceq1  10030  aceq0  10031  aceq3lem  10033  dfac4  10035  kmlem2  10065  kmlem13  10076  axdc4lem  10368  zfac  10373  zfcndun  10529  zfcndac  10533  sup2  12103  supmul  12119  climmo  15510  summo  15670  prodmo  15892  gsumval3eu  19870  elpt  23547  gsumwrd2dccatlem  33153  1arithidomlem1  33610  1arithidom  33612  bnj1185  34951  axprALT2  35269  fineqvac  35276  axreg  35287  axregscl  35288  tz9.1regs  35294  satf0op  35575  sat1el2xp  35577  cbvrexvw2  36425  cbvoprab1vw  36435  cbvoprab2vw  36436  cbvoprab13vw  36439  mh-regprimbi  36743  bj-bm1.3ii  37387  wl-ax12v2cl  37836  wl-dfclel  37845  fdc  38080  sn-sup2  42950  cpcoll2d  44704  axc11next  44851  fnchoice  45478  ichexmpl1  47941