Metamath Proof Explorer

Theorem 2pm13.193VD

Description: Virtual deduction proof of 2pm13.193 . The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. 2pm13.193 is 2pm13.193VD without virtual deductions and was automatically derived from 2pm13.193VD . (Contributed by Alan Sare, 8-Feb-2014) (Proof modification is discouraged.) (New usage is discouraged.)

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

Ref Expression
Assertion 2pm13.193VD ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) ↔ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) )

Proof

Step Hyp Ref Expression
1 idn1 ⊢ (    ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 )    ▶    ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 )    )
2 simpl ⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) → ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )
3 1 2 e1a ⊢ (    ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 )    ▶    ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 )    )
4 simpl ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → 𝑥 = 𝑢 )
5 3 4 e1a ⊢ (    ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 )    ▶    𝑥 = 𝑢    )
6 simpr ⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) → [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 )
7 1 6 e1a ⊢ (    ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 )    ▶    [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑    )
8 pm3.21 ⊢ ( 𝑥 = 𝑢 → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ∧ 𝑥 = 𝑢 ) ) )
9 5 7 8 e11 ⊢ (    ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 )    ▶    ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ∧ 𝑥 = 𝑢 )    )
10 sbequ2 ⊢ ( 𝑥 = 𝑢 → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 → [ 𝑣 / 𝑦 ] 𝜑 ) )
11 10 imdistanri ⊢ ( ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ∧ 𝑥 = 𝑢 ) → ( [ 𝑣 / 𝑦 ] 𝜑 ∧ 𝑥 = 𝑢 ) )
12 9 11 e1a ⊢ (    ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 )    ▶    ( [ 𝑣 / 𝑦 ] 𝜑 ∧ 𝑥 = 𝑢 )    )
13 simpl ⊢ ( ( [ 𝑣 / 𝑦 ] 𝜑 ∧ 𝑥 = 𝑢 ) → [ 𝑣 / 𝑦 ] 𝜑 )
14 12 13 e1a ⊢ (    ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 )    ▶    [ 𝑣 / 𝑦 ] 𝜑    )
15 simpr ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → 𝑦 = 𝑣 )
16 3 15 e1a ⊢ (    ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 )    ▶    𝑦 = 𝑣    )
17 pm3.2 ⊢ ( [ 𝑣 / 𝑦 ] 𝜑 → ( 𝑦 = 𝑣 → ( [ 𝑣 / 𝑦 ] 𝜑 ∧ 𝑦 = 𝑣 ) ) )
18 14 16 17 e11 ⊢ (    ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 )    ▶    ( [ 𝑣 / 𝑦 ] 𝜑 ∧ 𝑦 = 𝑣 )    )
19 sbequ2 ⊢ ( 𝑦 = 𝑣 → ( [ 𝑣 / 𝑦 ] 𝜑 → 𝜑 ) )
20 19 imdistanri ⊢ ( ( [ 𝑣 / 𝑦 ] 𝜑 ∧ 𝑦 = 𝑣 ) → ( 𝜑 ∧ 𝑦 = 𝑣 ) )
21 18 20 e1a ⊢ (    ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 )    ▶    ( 𝜑 ∧ 𝑦 = 𝑣 )    )
22 simpl ⊢ ( ( 𝜑 ∧ 𝑦 = 𝑣 ) → 𝜑 )
23 21 22 e1a ⊢ (    ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 )    ▶    𝜑    )
24 pm3.2 ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( 𝜑 → ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ) )
25 3 23 24 e11 ⊢ (    ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 )    ▶    ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 )    )
26 25 in1 ⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) → ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) )
27 idn1 ⊢ (    ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 )    ▶    ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 )    )
28 simpl ⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) → ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )
29 27 28 e1a ⊢ (    ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 )    ▶    ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 )    )
30 29 4 e1a ⊢ (    ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 )    ▶    𝑥 = 𝑢    )
31 29 15 e1a ⊢ (    ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 )    ▶    𝑦 = 𝑣    )
32 simpr ⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) → 𝜑 )
33 27 32 e1a ⊢ (    ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 )    ▶    𝜑    )
34 pm3.21 ⊢ ( 𝑦 = 𝑣 → ( 𝜑 → ( 𝜑 ∧ 𝑦 = 𝑣 ) ) )
35 31 33 34 e11 ⊢ (    ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 )    ▶    ( 𝜑 ∧ 𝑦 = 𝑣 )    )
36 sbequ1 ⊢ ( 𝑦 = 𝑣 → ( 𝜑 → [ 𝑣 / 𝑦 ] 𝜑 ) )
37 36 imdistanri ⊢ ( ( 𝜑 ∧ 𝑦 = 𝑣 ) → ( [ 𝑣 / 𝑦 ] 𝜑 ∧ 𝑦 = 𝑣 ) )
38 35 37 e1a ⊢ (    ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 )    ▶    ( [ 𝑣 / 𝑦 ] 𝜑 ∧ 𝑦 = 𝑣 )    )
39 simpl ⊢ ( ( [ 𝑣 / 𝑦 ] 𝜑 ∧ 𝑦 = 𝑣 ) → [ 𝑣 / 𝑦 ] 𝜑 )
40 38 39 e1a ⊢ (    ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 )    ▶    [ 𝑣 / 𝑦 ] 𝜑    )
41 pm3.21 ⊢ ( 𝑥 = 𝑢 → ( [ 𝑣 / 𝑦 ] 𝜑 → ( [ 𝑣 / 𝑦 ] 𝜑 ∧ 𝑥 = 𝑢 ) ) )
42 30 40 41 e11 ⊢ (    ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 )    ▶    ( [ 𝑣 / 𝑦 ] 𝜑 ∧ 𝑥 = 𝑢 )    )
43 sbequ1 ⊢ ( 𝑥 = 𝑢 → ( [ 𝑣 / 𝑦 ] 𝜑 → [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) )
44 43 imdistanri ⊢ ( ( [ 𝑣 / 𝑦 ] 𝜑 ∧ 𝑥 = 𝑢 ) → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ∧ 𝑥 = 𝑢 ) )
45 42 44 e1a ⊢ (    ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 )    ▶    ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ∧ 𝑥 = 𝑢 )    )
46 simpl ⊢ ( ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ∧ 𝑥 = 𝑢 ) → [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 )
47 45 46 e1a ⊢ (    ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 )    ▶    [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑    )
48 pm3.2 ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 → ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) ) )
49 29 47 48 e11 ⊢ (    ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 )    ▶    ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 )    )
50 49 in1 ⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) → ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) )
51 26 50 impbii ⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) ↔ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) )