Theorem cbvexv1 2343

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-11 2158  ax-12 2175

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

This theorem is referenced by:  sb8ev  2355  exsb  2359  mof  2565  euf  2578  cbveuw  2609  clelabOLD  2886  issetf  3445  eqvincf  3581  rexab2  3639  rexab2OLD  3640  euabsn  4668  eluniab  4860  cbvopab1  5154  cbvopab1g  5155  cbvopab2  5156  cbvopab1s  5157  axrep1  5215  axrep2  5217  axrep4  5219  opeliunxp  5655  dfdmf  5804  dfrnf  5858  elrnmpt1  5866  cbvoprab1  7356  cbvoprab2  7357  opabex3d  7801  opabex3rd  7802  opabex3  7803  zfcndrep  10371  fsum2dlem  15480  fprod2dlem  15688  2ndresdju  30982  bnj1146  32767  bnj607  32892  bnj1228  32987  fineqvrep  33060  poimirlem26  35799  sbcexf  36269  elunif  42529  stoweidlem46  43558  opeliun2xp  45637