Theorem cbvexv1 2333

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205  ∀wal 1532  ∃wex 1774  Ⅎwnf 1778

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-11 2147  ax-12 2164

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-ex 1775  df-nf 1779

This theorem is referenced by:  sb8ef  2346  exsb  2350  mof  2552  euf  2565  cbveuw  2596  clelabOLD  2875  eqvincf  3634  rexab2  3692  euabsn  4726  eluniab  4917  cbvopab1  5217  cbvopab1g  5218  cbvopab2  5219  cbvopab1s  5220  axrep1  5280  axrep2  5282  axrep4  5284  opeliunxp  5739  dfdmf  5893  dfrnf  5946  elrnmpt1  5954  cbvoprab1  7501  cbvoprab2  7502  opabex3d  7963  opabex3rd  7964  opabex3  7965  zfcndrep  10629  fsum2dlem  15740  fprod2dlem  15948  2ndresdju  32418  bnj1146  34358  bnj607  34483  bnj1228  34578  fineqvrep  34651  poimirlem26  37054  sbcexf  37523  elunif  44301  stoweidlem46  45357  opeliun2xp  47319