Theorem cbvexv1 2341

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 2041 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 1861	. . . 4 ⊢ Ⅎ𝑦 ¬ 𝜑
3		cbvalv1.nf2	. . . . 5 ⊢ Ⅎ𝑥𝜓
4	3	nfn 1861	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝜓
5		cbvalv1.1	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
6	5	notbid 317	. . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
7	2, 4, 6	cbvalv1 2340	. . 3 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓)
8		alnex 1785	. . 3 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
9		alnex 1785	. . 3 ⊢ (∀𝑦 ¬ 𝜓 ↔ ¬ ∃𝑦𝜓)
10	7, 8, 9	3bitr3i 300	. 2 ⊢ (¬ ∃𝑥𝜑 ↔ ¬ ∃𝑦𝜓)
11	10	con4bii 320	1 ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-11 2156  ax-12 2173

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-ex 1784  df-nf 1788

This theorem is referenced by:  sb8ev  2353  exsb  2357  mof  2563  euf  2576  cbveuw  2607  clelabOLD  2883  issetf  3436  eqvincf  3572  rexab2  3630  rexab2OLD  3631  euabsn  4659  eluniab  4851  cbvopab1  5145  cbvopab1g  5146  cbvopab2  5147  cbvopab1s  5148  axrep1  5206  axrep2  5208  axrep4  5210  opeliunxp  5645  dfdmf  5794  dfrnf  5848  elrnmpt1  5856  cbvoprab1  7340  cbvoprab2  7341  opabex3d  7781  opabex3rd  7782  opabex3  7783  zfcndrep  10301  fsum2dlem  15410  fprod2dlem  15618  2ndresdju  30887  bnj1146  32671  bnj607  32796  bnj1228  32891  fineqvrep  32964  poimirlem26  35730  sbcexf  36200  elunif  42448  stoweidlem46  43477  opeliun2xp  45556