Theorem cbvexv1 2351

Description: Rule used to change bound variables, using implicit substitution. Version of cbvex 2406 with a disjoint variable condition, which does not require ax-13 2379. See cbvexvw 2044 for a version with two disjoint variable conditions, requiring fewer axioms, and cbvexv 2408 for another variant. (Contributed by NM, 21-Jun-1993.) (Revised by BJ, 31-May-2019.)

Hypotheses

Ref	Expression
cbvalv1.nf1	⊢ Ⅎ𝑦𝜑
cbvalv1.nf2	⊢ Ⅎ𝑥𝜓
cbvalv1.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

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

Distinct variable group:   𝑥,𝑦

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

Proof of Theorem cbvexv1

Step	Hyp	Ref	Expression
1		cbvalv1.nf1	. . . . 5 ⊢ Ⅎ𝑦𝜑
2	1	nfn 1858	. . . 4 ⊢ Ⅎ𝑦 ¬ 𝜑
3		cbvalv1.nf2	. . . . 5 ⊢ Ⅎ𝑥𝜓
4	3	nfn 1858	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝜓
5		cbvalv1.1	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
6	5	notbid 321	. . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
7	2, 4, 6	cbvalv1 2350	. . 3 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓)
8	7	notbii 323	. 2 ⊢ (¬ ∀𝑥 ¬ 𝜑 ↔ ¬ ∀𝑦 ¬ 𝜓)
9		df-ex 1782	. 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
10		df-ex 1782	. 2 ⊢ (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓)
11	8, 9, 10	3bitr4i 306	1 ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209  ∀wal 1536  ∃wex 1781  Ⅎwnf 1785

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 1911  ax-6 1970  ax-7 2015  ax-11 2158  ax-12 2175

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786

This theorem is referenced by:  sb8ev  2363  exsb  2367  mof  2622  euf  2636  cbveuw  2666  clelab  2933  issetf  3454  eqvincf  3591  rexab2  3639  rexab2OLD  3640  euabsn  4622  eluniab  4815  cbvopab1  5103  cbvopab1g  5104  cbvopab2  5105  cbvopab1s  5106  axrep1  5155  axrep2  5157  axrep4  5159  opeliunxp  5583  dfdmf  5729  dfrnf  5784  elrnmpt1  5794  cbvoprab1  7220  cbvoprab2  7221  opabex3d  7648  opabex3rd  7649  opabex3  7650  zfcndrep  10025  fsum2dlem  15117  fprod2dlem  15326  2ndresdju  30411  bnj1146  32173  bnj607  32298  bnj1228  32393  poimirlem26  35083  sbcexf  35553  elunif  41645  stoweidlem46  42688  opeliun2xp  44734