Theorem cbvexv1 2338

Description: Rule used to change bound variables, using implicit substitution. Version of cbvex 2398 with a disjoint variable condition, which does not require ax-13 2371. See cbvexvw 2040 for a version with two disjoint variable conditions, requiring fewer axioms, and cbvexv 2400 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 317	. . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
7	2, 4, 6	cbvalv1 2337	. . 3 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓)
8		alnex 1783	. . 3 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
9		alnex 1783	. . 3 ⊢ (∀𝑦 ¬ 𝜓 ↔ ¬ ∃𝑦𝜓)
10	7, 8, 9	3bitr3i 300	. 2 ⊢ (¬ ∃𝑥𝜑 ↔ ¬ ∃𝑦𝜓)
11	10	con4bii 320	1 ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205  ∀wal 1539  ∃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 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 846  df-ex 1782  df-nf 1786

This theorem is referenced by:  sb8ef  2351  exsb  2355  mof  2557  euf  2570  cbveuw  2601  clelabOLD  2880  issetf  3488  eqvincf  3638  rexab2  3695  euabsn  4730  eluniab  4923  cbvopab1  5223  cbvopab1g  5224  cbvopab2  5225  cbvopab1s  5226  axrep1  5286  axrep2  5288  axrep4  5290  opeliunxp  5743  dfdmf  5896  dfrnf  5949  elrnmpt1  5957  cbvoprab1  7495  cbvoprab2  7496  opabex3d  7951  opabex3rd  7952  opabex3  7953  zfcndrep  10608  fsum2dlem  15715  fprod2dlem  15923  2ndresdju  31869  bnj1146  33797  bnj607  33922  bnj1228  34017  fineqvrep  34090  poimirlem26  36509  sbcexf  36978  elunif  43690  stoweidlem46  44752  opeliun2xp  46998