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 41524
Description: Virtual deduction proof of csbuni 4853. 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 4853 is csbunigVD 41524 without virtual deductions and was automatically derived from csbunigVD 41524.
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 41200 . . . . . . . . . . . . 13 (   𝐴𝑉   ▶   𝐴𝑉   )
2 sbcg 3831 . . . . . . . . . . . . 13 (𝐴𝑉 → ([𝐴 / 𝑥]𝑧𝑦𝑧𝑦))
31, 2e1a 41253 . . . . . . . . . . . 12 (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑧𝑦𝑧𝑦)   )
4 sbcel2 4350 . . . . . . . . . . . . . 14 ([𝐴 / 𝑥]𝑦𝐵𝑦𝐴 / 𝑥𝐵)
54a1i 11 . . . . . . . . . . . . 13 (𝐴𝑉 → ([𝐴 / 𝑥]𝑦𝐵𝑦𝐴 / 𝑥𝐵))
61, 5e1a 41253 . . . . . . . . . . . 12 (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑦𝐵𝑦𝐴 / 𝑥𝐵)   )
7 pm4.38 637 . . . . . . . . . . . . 13 ((([𝐴 / 𝑥]𝑧𝑦𝑧𝑦) ∧ ([𝐴 / 𝑥]𝑦𝐵𝑦𝐴 / 𝑥𝐵)) → (([𝐴 / 𝑥]𝑧𝑦[𝐴 / 𝑥]𝑦𝐵) ↔ (𝑧𝑦𝑦𝐴 / 𝑥𝐵)))
87ex 416 . . . . . . . . . . . 12 (([𝐴 / 𝑥]𝑧𝑦𝑧𝑦) → (([𝐴 / 𝑥]𝑦𝐵𝑦𝐴 / 𝑥𝐵) → (([𝐴 / 𝑥]𝑧𝑦[𝐴 / 𝑥]𝑦𝐵) ↔ (𝑧𝑦𝑦𝐴 / 𝑥𝐵))))
93, 6, 8e11 41314 . . . . . . . . . . 11 (   𝐴𝑉   ▶   (([𝐴 / 𝑥]𝑧𝑦[𝐴 / 𝑥]𝑦𝐵) ↔ (𝑧𝑦𝑦𝐴 / 𝑥𝐵))   )
10 sbcan 3806 . . . . . . . . . . . . 13 ([𝐴 / 𝑥](𝑧𝑦𝑦𝐵) ↔ ([𝐴 / 𝑥]𝑧𝑦[𝐴 / 𝑥]𝑦𝐵))
1110a1i 11 . . . . . . . . . . . 12 (𝐴𝑉 → ([𝐴 / 𝑥](𝑧𝑦𝑦𝐵) ↔ ([𝐴 / 𝑥]𝑧𝑦[𝐴 / 𝑥]𝑦𝐵)))
121, 11e1a 41253 . . . . . . . . . . 11 (   𝐴𝑉   ▶   ([𝐴 / 𝑥](𝑧𝑦𝑦𝐵) ↔ ([𝐴 / 𝑥]𝑧𝑦[𝐴 / 𝑥]𝑦𝐵))   )
13 bibi1 355 . . . . . . . . . . . 12 (([𝐴 / 𝑥](𝑧𝑦𝑦𝐵) ↔ ([𝐴 / 𝑥]𝑧𝑦[𝐴 / 𝑥]𝑦𝐵)) → (([𝐴 / 𝑥](𝑧𝑦𝑦𝐵) ↔ (𝑧𝑦𝑦𝐴 / 𝑥𝐵)) ↔ (([𝐴 / 𝑥]𝑧𝑦[𝐴 / 𝑥]𝑦𝐵) ↔ (𝑧𝑦𝑦𝐴 / 𝑥𝐵))))
1413biimprcd 253 . . . . . . . . . . 11 ((([𝐴 / 𝑥]𝑧𝑦[𝐴 / 𝑥]𝑦𝐵) ↔ (𝑧𝑦𝑦𝐴 / 𝑥𝐵)) → (([𝐴 / 𝑥](𝑧𝑦𝑦𝐵) ↔ ([𝐴 / 𝑥]𝑧𝑦[𝐴 / 𝑥]𝑦𝐵)) → ([𝐴 / 𝑥](𝑧𝑦𝑦𝐵) ↔ (𝑧𝑦𝑦𝐴 / 𝑥𝐵))))
159, 12, 14e11 41314 . . . . . . . . . 10 (   𝐴𝑉   ▶   ([𝐴 / 𝑥](𝑧𝑦𝑦𝐵) ↔ (𝑧𝑦𝑦𝐴 / 𝑥𝐵))   )
1615gen11 41242 . . . . . . . . 9 (   𝐴𝑉   ▶   𝑦([𝐴 / 𝑥](𝑧𝑦𝑦𝐵) ↔ (𝑧𝑦𝑦𝐴 / 𝑥𝐵))   )
17 exbi 1848 . . . . . . . . 9 (∀𝑦([𝐴 / 𝑥](𝑧𝑦𝑦𝐵) ↔ (𝑧𝑦𝑦𝐴 / 𝑥𝐵)) → (∃𝑦[𝐴 / 𝑥](𝑧𝑦𝑦𝐵) ↔ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)))
1816, 17e1a 41253 . . . . . . . 8 (   𝐴𝑉   ▶   (∃𝑦[𝐴 / 𝑥](𝑧𝑦𝑦𝐵) ↔ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵))   )
19 sbcex2 3819 . . . . . . . . . 10 ([𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵) ↔ ∃𝑦[𝐴 / 𝑥](𝑧𝑦𝑦𝐵))
2019a1i 11 . . . . . . . . 9 (𝐴𝑉 → ([𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵) ↔ ∃𝑦[𝐴 / 𝑥](𝑧𝑦𝑦𝐵)))
211, 20e1a 41253 . . . . . . . 8 (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵) ↔ ∃𝑦[𝐴 / 𝑥](𝑧𝑦𝑦𝐵))   )
22 bibi1 355 . . . . . . . . 9 (([𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵) ↔ ∃𝑦[𝐴 / 𝑥](𝑧𝑦𝑦𝐵)) → (([𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵) ↔ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)) ↔ (∃𝑦[𝐴 / 𝑥](𝑧𝑦𝑦𝐵) ↔ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵))))
2322biimprcd 253 . . . . . . . 8 ((∃𝑦[𝐴 / 𝑥](𝑧𝑦𝑦𝐵) ↔ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)) → (([𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵) ↔ ∃𝑦[𝐴 / 𝑥](𝑧𝑦𝑦𝐵)) → ([𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵) ↔ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵))))
2418, 21, 23e11 41314 . . . . . . 7 (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵) ↔ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵))   )
2524gen11 41242 . . . . . 6 (   𝐴𝑉   ▶   𝑧([𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵) ↔ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵))   )
26 abbi 2891 . . . . . . 7 (∀𝑧([𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵) ↔ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)) ↔ {𝑧[𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵)} = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)})
2726biimpi 219 . . . . . 6 (∀𝑧([𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵) ↔ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)) → {𝑧[𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵)} = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)})
2825, 27e1a 41253 . . . . 5 (   𝐴𝑉   ▶   {𝑧[𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵)} = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)}   )
29 csbab 4372 . . . . . . 7 𝐴 / 𝑥{𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)} = {𝑧[𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵)}
3029a1i 11 . . . . . 6 (𝐴𝑉𝐴 / 𝑥{𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)} = {𝑧[𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵)})
311, 30e1a 41253 . . . . 5 (   𝐴𝑉   ▶   𝐴 / 𝑥{𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)} = {𝑧[𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵)}   )
32 eqeq2 2836 . . . . . 6 ({𝑧[𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵)} = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)} → (𝐴 / 𝑥{𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)} = {𝑧[𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵)} ↔ 𝐴 / 𝑥{𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)} = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)}))
3332biimpd 232 . . . . 5 ({𝑧[𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵)} = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)} → (𝐴 / 𝑥{𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)} = {𝑧[𝐴 / 𝑥]𝑦(𝑧𝑦𝑦𝐵)} → 𝐴 / 𝑥{𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)} = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)}))
3428, 31, 33e11 41314 . . . 4 (   𝐴𝑉   ▶   𝐴 / 𝑥{𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)} = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)}   )
35 df-uni 4825 . . . . . . 7 𝐵 = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)}
3635ax-gen 1797 . . . . . 6 𝑥 𝐵 = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)}
37 spsbc 3771 . . . . . 6 (𝐴𝑉 → (∀𝑥 𝐵 = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)} → [𝐴 / 𝑥] 𝐵 = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)}))
381, 36, 37e10 41320 . . . . 5 (   𝐴𝑉   ▶   [𝐴 / 𝑥] 𝐵 = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)}   )
39 sbceqg 4344 . . . . . 6 (𝐴𝑉 → ([𝐴 / 𝑥] 𝐵 = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)} ↔ 𝐴 / 𝑥 𝐵 = 𝐴 / 𝑥{𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)}))
4039biimpd 232 . . . . 5 (𝐴𝑉 → ([𝐴 / 𝑥] 𝐵 = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)} → 𝐴 / 𝑥 𝐵 = 𝐴 / 𝑥{𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)}))
411, 38, 40e11 41314 . . . 4 (   𝐴𝑉   ▶   𝐴 / 𝑥 𝐵 = 𝐴 / 𝑥{𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)}   )
42 eqeq2 2836 . . . . 5 (𝐴 / 𝑥{𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)} = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)} → (𝐴 / 𝑥 𝐵 = 𝐴 / 𝑥{𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)} ↔ 𝐴 / 𝑥 𝐵 = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)}))
4342biimpd 232 . . . 4 (𝐴 / 𝑥{𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)} = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)} → (𝐴 / 𝑥 𝐵 = 𝐴 / 𝑥{𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐵)} → 𝐴 / 𝑥 𝐵 = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)}))
4434, 41, 43e11 41314 . . 3 (   𝐴𝑉   ▶   𝐴 / 𝑥 𝐵 = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)}   )
45 df-uni 4825 . . 3 𝐴 / 𝑥𝐵 = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)}
46 eqeq2 2836 . . . 4 ( 𝐴 / 𝑥𝐵 = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)} → (𝐴 / 𝑥 𝐵 = 𝐴 / 𝑥𝐵𝐴 / 𝑥 𝐵 = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)}))
4746biimprcd 253 . . 3 (𝐴 / 𝑥 𝐵 = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)} → ( 𝐴 / 𝑥𝐵 = {𝑧 ∣ ∃𝑦(𝑧𝑦𝑦𝐴 / 𝑥𝐵)} → 𝐴 / 𝑥 𝐵 = 𝐴 / 𝑥𝐵))
4844, 45, 47e10 41320 . 2 (   𝐴𝑉   ▶   𝐴 / 𝑥 𝐵 = 𝐴 / 𝑥𝐵   )
4948in1 41197 1 (𝐴𝑉𝐴 / 𝑥 𝐵 = 𝐴 / 𝑥𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wal 1536   = wceq 1538  wex 1781  wcel 2115  {cab 2802  [wsbc 3758  csb 3866   cuni 4824
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-nul 4277  df-uni 4825  df-vd1 41196
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator