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

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

Proof of Theorem csbfv12gALTVD
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 idn1 38616 . . . . . . . . . . 11 (   𝐴𝐶   ▶   𝐴𝐶   )
2 sbceqg 3982 . . . . . . . . . . 11 (𝐴𝐶 → ([𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦} ↔ 𝐴 / 𝑥(𝐹 “ {𝐵}) = 𝐴 / 𝑥{𝑦}))
31, 2e1a 38678 . . . . . . . . . 10 (   𝐴𝐶   ▶   ([𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦} ↔ 𝐴 / 𝑥(𝐹 “ {𝐵}) = 𝐴 / 𝑥{𝑦})   )
4 csbima12 5481 . . . . . . . . . . . . . 14 𝐴 / 𝑥(𝐹 “ {𝐵}) = (𝐴 / 𝑥𝐹𝐴 / 𝑥{𝐵})
54a1i 11 . . . . . . . . . . . . 13 (𝐴𝐶𝐴 / 𝑥(𝐹 “ {𝐵}) = (𝐴 / 𝑥𝐹𝐴 / 𝑥{𝐵}))
61, 5e1a 38678 . . . . . . . . . . . 12 (   𝐴𝐶   ▶   𝐴 / 𝑥(𝐹 “ {𝐵}) = (𝐴 / 𝑥𝐹𝐴 / 𝑥{𝐵})   )
7 csbsng 4241 . . . . . . . . . . . . . 14 (𝐴𝐶𝐴 / 𝑥{𝐵} = {𝐴 / 𝑥𝐵})
81, 7e1a 38678 . . . . . . . . . . . . 13 (   𝐴𝐶   ▶   𝐴 / 𝑥{𝐵} = {𝐴 / 𝑥𝐵}   )
9 imaeq2 5460 . . . . . . . . . . . . 13 (𝐴 / 𝑥{𝐵} = {𝐴 / 𝑥𝐵} → (𝐴 / 𝑥𝐹𝐴 / 𝑥{𝐵}) = (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}))
108, 9e1a 38678 . . . . . . . . . . . 12 (   𝐴𝐶   ▶   (𝐴 / 𝑥𝐹𝐴 / 𝑥{𝐵}) = (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵})   )
11 eqeq1 2625 . . . . . . . . . . . . 13 (𝐴 / 𝑥(𝐹 “ {𝐵}) = (𝐴 / 𝑥𝐹𝐴 / 𝑥{𝐵}) → (𝐴 / 𝑥(𝐹 “ {𝐵}) = (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) ↔ (𝐴 / 𝑥𝐹𝐴 / 𝑥{𝐵}) = (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵})))
1211biimprd 238 . . . . . . . . . . . 12 (𝐴 / 𝑥(𝐹 “ {𝐵}) = (𝐴 / 𝑥𝐹𝐴 / 𝑥{𝐵}) → ((𝐴 / 𝑥𝐹𝐴 / 𝑥{𝐵}) = (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) → 𝐴 / 𝑥(𝐹 “ {𝐵}) = (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵})))
136, 10, 12e11 38739 . . . . . . . . . . 11 (   𝐴𝐶   ▶   𝐴 / 𝑥(𝐹 “ {𝐵}) = (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵})   )
14 csbconstg 3544 . . . . . . . . . . . 12 (𝐴𝐶𝐴 / 𝑥{𝑦} = {𝑦})
151, 14e1a 38678 . . . . . . . . . . 11 (   𝐴𝐶   ▶   𝐴 / 𝑥{𝑦} = {𝑦}   )
16 eqeq12 2634 . . . . . . . . . . . 12 ((𝐴 / 𝑥(𝐹 “ {𝐵}) = (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) ∧ 𝐴 / 𝑥{𝑦} = {𝑦}) → (𝐴 / 𝑥(𝐹 “ {𝐵}) = 𝐴 / 𝑥{𝑦} ↔ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}))
1716ex 450 . . . . . . . . . . 11 (𝐴 / 𝑥(𝐹 “ {𝐵}) = (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) → (𝐴 / 𝑥{𝑦} = {𝑦} → (𝐴 / 𝑥(𝐹 “ {𝐵}) = 𝐴 / 𝑥{𝑦} ↔ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦})))
1813, 15, 17e11 38739 . . . . . . . . . 10 (   𝐴𝐶   ▶   (𝐴 / 𝑥(𝐹 “ {𝐵}) = 𝐴 / 𝑥{𝑦} ↔ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦})   )
19 bibi1 341 . . . . . . . . . . 11 (([𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦} ↔ 𝐴 / 𝑥(𝐹 “ {𝐵}) = 𝐴 / 𝑥{𝑦}) → (([𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦} ↔ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}) ↔ (𝐴 / 𝑥(𝐹 “ {𝐵}) = 𝐴 / 𝑥{𝑦} ↔ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦})))
2019biimprd 238 . . . . . . . . . 10 (([𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦} ↔ 𝐴 / 𝑥(𝐹 “ {𝐵}) = 𝐴 / 𝑥{𝑦}) → ((𝐴 / 𝑥(𝐹 “ {𝐵}) = 𝐴 / 𝑥{𝑦} ↔ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}) → ([𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦} ↔ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦})))
213, 18, 20e11 38739 . . . . . . . . 9 (   𝐴𝐶   ▶   ([𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦} ↔ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦})   )
2221gen11 38667 . . . . . . . 8 (   𝐴𝐶   ▶   𝑦([𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦} ↔ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦})   )
23 abbi 2736 . . . . . . . . 9 (∀𝑦([𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦} ↔ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}) ↔ {𝑦[𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}})
2423biimpi 206 . . . . . . . 8 (∀𝑦([𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦} ↔ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}) → {𝑦[𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}})
2522, 24e1a 38678 . . . . . . 7 (   𝐴𝐶   ▶   {𝑦[𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}}   )
26 csbab 4006 . . . . . . . . 9 𝐴 / 𝑥{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦[𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦}}
2726a1i 11 . . . . . . . 8 (𝐴𝐶𝐴 / 𝑥{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦[𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦}})
281, 27e1a 38678 . . . . . . 7 (   𝐴𝐶   ▶   𝐴 / 𝑥{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦[𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦}}   )
29 eqeq2 2632 . . . . . . . 8 ({𝑦[𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}} → (𝐴 / 𝑥{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦[𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦}} ↔ 𝐴 / 𝑥{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}}))
3029biimpd 219 . . . . . . 7 ({𝑦[𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}} → (𝐴 / 𝑥{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦[𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦}} → 𝐴 / 𝑥{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}}))
3125, 28, 30e11 38739 . . . . . 6 (   𝐴𝐶   ▶   𝐴 / 𝑥{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}}   )
32 unieq 4442 . . . . . 6 (𝐴 / 𝑥{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}} → 𝐴 / 𝑥{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}})
3331, 32e1a 38678 . . . . 5 (   𝐴𝐶   ▶    𝐴 / 𝑥{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}}   )
34 csbuni 4464 . . . . . . 7 𝐴 / 𝑥 {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = 𝐴 / 𝑥{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}}
3534a1i 11 . . . . . 6 (𝐴𝐶𝐴 / 𝑥 {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = 𝐴 / 𝑥{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}})
361, 35e1a 38678 . . . . 5 (   𝐴𝐶   ▶   𝐴 / 𝑥 {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = 𝐴 / 𝑥{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}}   )
37 eqeq2 2632 . . . . . 6 ( 𝐴 / 𝑥{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}} → (𝐴 / 𝑥 {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = 𝐴 / 𝑥{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} ↔ 𝐴 / 𝑥 {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}}))
3837biimpd 219 . . . . 5 ( 𝐴 / 𝑥{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}} → (𝐴 / 𝑥 {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = 𝐴 / 𝑥{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} → 𝐴 / 𝑥 {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}}))
3933, 36, 38e11 38739 . . . 4 (   𝐴𝐶   ▶   𝐴 / 𝑥 {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}}   )
40 dffv4 6186 . . . . . 6 (𝐹𝐵) = {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}}
4140ax-gen 1721 . . . . 5 𝑥(𝐹𝐵) = {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}}
42 csbeq2 3535 . . . . . 6 (∀𝑥(𝐹𝐵) = {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} → 𝐴 / 𝑥(𝐹𝐵) = 𝐴 / 𝑥 {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}})
4342a1i 11 . . . . 5 (𝐴𝐶 → (∀𝑥(𝐹𝐵) = {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} → 𝐴 / 𝑥(𝐹𝐵) = 𝐴 / 𝑥 {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}}))
441, 41, 43e10 38745 . . . 4 (   𝐴𝐶   ▶   𝐴 / 𝑥(𝐹𝐵) = 𝐴 / 𝑥 {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}}   )
45 eqeq2 2632 . . . . 5 (𝐴 / 𝑥 {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}} → (𝐴 / 𝑥(𝐹𝐵) = 𝐴 / 𝑥 {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} ↔ 𝐴 / 𝑥(𝐹𝐵) = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}}))
4645biimpd 219 . . . 4 (𝐴 / 𝑥 {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}} → (𝐴 / 𝑥(𝐹𝐵) = 𝐴 / 𝑥 {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} → 𝐴 / 𝑥(𝐹𝐵) = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}}))
4739, 44, 46e11 38739 . . 3 (   𝐴𝐶   ▶   𝐴 / 𝑥(𝐹𝐵) = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}}   )
48 dffv4 6186 . . 3 (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵) = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}}
49 eqeq2 2632 . . . 4 ((𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵) = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}} → (𝐴 / 𝑥(𝐹𝐵) = (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵) ↔ 𝐴 / 𝑥(𝐹𝐵) = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}}))
5049biimprcd 240 . . 3 (𝐴 / 𝑥(𝐹𝐵) = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}} → ((𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵) = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}} → 𝐴 / 𝑥(𝐹𝐵) = (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵)))
5147, 48, 50e10 38745 . 2 (   𝐴𝐶   ▶   𝐴 / 𝑥(𝐹𝐵) = (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵)   )
5251in1 38613 1 (𝐴𝐶𝐴 / 𝑥(𝐹𝐵) = (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wal 1480   = wceq 1482  wcel 1989  {cab 2607  [wsbc 3433  csb 3531  {csn 4175   cuni 4434  cima 5115  cfv 5886
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-8 1991  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-sep 4779  ax-nul 4787  ax-pow 4841  ax-pr 4904
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1485  df-fal 1488  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ral 2916  df-rex 2917  df-rab 2920  df-v 3200  df-sbc 3434  df-csb 3532  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-nul 3914  df-if 4085  df-sn 4176  df-pr 4178  df-op 4182  df-uni 4435  df-br 4652  df-opab 4711  df-xp 5118  df-cnv 5120  df-dm 5122  df-rn 5123  df-res 5124  df-ima 5125  df-iota 5849  df-fv 5894  df-vd1 38612
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator