Metamath Proof Explorer


Theorem cbvex

Description: Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . Check out cbvexvw , cbvexv1 for weaker versions requiring fewer axioms. (Contributed by NM, 21-Jun-1993) (New usage is discouraged.)

Ref Expression
Hypotheses cbval.1 𝑦 𝜑
cbval.2 𝑥 𝜓
cbval.3 ( 𝑥 = 𝑦 → ( 𝜑𝜓 ) )
Assertion cbvex ( ∃ 𝑥 𝜑 ↔ ∃ 𝑦 𝜓 )

Proof

Step Hyp Ref Expression
1 cbval.1 𝑦 𝜑
2 cbval.2 𝑥 𝜓
3 cbval.3 ( 𝑥 = 𝑦 → ( 𝜑𝜓 ) )
4 1 nfn 𝑦 ¬ 𝜑
5 2 nfn 𝑥 ¬ 𝜓
6 3 notbid ( 𝑥 = 𝑦 → ( ¬ 𝜑 ↔ ¬ 𝜓 ) )
7 4 5 6 cbval ( ∀ 𝑥 ¬ 𝜑 ↔ ∀ 𝑦 ¬ 𝜓 )
8 alnex ( ∀ 𝑥 ¬ 𝜑 ↔ ¬ ∃ 𝑥 𝜑 )
9 alnex ( ∀ 𝑦 ¬ 𝜓 ↔ ¬ ∃ 𝑦 𝜓 )
10 7 8 9 3bitr3i ( ¬ ∃ 𝑥 𝜑 ↔ ¬ ∃ 𝑦 𝜓 )
11 10 con4bii ( ∃ 𝑥 𝜑 ↔ ∃ 𝑦 𝜓 )