Theorem cbvexv1 2339

Description: Rule used to change bound variables, using implicit substitution. Version of cbvex 2399 with a disjoint variable condition, which does not require ax-13 2372. See cbvexvw 2040 for a version with two disjoint variable conditions, requiring fewer axioms, and cbvexv 2401 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 1860	. . . 4 ⊢ Ⅎ𝑦 ¬ 𝜑
3		cbvalv1.nf2	. . . . 5 ⊢ Ⅎ𝑥𝜓
4	3	nfn 1860	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝜓
5		cbvalv1.1	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
6	5	notbid 318	. . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
7	2, 4, 6	cbvalv1 2338	. . 3 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓)
8		alnex 1784	. . 3 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
9		alnex 1784	. . 3 ⊢ (∀𝑦 ¬ 𝜓 ↔ ¬ ∃𝑦𝜓)
10	7, 8, 9	3bitr3i 301	. 2 ⊢ (¬ ∃𝑥𝜑 ↔ ¬ ∃𝑦𝜓)
11	10	con4bii 321	1 ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205  ∀wal 1537  ∃wex 1782  Ⅎwnf 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-11 2154  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-ex 1783  df-nf 1787

This theorem is referenced by:  sb8ef  2353  exsb  2357  mof  2563  euf  2576  cbveuw  2607  clelabOLD  2884  issetf  3446  eqvincf  3580  rexab2  3636  euabsn  4662  eluniab  4854  cbvopab1  5149  cbvopab1g  5150  cbvopab2  5151  cbvopab1s  5152  axrep1  5210  axrep2  5212  axrep4  5214  opeliunxp  5654  dfdmf  5805  dfrnf  5859  elrnmpt1  5867  cbvoprab1  7362  cbvoprab2  7363  opabex3d  7808  opabex3rd  7809  opabex3  7810  zfcndrep  10370  fsum2dlem  15482  fprod2dlem  15690  2ndresdju  30986  bnj1146  32771  bnj607  32896  bnj1228  32991  fineqvrep  33064  poimirlem26  35803  sbcexf  36273  elunif  42559  stoweidlem46  43587  opeliun2xp  45668