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 | ⊢ ( 𝜑 → ( ∃ 𝑥 𝜓 ↔ ∃ 𝑦 𝜒 ) ) |
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 | ⊢ ( 𝜑 → ( ∃ 𝑥 𝜓 ↔ ∃ 𝑦 𝜒 ) ) |