This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 2sb5nd

Description: Equivalence for double substitution 2sb5 without distinct x , y requirement. 2sb5nd is derived from 2sb5ndVD . (Contributed by Alan Sare, 30-Apr-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion 2sb5nd ⊢ ¬ ∀ x x = y ∨ u = v → u x v y φ ↔ ∃ x ∃ y x = u ∧ y = v ∧ φ

Proof

Step Hyp Ref Expression
1 ax6e2ndeq ⊢ ¬ ∀ x x = y ∨ u = v ↔ ∃ x ∃ y x = u ∧ y = v
2 anabs5 ⊢ ∃ x ∃ y x = u ∧ y = v ∧ ∃ x ∃ y x = u ∧ y = v ∧ u x v y φ ↔ ∃ x ∃ y x = u ∧ y = v ∧ u x v y φ
3 2pm13.193 ⊢ x = u ∧ y = v ∧ u x v y φ ↔ x = u ∧ y = v ∧ φ
4 3 exbii ⊢ ∃ y x = u ∧ y = v ∧ u x v y φ ↔ ∃ y x = u ∧ y = v ∧ φ
5 nfs1v ⊢ Ⅎ y v y φ
6 5 nfsb ⊢ Ⅎ y u x v y φ
7 6 19.41 ⊢ ∃ y x = u ∧ y = v ∧ u x v y φ ↔ ∃ y x = u ∧ y = v ∧ u x v y φ
8 4 7 bitr3i ⊢ ∃ y x = u ∧ y = v ∧ φ ↔ ∃ y x = u ∧ y = v ∧ u x v y φ
9 8 exbii ⊢ ∃ x ∃ y x = u ∧ y = v ∧ φ ↔ ∃ x ∃ y x = u ∧ y = v ∧ u x v y φ
10 nfs1v ⊢ Ⅎ x u x v y φ
11 10 19.41 ⊢ ∃ x ∃ y x = u ∧ y = v ∧ u x v y φ ↔ ∃ x ∃ y x = u ∧ y = v ∧ u x v y φ
12 9 11 bitr2i ⊢ ∃ x ∃ y x = u ∧ y = v ∧ u x v y φ ↔ ∃ x ∃ y x = u ∧ y = v ∧ φ
13 12 anbi2i ⊢ ∃ x ∃ y x = u ∧ y = v ∧ ∃ x ∃ y x = u ∧ y = v ∧ u x v y φ ↔ ∃ x ∃ y x = u ∧ y = v ∧ ∃ x ∃ y x = u ∧ y = v ∧ φ
14 2 13 bitr3i ⊢ ∃ x ∃ y x = u ∧ y = v ∧ u x v y φ ↔ ∃ x ∃ y x = u ∧ y = v ∧ ∃ x ∃ y x = u ∧ y = v ∧ φ
15 pm5.32 ⊢ ∃ x ∃ y x = u ∧ y = v → u x v y φ ↔ ∃ x ∃ y x = u ∧ y = v ∧ φ ↔ ∃ x ∃ y x = u ∧ y = v ∧ u x v y φ ↔ ∃ x ∃ y x = u ∧ y = v ∧ ∃ x ∃ y x = u ∧ y = v ∧ φ
16 14 15 mpbir ⊢ ∃ x ∃ y x = u ∧ y = v → u x v y φ ↔ ∃ x ∃ y x = u ∧ y = v ∧ φ
17 1 16 sylbi ⊢ ¬ ∀ x x = y ∨ u = v → u x v y φ ↔ ∃ x ∃ y x = u ∧ y = v ∧ φ