Description: Version of cbvex4v 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-cbvex4vv.1 | ⊢ ( ( 𝑥 = 𝑣 ∧ 𝑦 = 𝑢 ) → ( 𝜑 ↔ 𝜓 ) ) | |
bj-cbvex4vv.2 | ⊢ ( ( 𝑧 = 𝑓 ∧ 𝑤 = 𝑔 ) → ( 𝜓 ↔ 𝜒 ) ) | ||
Assertion | bj-cbvex4vv | ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 𝜑 ↔ ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ∃ 𝑔 𝜒 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-cbvex4vv.1 | ⊢ ( ( 𝑥 = 𝑣 ∧ 𝑦 = 𝑢 ) → ( 𝜑 ↔ 𝜓 ) ) | |
2 | bj-cbvex4vv.2 | ⊢ ( ( 𝑧 = 𝑓 ∧ 𝑤 = 𝑔 ) → ( 𝜓 ↔ 𝜒 ) ) | |
3 | 1 | 2exbidv | ⊢ ( ( 𝑥 = 𝑣 ∧ 𝑦 = 𝑢 ) → ( ∃ 𝑧 ∃ 𝑤 𝜑 ↔ ∃ 𝑧 ∃ 𝑤 𝜓 ) ) |
4 | 3 | cbvex2vw | ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 𝜑 ↔ ∃ 𝑣 ∃ 𝑢 ∃ 𝑧 ∃ 𝑤 𝜓 ) |
5 | 2 | cbvex2vw | ⊢ ( ∃ 𝑧 ∃ 𝑤 𝜓 ↔ ∃ 𝑓 ∃ 𝑔 𝜒 ) |
6 | 5 | 2exbii | ⊢ ( ∃ 𝑣 ∃ 𝑢 ∃ 𝑧 ∃ 𝑤 𝜓 ↔ ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ∃ 𝑔 𝜒 ) |
7 | 4 6 | bitri | ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 𝜑 ↔ ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ∃ 𝑔 𝜒 ) |