Metamath Proof Explorer


Theorem bj-cbvexdv

Description: Version of cbvexd with a disjoint variable condition, which does not require ax-13 . (Contributed by BJ, 16-Jun-2019) (Proof modification is discouraged.)

Ref Expression
Hypotheses bj-cbvaldv.1 𝑦 𝜑
bj-cbvaldv.2 ( 𝜑 → Ⅎ 𝑦 𝜓 )
bj-cbvaldv.3 ( 𝜑 → ( 𝑥 = 𝑦 → ( 𝜓𝜒 ) ) )
Assertion bj-cbvexdv ( 𝜑 → ( ∃ 𝑥 𝜓 ↔ ∃ 𝑦 𝜒 ) )

Proof

Step Hyp Ref Expression
1 bj-cbvaldv.1 𝑦 𝜑
2 bj-cbvaldv.2 ( 𝜑 → Ⅎ 𝑦 𝜓 )
3 bj-cbvaldv.3 ( 𝜑 → ( 𝑥 = 𝑦 → ( 𝜓𝜒 ) ) )
4 2 nfnd ( 𝜑 → Ⅎ 𝑦 ¬ 𝜓 )
5 notbi ( ( 𝜓𝜒 ) ↔ ( ¬ 𝜓 ↔ ¬ 𝜒 ) )
6 3 5 syl6ib ( 𝜑 → ( 𝑥 = 𝑦 → ( ¬ 𝜓 ↔ ¬ 𝜒 ) ) )
7 1 4 6 bj-cbvaldv ( 𝜑 → ( ∀ 𝑥 ¬ 𝜓 ↔ ∀ 𝑦 ¬ 𝜒 ) )
8 7 notbid ( 𝜑 → ( ¬ ∀ 𝑥 ¬ 𝜓 ↔ ¬ ∀ 𝑦 ¬ 𝜒 ) )
9 df-ex ( ∃ 𝑥 𝜓 ↔ ¬ ∀ 𝑥 ¬ 𝜓 )
10 df-ex ( ∃ 𝑦 𝜒 ↔ ¬ ∀ 𝑦 ¬ 𝜒 )
11 8 9 10 3bitr4g ( 𝜑 → ( ∃ 𝑥 𝜓 ↔ ∃ 𝑦 𝜒 ) )