Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  2sb5ndVD Structured version   Visualization version   GIF version

Theorem 2sb5ndVD 39460
Description: The following User's Proof is a Virtual Deduction proof (see wvd1 39102) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. 2sb5nd 39093 is 2sb5ndVD 39460 without virtual deductions and was automatically derived from 2sb5ndVD 39460. (Contributed by Alan Sare, 30-Apr-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
1:: (((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][ 𝑣 / 𝑦]𝜑) ↔ ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))
2:1: (∃𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ ∃𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))
3:: ([𝑣 / 𝑦]𝜑 → ∀𝑦[𝑣 / 𝑦]𝜑)
4:3: [𝑢 / 𝑥]([𝑣 / 𝑦]𝜑 → ∀𝑦[𝑣 / 𝑦]𝜑)
5:4: ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → [𝑢 / 𝑥] 𝑦[𝑣 / 𝑦]𝜑)
6:: (   ¬ ∀𝑥𝑥 = 𝑦   ▶   ¬ ∀𝑥𝑥 = 𝑦   )
7:: (∀𝑦𝑦 = 𝑥 → ∀𝑥𝑥 = 𝑦)
8:7: (¬ ∀𝑥𝑥 = 𝑦 → ¬ ∀𝑦𝑦 = 𝑥)
9:6,8: (   ¬ ∀𝑥𝑥 = 𝑦   ▶   ¬ ∀𝑦𝑦 = 𝑥   )
10:9: ([𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑 ↔ ∀ 𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)
11:5,10: ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)
12:11: (¬ ∀𝑥𝑥 = 𝑦 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
13:: ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑥[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)
14:: (   𝑥𝑥 = 𝑦   ▶   𝑥𝑥 = 𝑦   )
15:14: (   𝑥𝑥 = 𝑦   ▶   (∀𝑥[𝑢 / 𝑥][ 𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   )
16:13,15: (   𝑥𝑥 = 𝑦   ▶   ([𝑢 / 𝑥][𝑣 / 𝑦 ]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   )
17:16: (∀𝑥𝑥 = 𝑦 → ([𝑢 / 𝑥][𝑣 / 𝑦] 𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
19:12,17: ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)
20:19: (∃𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ (∃𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
21:2,20: (∃𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) ↔ (∃𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
22:21: (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) ↔ ∃𝑥(∃𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
23:13: (∃𝑥(∃𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [ 𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
24:22,23: ((∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [ 𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))
240:24: ((∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ ( 𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)) ↔ (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)))
241:: ((∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ ( 𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)) ↔ (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
242:241,240: ((∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [ 𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)))
243:: ((∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) → ( [𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))) ↔ ((∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))))
25:242,243: (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) → ([ 𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)))
26:: ((¬ ∀𝑥𝑥 = 𝑦𝑢 = 𝑣) ↔ ∃𝑥 𝑦(𝑥 = 𝑢𝑦 = 𝑣))
qed:25,26: ((¬ ∀𝑥𝑥 = 𝑦𝑢 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)))
Assertion
Ref Expression
2sb5ndVD ((¬ ∀𝑥 𝑥 = 𝑦𝑢 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)))
Distinct variable groups:   𝑥,𝑢   𝑦,𝑢   𝑥,𝑣   𝑦,𝑣
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑣,𝑢)

Proof of Theorem 2sb5ndVD
StepHypRef Expression
1 ax6e2ndeq 39092 . 2 ((¬ ∀𝑥 𝑥 = 𝑦𝑢 = 𝑣) ↔ ∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣))
2 anabs5 868 . . . 4 ((∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)) ↔ (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
3 2pm13.193 39085 . . . . . . . . 9 (((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))
43exbii 1814 . . . . . . . 8 (∃𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ ∃𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))
5 hbs1 2464 . . . . . . . . . . . . 13 ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑥[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)
6 idn1 39107 . . . . . . . . . . . . . 14 (   𝑥 𝑥 = 𝑦   ▶   𝑥 𝑥 = 𝑦   )
7 axc11 2347 . . . . . . . . . . . . . 14 (∀𝑥 𝑥 = 𝑦 → (∀𝑥[𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
86, 7e1a 39169 . . . . . . . . . . . . 13 (   𝑥 𝑥 = 𝑦   ▶   (∀𝑥[𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   )
9 imim1 83 . . . . . . . . . . . . 13 (([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑥[𝑢 / 𝑥][𝑣 / 𝑦]𝜑) → ((∀𝑥[𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)))
105, 8, 9e01 39233 . . . . . . . . . . . 12 (   𝑥 𝑥 = 𝑦   ▶   ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   )
1110in1 39104 . . . . . . . . . . 11 (∀𝑥 𝑥 = 𝑦 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
12 hbs1 2464 . . . . . . . . . . . . . . 15 ([𝑣 / 𝑦]𝜑 → ∀𝑦[𝑣 / 𝑦]𝜑)
1312sbt 2447 . . . . . . . . . . . . . 14 [𝑢 / 𝑥]([𝑣 / 𝑦]𝜑 → ∀𝑦[𝑣 / 𝑦]𝜑)
14 sbi1 2420 . . . . . . . . . . . . . 14 ([𝑢 / 𝑥]([𝑣 / 𝑦]𝜑 → ∀𝑦[𝑣 / 𝑦]𝜑) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → [𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑))
1513, 14e0a 39316 . . . . . . . . . . . . 13 ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → [𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑)
16 idn1 39107 . . . . . . . . . . . . . . 15 (    ¬ ∀𝑥 𝑥 = 𝑦   ▶    ¬ ∀𝑥 𝑥 = 𝑦   )
17 axc11n 2342 . . . . . . . . . . . . . . . 16 (∀𝑦 𝑦 = 𝑥 → ∀𝑥 𝑥 = 𝑦)
1817con3i 150 . . . . . . . . . . . . . . 15 (¬ ∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑦 𝑦 = 𝑥)
1916, 18e1a 39169 . . . . . . . . . . . . . 14 (    ¬ ∀𝑥 𝑥 = 𝑦   ▶    ¬ ∀𝑦 𝑦 = 𝑥   )
20 sbal2 2489 . . . . . . . . . . . . . 14 (¬ ∀𝑦 𝑦 = 𝑥 → ([𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑 ↔ ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
2119, 20e1a 39169 . . . . . . . . . . . . 13 (    ¬ ∀𝑥 𝑥 = 𝑦   ▶   ([𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑 ↔ ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   )
22 imbi2 337 . . . . . . . . . . . . . 14 (([𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑 ↔ ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑) → (([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → [𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑) ↔ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)))
2322biimpcd 239 . . . . . . . . . . . . 13 (([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → [𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑) → (([𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑 ↔ ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)))
2415, 21, 23e01 39233 . . . . . . . . . . . 12 (    ¬ ∀𝑥 𝑥 = 𝑦   ▶   ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   )
2524in1 39104 . . . . . . . . . . 11 (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
2611, 25pm2.61i 176 . . . . . . . . . 10 ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)
2726nf5i 2064 . . . . . . . . 9 𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑
282719.41 2141 . . . . . . . 8 (∃𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ (∃𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
294, 28bitr3i 266 . . . . . . 7 (∃𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) ↔ (∃𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
3029exbii 1814 . . . . . 6 (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) ↔ ∃𝑥(∃𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
315nf5i 2064 . . . . . . 7 𝑥[𝑢 / 𝑥][𝑣 / 𝑦]𝜑
323119.41 2141 . . . . . 6 (∃𝑥(∃𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
3330, 32bitr2i 265 . . . . 5 ((∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))
3433anbi2i 730 . . . 4 ((∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)) ↔ (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)))
352, 34bitr3i 266 . . 3 ((∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)))
36 pm5.32 669 . . 3 ((∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))) ↔ ((∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) ∧ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))))
3735, 36mpbir 221 . 2 (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)))
381, 37sylbi 207 1 ((¬ ∀𝑥 𝑥 = 𝑦𝑢 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  wal 1521   = wceq 1523  wex 1744  [wsb 1937
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-ne 2824  df-v 3233  df-vd1 39103
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator