Metamath Proof Explorer

Theorem 2sb5ndVD

Description: The following User's Proof is a Virtual Deduction proof (see wvd1 ) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. 2sb5nd is 2sb5ndVD without virtual deductions and was automatically derived from 2sb5ndVD . (Contributed by Alan Sare, 30-Apr-2014) (Proof modification is discouraged.) (New usage is discouraged.)

1:: |- ( ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> ( ( x = u /\ y = v ) /\ ph ) )
2:1: |- ( E. y ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> E. y ( ( x = u /\ y = v ) /\ ph ) )
3:: |- ( [ v / y ] ph -> A. y [ v / y ] ph )
4:3: |- [ u / x ] ( [ v / y ] ph -> A. y [ v / y ] ph )
5:4: |- ( [ u / x ] [ v / y ] ph -> [ u / x ] A. y [ v / y ] ph )
6:: |- (. -. A. x x = y ->. -. A. x x = y ).
7:: |- ( A. y y = x -> A. x x = y )
8:7: |- ( -. A. x x = y -> -. A. y y = x )
9:6,8: |- (. -. A. x x = y ->. -. A. y y = x ).
10:9: |- ( [ u / x ] A. y [ v / y ] ph <-> A. y [ u / x ] [ v / y ] ph )
11:5,10: |- ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph )
12:11: |- ( -. A. x x = y -> ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) )
13:: |- ( [ u / x ] [ v / y ] ph -> A. x [ u / x ] [ v / y ] ph )
14:: |- (. A. x x = y ->. A. x x = y ).
15:14: |- (. A. x x = y ->. ( A. x [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) ).
16:13,15: |- (. A. x x = y ->. ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) ).
17:16: |- ( A. x x = y -> ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) )
19:12,17: |- ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph )
20:19: |- ( E. y ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> ( E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) )
21:2,20: |- ( E. y ( ( x = u /\ y = v ) /\ ph ) <-> ( E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) )
22:21: |- ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) <-> E. x ( E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) )
23:13: |- ( E. x ( E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> ( E. x E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) )
24:22,23: |- ( ( E. x E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) )
240:24: |- ( ( E. x E. y ( x = u /\ y = v ) /\ ( E. x E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ) <-> ( E. x E. y ( x = u /\ y = v ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) )
241:: |- ( ( E. x E. y ( x = u /\ y = v ) /\ ( E. x E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ) <-> ( E. x E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) )
242:241,240: |- ( ( E. x E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> ( E. x E. y ( x = u /\ y = v ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) )
243:: |- ( ( E. x E. y ( x = u /\ y = v ) -> ( [ u / x ] [ v / y ] ph <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) ) <-> ( ( E. x E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> ( E. x E. y ( x = u /\ y = v ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) ) )
25:242,243: |- ( E. x E. y ( x = u /\ y = v ) -> ( [ u / x ] [ v / y ] ph <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) )
26:: |- ( ( -. A. x x = y \/ u = v ) <-> E. x E. y ( x = u /\ y = v ) )
qed:25,26: |- ( ( -. A. x x = y \/ u = v ) -> ( [ u / x ] [ v / y ] ph <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) )

Ref Expression
Assertion 2sb5ndVD ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ) )

Proof

Step Hyp Ref Expression
1 ax6e2ndeq ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )
2 anabs5 ⊢ ( ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) ) ↔ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) )
3 2pm13.193 ⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) ↔ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) )
4 3 exbii ⊢ ( ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) ↔ ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) )
5 hbs1 ⊢ ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 → ∀ 𝑥 [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 )
6 idn1 ⊢ (    ∀ 𝑥 𝑥 = 𝑦    ▶    ∀ 𝑥 𝑥 = 𝑦    )
7 axc11 ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 → ∀ 𝑦 [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) )
8 6 7 e1a ⊢ (    ∀ 𝑥 𝑥 = 𝑦    ▶    ( ∀ 𝑥 [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 → ∀ 𝑦 [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 )    )
9 imim1 ⊢ ( ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 → ∀ 𝑥 [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) → ( ( ∀ 𝑥 [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 → ∀ 𝑦 [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 → ∀ 𝑦 [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) ) )
10 5 8 9 e01 ⊢ (    ∀ 𝑥 𝑥 = 𝑦    ▶    ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 → ∀ 𝑦 [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 )    )
11 10 in1 ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 → ∀ 𝑦 [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) )
12 hbs1 ⊢ ( [ 𝑣 / 𝑦 ] 𝜑 → ∀ 𝑦 [ 𝑣 / 𝑦 ] 𝜑 )
13 12 sbt ⊢ [ 𝑢 / 𝑥 ] ( [ 𝑣 / 𝑦 ] 𝜑 → ∀ 𝑦 [ 𝑣 / 𝑦 ] 𝜑 )
14 sbi1 ⊢ ( [ 𝑢 / 𝑥 ] ( [ 𝑣 / 𝑦 ] 𝜑 → ∀ 𝑦 [ 𝑣 / 𝑦 ] 𝜑 ) → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 → [ 𝑢 / 𝑥 ] ∀ 𝑦 [ 𝑣 / 𝑦 ] 𝜑 ) )
15 13 14 e0a ⊢ ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 → [ 𝑢 / 𝑥 ] ∀ 𝑦 [ 𝑣 / 𝑦 ] 𝜑 )
16 idn1 ⊢ (    ¬ ∀ 𝑥 𝑥 = 𝑦    ▶    ¬ ∀ 𝑥 𝑥 = 𝑦    )
17 axc11n ⊢ ( ∀ 𝑦 𝑦 = 𝑥 → ∀ 𝑥 𝑥 = 𝑦 )
18 17 con3i ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ¬ ∀ 𝑦 𝑦 = 𝑥 )
19 16 18 e1a ⊢ (    ¬ ∀ 𝑥 𝑥 = 𝑦    ▶    ¬ ∀ 𝑦 𝑦 = 𝑥    )
20 sbal2 ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑥 → ( [ 𝑢 / 𝑥 ] ∀ 𝑦 [ 𝑣 / 𝑦 ] 𝜑 ↔ ∀ 𝑦 [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) )
21 19 20 e1a ⊢ (    ¬ ∀ 𝑥 𝑥 = 𝑦    ▶    ( [ 𝑢 / 𝑥 ] ∀ 𝑦 [ 𝑣 / 𝑦 ] 𝜑 ↔ ∀ 𝑦 [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 )    )
22 imbi2 ⊢ ( ( [ 𝑢 / 𝑥 ] ∀ 𝑦 [ 𝑣 / 𝑦 ] 𝜑 ↔ ∀ 𝑦 [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) → ( ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 → [ 𝑢 / 𝑥 ] ∀ 𝑦 [ 𝑣 / 𝑦 ] 𝜑 ) ↔ ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 → ∀ 𝑦 [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) ) )
23 22 biimpcd ⊢ ( ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 → [ 𝑢 / 𝑥 ] ∀ 𝑦 [ 𝑣 / 𝑦 ] 𝜑 ) → ( ( [ 𝑢 / 𝑥 ] ∀ 𝑦 [ 𝑣 / 𝑦 ] 𝜑 ↔ ∀ 𝑦 [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 → ∀ 𝑦 [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) ) )
24 15 21 23 e01 ⊢ (    ¬ ∀ 𝑥 𝑥 = 𝑦    ▶    ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 → ∀ 𝑦 [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 )    )
25 24 in1 ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 → ∀ 𝑦 [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) )
26 11 25 pm2.61i ⊢ ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 → ∀ 𝑦 [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 )
27 26 nf5i ⊢ Ⅎ 𝑦 [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑
28 27 19.41 ⊢ ( ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) ↔ ( ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) )
29 4 28 bitr3i ⊢ ( ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ↔ ( ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) )
30 29 exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ↔ ∃ 𝑥 ( ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) )
31 5 nf5i ⊢ Ⅎ 𝑥 [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑
32 31 19.41 ⊢ ( ∃ 𝑥 ( ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) ↔ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) )
33 30 32 bitr2i ⊢ ( ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) )
34 33 anbi2i ⊢ ( ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) ) ↔ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ) )
35 2 34 bitr3i ⊢ ( ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) ↔ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ) )
36 pm5.32 ⊢ ( ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ) ) ↔ ( ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) ↔ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ) ) )
37 35 36 mpbir ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ) )
38 1 37 sylbi ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ) )