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

Theorem csbunigVD 43644
Description: Virtual deduction proof of csbuni 4939. 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. csbuni 4939 is csbunigVD 43644 without virtual deductions and was automatically derived from csbunigVD 43644.
1:: (   𝐴𝑉   ▶   𝐴𝑉   )
2:1: (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑧𝑦𝑧 𝑦)   )
3:1: (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑦𝐵𝑦 𝐴 / 𝑥𝐵)   )
4:2,3: (   𝐴𝑉   ▶   (([𝐴 / 𝑥]𝑧𝑦 [𝐴 / 𝑥]𝑦𝐵) ↔ (𝑧𝑦𝑦𝐴 / 𝑥𝐵))   )
5:1: (   𝐴𝑉   ▶   ([𝐴 / 𝑥](𝑧𝑦 𝑦𝐵) ↔ ([𝐴 / 𝑥]𝑧𝑦[𝐴 / 𝑥]𝑦𝐵))   )
6:4,5: (   𝐴𝑉   ▶   ([𝐴 / 𝑥](𝑧𝑦 𝑦𝐵) ↔ (𝑧𝑦𝑦𝐴 / 𝑥𝐵))   )
7:6: (   𝐴𝑉   ▶   𝑦([𝐴 / 𝑥](𝑧 𝑦𝑦𝐵) ↔ (𝑧𝑦𝑦𝐴 / 𝑥𝐵))   )
8:7: (   𝐴𝑉   ▶   (∃𝑦[𝐴 / 𝑥](𝑧 𝑦𝑦𝐵) ↔ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵))   )
9:1: (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑦(𝑧 𝑦𝑦𝐵) ↔ ∃𝑦[𝐴 / 𝑥](𝑧𝑦𝑦𝐵))   )
10:8,9: (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑦(𝑧 𝑦𝑦𝐵) ↔ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵))   )
11:10: (   𝐴𝑉   ▶   𝑧([𝐴 / 𝑥]𝑦( 𝑧𝑦𝑦𝐵) ↔ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵))   )
12:11: (   𝐴𝑉   ▶   {𝑧[𝐴 / 𝑥]𝑦( 𝑧𝑦𝑦𝐵)} = {𝑧 ∣ ∃𝑦(𝑧𝑦 𝑦𝐴 / 𝑥𝐵)}   )
13:1: (   𝐴𝑉   ▶   𝐴 / 𝑥{𝑧 ∣ ∃𝑦(𝑧 𝑦𝑦𝐵)} = {𝑧[𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵)}    )
14:12,13: (   𝐴𝑉   ▶   𝐴 / 𝑥{𝑧 ∣ ∃𝑦(𝑧 𝑦𝑦𝐵)} = {𝑧 ∣ ∃𝑦(𝑧𝑦 𝑦𝐴 / 𝑥𝐵)}   )
15:: 𝐵 = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)}
16:15: 𝑥 𝐵 = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦 𝐵)}
17:1,16: (   𝐴𝑉   ▶   [𝐴 / 𝑥] 𝐵 = {𝑧 𝑦(𝑧𝑦𝑦𝐵)}   )
18:1,17: (   𝐴𝑉   ▶   𝐴 / 𝑥 𝐵 = 𝐴 / 𝑥{𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)}   )
19:14,18: (   𝐴𝑉   ▶   𝐴 / 𝑥 𝐵 = {𝑧 𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)}   )
20:: 𝐴 / 𝑥𝐵 = {𝑧 ∣ ∃𝑦(𝑧𝑦 𝑦𝐴 / 𝑥𝐵)}
21:19,20: (   𝐴𝑉   ▶   𝐴 / 𝑥 𝐵 = 𝐴 / 𝑥𝐵   )
qed:21: (𝐴𝑉𝐴 / 𝑥 𝐵 = 𝐴 / 𝑥𝐵)
(Contributed by Alan Sare, 10-Nov-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
csbunigVD (𝐴𝑉𝐴 / 𝑥 𝐵 = 𝐴 / 𝑥𝐵)

Proof of Theorem csbunigVD
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 idn1 43320 . . . . . . . . . . . . 13 (   𝐴𝑉   ▶   𝐴𝑉   )
2 sbcg 3855 . . . . . . . . . . . . 13 (𝐴𝑉 → ([𝐴 / 𝑥]𝑧𝑦𝑧𝑦))
31, 2e1a 43373 . . . . . . . . . . . 12 (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑧𝑦𝑧𝑦)   )
4 sbcel2 4414 . . . . . . . . . . . . . 14 ([𝐴 / 𝑥]𝑦𝐵𝑦𝐴 / 𝑥𝐵)
54a1i 11 . . . . . . . . . . . . 13 (𝐴𝑉 → ([𝐴 / 𝑥]𝑦𝐵𝑦𝐴 / 𝑥𝐵))
61, 5e1a 43373 . . . . . . . . . . . 12 (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑦𝐵𝑦𝐴 / 𝑥𝐵)   )
7 pm4.38 636 . . . . . . . . . . . . 13 ((([𝐴 / 𝑥]𝑧𝑦𝑧𝑦) ∧ ([𝐴 / 𝑥]𝑦𝐵𝑦𝐴 / 𝑥𝐵)) → (([𝐴 / 𝑥]𝑧𝑦[𝐴 / 𝑥]𝑦𝐵) ↔ (𝑧𝑦𝑦𝐴 / 𝑥𝐵)))
87ex 413 . . . . . . . . . . . 12 (([𝐴 / 𝑥]𝑧𝑦𝑧𝑦) → (([𝐴 / 𝑥]𝑦𝐵𝑦𝐴 / 𝑥𝐵) → (([𝐴 / 𝑥]𝑧𝑦[𝐴 / 𝑥]𝑦𝐵) ↔ (𝑧𝑦𝑦𝐴 / 𝑥𝐵))))
93, 6, 8e11 43434 . . . . . . . . . . 11 (   𝐴𝑉   ▶   (([𝐴 / 𝑥]𝑧𝑦[𝐴 / 𝑥]𝑦𝐵) ↔ (𝑧𝑦𝑦𝐴 / 𝑥𝐵))   )
10 sbcan 3828 . . . . . . . . . . . . 13 ([𝐴 / 𝑥](𝑧𝑦𝑦𝐵) ↔ ([𝐴 / 𝑥]𝑧𝑦[𝐴 / 𝑥]𝑦𝐵))
1110a1i 11 . . . . . . . . . . . 12 (𝐴𝑉 → ([𝐴 / 𝑥](𝑧𝑦𝑦𝐵) ↔ ([𝐴 / 𝑥]𝑧𝑦[𝐴 / 𝑥]𝑦𝐵)))
121, 11e1a 43373 . . . . . . . . . . 11 (   𝐴𝑉   ▶   ([𝐴 / 𝑥](𝑧𝑦𝑦𝐵) ↔ ([𝐴 / 𝑥]𝑧𝑦[𝐴 / 𝑥]𝑦𝐵))   )
13 bibi1 351 . . . . . . . . . . . 12 (([𝐴 / 𝑥](𝑧𝑦𝑦𝐵) ↔ ([𝐴 / 𝑥]𝑧𝑦[𝐴 / 𝑥]𝑦𝐵)) → (([𝐴 / 𝑥](𝑧𝑦𝑦𝐵) ↔ (𝑧𝑦𝑦𝐴 / 𝑥𝐵)) ↔ (([𝐴 / 𝑥]𝑧𝑦[𝐴 / 𝑥]𝑦𝐵) ↔ (𝑧𝑦𝑦𝐴 / 𝑥𝐵))))
1413biimprcd 249 . . . . . . . . . . 11 ((([𝐴 / 𝑥]𝑧𝑦[𝐴 / 𝑥]𝑦𝐵) ↔ (𝑧𝑦𝑦𝐴 / 𝑥𝐵)) → (([𝐴 / 𝑥](𝑧𝑦𝑦𝐵) ↔ ([𝐴 / 𝑥]𝑧𝑦[𝐴 / 𝑥]𝑦𝐵)) → ([𝐴 / 𝑥](𝑧𝑦𝑦𝐵) ↔ (𝑧𝑦𝑦𝐴 / 𝑥𝐵))))
159, 12, 14e11 43434 . . . . . . . . . 10 (   𝐴𝑉   ▶   ([𝐴 / 𝑥](𝑧𝑦𝑦𝐵) ↔ (𝑧𝑦𝑦𝐴 / 𝑥𝐵))   )
1615gen11 43362 . . . . . . . . 9 (   𝐴𝑉   ▶   𝑦([𝐴 / 𝑥](𝑧𝑦𝑦𝐵) ↔ (𝑧𝑦𝑦𝐴 / 𝑥𝐵))   )
17 exbi 1849 . . . . . . . . 9 (∀𝑦([𝐴 / 𝑥](𝑧𝑦𝑦𝐵) ↔ (𝑧𝑦𝑦𝐴 / 𝑥𝐵)) → (∃𝑦[𝐴 / 𝑥](𝑧𝑦𝑦𝐵) ↔ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)))
1816, 17e1a 43373 . . . . . . . 8 (   𝐴𝑉   ▶   (∃𝑦[𝐴 / 𝑥](𝑧𝑦𝑦𝐵) ↔ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵))   )
19 sbcex2 3841 . . . . . . . . . 10 ([𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵) ↔ ∃𝑦[𝐴 / 𝑥](𝑧𝑦𝑦𝐵))
2019a1i 11 . . . . . . . . 9 (𝐴𝑉 → ([𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵) ↔ ∃𝑦[𝐴 / 𝑥](𝑧𝑦𝑦𝐵)))
211, 20e1a 43373 . . . . . . . 8 (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵) ↔ ∃𝑦[𝐴 / 𝑥](𝑧𝑦𝑦𝐵))   )
22 bibi1 351 . . . . . . . . 9 (([𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵) ↔ ∃𝑦[𝐴 / 𝑥](𝑧𝑦𝑦𝐵)) → (([𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵) ↔ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)) ↔ (∃𝑦[𝐴 / 𝑥](𝑧𝑦𝑦𝐵) ↔ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵))))
2322biimprcd 249 . . . . . . . 8 ((∃𝑦[𝐴 / 𝑥](𝑧𝑦𝑦𝐵) ↔ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)) → (([𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵) ↔ ∃𝑦[𝐴 / 𝑥](𝑧𝑦𝑦𝐵)) → ([𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵) ↔ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵))))
2418, 21, 23e11 43434 . . . . . . 7 (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵) ↔ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵))   )
2524gen11 43362 . . . . . 6 (   𝐴𝑉   ▶   𝑧([𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵) ↔ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵))   )
26 abbib 2804 . . . . . . 7 ({𝑧[𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵)} = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)} ↔ ∀𝑧([𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵) ↔ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)))
2726biimpri 227 . . . . . 6 (∀𝑧([𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵) ↔ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)) → {𝑧[𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵)} = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)})
2825, 27e1a 43373 . . . . 5 (   𝐴𝑉   ▶   {𝑧[𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵)} = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)}   )
29 csbab 4436 . . . . . . 7 𝐴 / 𝑥{𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)} = {𝑧[𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵)}
3029a1i 11 . . . . . 6 (𝐴𝑉𝐴 / 𝑥{𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)} = {𝑧[𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵)})
311, 30e1a 43373 . . . . 5 (   𝐴𝑉   ▶   𝐴 / 𝑥{𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)} = {𝑧[𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵)}   )
32 eqeq2 2744 . . . . . 6 ({𝑧[𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵)} = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)} → (𝐴 / 𝑥{𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)} = {𝑧[𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵)} ↔ 𝐴 / 𝑥{𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)} = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)}))
3332biimpd 228 . . . . 5 ({𝑧[𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵)} = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)} → (𝐴 / 𝑥{𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)} = {𝑧[𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵)} → 𝐴 / 𝑥{𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)} = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)}))
3428, 31, 33e11 43434 . . . 4 (   𝐴𝑉   ▶   𝐴 / 𝑥{𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)} = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)}   )
35 df-uni 4908 . . . . . . 7 𝐵 = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)}
3635ax-gen 1797 . . . . . 6 𝑥 𝐵 = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)}
37 spsbc 3789 . . . . . 6 (𝐴𝑉 → (∀𝑥 𝐵 = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)} → [𝐴 / 𝑥] 𝐵 = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)}))
381, 36, 37e10 43440 . . . . 5 (   𝐴𝑉   ▶   [𝐴 / 𝑥] 𝐵 = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)}   )
39 sbceqg 4408 . . . . . 6 (𝐴𝑉 → ([𝐴 / 𝑥] 𝐵 = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)} ↔ 𝐴 / 𝑥 𝐵 = 𝐴 / 𝑥{𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)}))
4039biimpd 228 . . . . 5 (𝐴𝑉 → ([𝐴 / 𝑥] 𝐵 = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)} → 𝐴 / 𝑥 𝐵 = 𝐴 / 𝑥{𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)}))
411, 38, 40e11 43434 . . . 4 (   𝐴𝑉   ▶   𝐴 / 𝑥 𝐵 = 𝐴 / 𝑥{𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)}   )
42 eqeq2 2744 . . . . 5 (𝐴 / 𝑥{𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)} = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)} → (𝐴 / 𝑥 𝐵 = 𝐴 / 𝑥{𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)} ↔ 𝐴 / 𝑥 𝐵 = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)}))
4342biimpd 228 . . . 4 (𝐴 / 𝑥{𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)} = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)} → (𝐴 / 𝑥 𝐵 = 𝐴 / 𝑥{𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)} → 𝐴 / 𝑥 𝐵 = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)}))
4434, 41, 43e11 43434 . . 3 (   𝐴𝑉   ▶   𝐴 / 𝑥 𝐵 = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)}   )
45 df-uni 4908 . . 3 𝐴 / 𝑥𝐵 = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)}
46 eqeq2 2744 . . . 4 ( 𝐴 / 𝑥𝐵 = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)} → (𝐴 / 𝑥 𝐵 = 𝐴 / 𝑥𝐵𝐴 / 𝑥 𝐵 = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)}))
4746biimprcd 249 . . 3 (𝐴 / 𝑥 𝐵 = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)} → ( 𝐴 / 𝑥𝐵 = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)} → 𝐴 / 𝑥 𝐵 = 𝐴 / 𝑥𝐵))
4844, 45, 47e10 43440 . 2 (   𝐴𝑉   ▶   𝐴 / 𝑥 𝐵 = 𝐴 / 𝑥𝐵   )
4948in1 43317 1 (𝐴𝑉𝐴 / 𝑥 𝐵 = 𝐴 / 𝑥𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wal 1539   = wceq 1541  wex 1781  wcel 2106  {cab 2709  [wsbc 3776  csb 3892   cuni 4907
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-nul 4322  df-uni 4908  df-vd1 43316
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator