Theorem cbvexv1 2332

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205  ∀wal 1531  ∃wex 1773  Ⅎwnf 1777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-11 2146  ax-12 2166

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-ex 1774  df-nf 1778

This theorem is referenced by:  sb8ef  2345  exsb  2349  mof  2551  euf  2564  cbveuw  2594  clelabOLD  2872  eqvincf  3633  rexab2  3691  euabsn  4732  eluniab  4923  cbvopab1  5224  cbvopab1g  5225  cbvopab2  5226  cbvopab1s  5227  axrep1  5287  axrep2  5289  axrep4  5291  opeliunxp  5745  dfdmf  5899  dfrnf  5952  elrnmpt1  5960  cbvoprab1  7507  cbvoprab2  7508  opabex3d  7970  opabex3rd  7971  opabex3  7972  zfcndrep  10639  fsum2dlem  15752  fprod2dlem  15960  2ndresdju  32516  bnj1146  34553  bnj607  34678  bnj1228  34773  fineqvrep  34846  poimirlem26  37250  sbcexf  37719  elunif  44520  stoweidlem46  45572  opeliun2xp  47582