Theorem cbvexv 2275

Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 21-Jun-1993.) Remove dependency on ax-10 2019. (Revised by Wolf Lammen, 17-Jul-2021.)

Hypothesis

Ref	Expression
cbvalv.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
cbvexv	⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)

Distinct variable groups:   𝜑,𝑦   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem cbvexv

Step	Hyp	Ref	Expression
1		cbvalv.1	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
2	1	notbid 308	. . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
3	2	cbvalv 2273	. . 3 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓)
4	3	notbii 310	. 2 ⊢ (¬ ∀𝑥 ¬ 𝜑 ↔ ¬ ∀𝑦 ¬ 𝜓)
5		df-ex 1705	. 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
6		df-ex 1705	. 2 ⊢ (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓)
7	4, 5, 6	3bitr4i 292	1 ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196  ∀wal 1481  ∃wex 1704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-11 2034  ax-12 2047  ax-13 2246

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705

This theorem is referenced by:  cbvex2v  2287  eujust  2472  euind  3393  reuind  3411  cbvopab2v  4727  bm1.3ii  4784  reusv2lem2  4869  reusv2lem2OLD  4870  relop  5272  dmcoss  5385  fv3  6206  exfo  6377  zfun  6950  wfrlem1  7414  ac6sfi  8204  brwdom2  8478  aceq1  8940  aceq0  8941  aceq3lem  8943  dfac4  8945  kmlem2  8973  kmlem13  8984  axdc4lem  9277  zfac  9282  zfcndun  9437  zfcndac  9441  sup2  10979  supmul  10995  climmo  14288  summo  14448  prodmo  14666  gsumval3eu  18305  elpt  21375  bnj1185  30864  frrlem1  31780  fdc  33541  axc11next  38607  fnchoice  39188