Theorem cbvexvw 2037

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008

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

This theorem is referenced by:  cbvex2vw  2041  mojust  2532  mo4  2559  eujust  2564  cbveuvw  2598  iseqsetvlem  2792  cbvrexvw  3216  cbvrexdva2OLD  3323  euind  3695  reuind  3724  cbvopab1v  5185  cbvopab2v  5186  bm1.3iiOLD  5257  reusv2lem2  5354  relop  5814  dmcoss  5938  fv3  6876  exfo  7077  cbvoprab3v  7481  zfun  7712  suppimacnv  8153  frrlem1  8265  ac6sfi  9231  brwdom2  9526  ttrclss  9673  ttrclselem2  9679  aceq1  10070  aceq0  10071  aceq3lem  10073  dfac4  10075  kmlem2  10105  kmlem13  10116  axdc4lem  10408  zfac  10413  zfcndun  10568  zfcndac  10572  sup2  12139  supmul  12155  climmo  15523  summo  15683  prodmo  15902  gsumval3eu  19834  elpt  23459  gsumwrd2dccatlem  33006  1arithidomlem1  33506  1arithidom  33508  bnj1185  34783  fineqvac  35087  satf0op  35364  sat1el2xp  35366  cbvrexvw2  36215  cbvoprab1vw  36225  cbvoprab2vw  36226  cbvoprab13vw  36229  bj-bm1.3ii  37052  wl-ax12v2cl  37494  fdc  37739  sn-sup2  42479  cpcoll2d  44248  axc11next  44395  fnchoice  45023  ichexmpl1  47470