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 43171
Description: Virtual deduction proof of csbfv12 6890. 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. csbfv12 6890 is csbfv12gALTVD 43171 without virtual deductions and was automatically derived from csbfv12gALTVD 43171.
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 42846 . . . . . . . . . . 11 (   𝐴𝐶   ▶   𝐴𝐶   )
2 sbceqg 4369 . . . . . . . . . . 11 (𝐴𝐶 → ([𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦} ↔ 𝐴 / 𝑥(𝐹 “ {𝐵}) = 𝐴 / 𝑥{𝑦}))
31, 2e1a 42899 . . . . . . . . . 10 (   𝐴𝐶   ▶   ([𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦} ↔ 𝐴 / 𝑥(𝐹 “ {𝐵}) = 𝐴 / 𝑥{𝑦})   )
4 csbima12 6031 . . . . . . . . . . . . . 14 𝐴 / 𝑥(𝐹 “ {𝐵}) = (𝐴 / 𝑥𝐹𝐴 / 𝑥{𝐵})
54a1i 11 . . . . . . . . . . . . 13 (𝐴𝐶𝐴 / 𝑥(𝐹 “ {𝐵}) = (𝐴 / 𝑥𝐹𝐴 / 𝑥{𝐵}))
61, 5e1a 42899 . . . . . . . . . . . 12 (   𝐴𝐶   ▶   𝐴 / 𝑥(𝐹 “ {𝐵}) = (𝐴 / 𝑥𝐹𝐴 / 𝑥{𝐵})   )
7 csbsng 4669 . . . . . . . . . . . . . 14 (𝐴𝐶𝐴 / 𝑥{𝐵} = {𝐴 / 𝑥𝐵})
81, 7e1a 42899 . . . . . . . . . . . . 13 (   𝐴𝐶   ▶   𝐴 / 𝑥{𝐵} = {𝐴 / 𝑥𝐵}   )
9 imaeq2 6009 . . . . . . . . . . . . 13 (𝐴 / 𝑥{𝐵} = {𝐴 / 𝑥𝐵} → (𝐴 / 𝑥𝐹𝐴 / 𝑥{𝐵}) = (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}))
108, 9e1a 42899 . . . . . . . . . . . 12 (   𝐴𝐶   ▶   (𝐴 / 𝑥𝐹𝐴 / 𝑥{𝐵}) = (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵})   )
11 eqeq1 2740 . . . . . . . . . . . . 13 (𝐴 / 𝑥(𝐹 “ {𝐵}) = (𝐴 / 𝑥𝐹𝐴 / 𝑥{𝐵}) → (𝐴 / 𝑥(𝐹 “ {𝐵}) = (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) ↔ (𝐴 / 𝑥𝐹𝐴 / 𝑥{𝐵}) = (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵})))
1211biimprd 247 . . . . . . . . . . . 12 (𝐴 / 𝑥(𝐹 “ {𝐵}) = (𝐴 / 𝑥𝐹𝐴 / 𝑥{𝐵}) → ((𝐴 / 𝑥𝐹𝐴 / 𝑥{𝐵}) = (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) → 𝐴 / 𝑥(𝐹 “ {𝐵}) = (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵})))
136, 10, 12e11 42960 . . . . . . . . . . 11 (   𝐴𝐶   ▶   𝐴 / 𝑥(𝐹 “ {𝐵}) = (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵})   )
14 csbconstg 3874 . . . . . . . . . . . 12 (𝐴𝐶𝐴 / 𝑥{𝑦} = {𝑦})
151, 14e1a 42899 . . . . . . . . . . 11 (   𝐴𝐶   ▶   𝐴 / 𝑥{𝑦} = {𝑦}   )
16 eqeq12 2753 . . . . . . . . . . . 12 ((𝐴 / 𝑥(𝐹 “ {𝐵}) = (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) ∧ 𝐴 / 𝑥{𝑦} = {𝑦}) → (𝐴 / 𝑥(𝐹 “ {𝐵}) = 𝐴 / 𝑥{𝑦} ↔ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}))
1716ex 413 . . . . . . . . . . 11 (𝐴 / 𝑥(𝐹 “ {𝐵}) = (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) → (𝐴 / 𝑥{𝑦} = {𝑦} → (𝐴 / 𝑥(𝐹 “ {𝐵}) = 𝐴 / 𝑥{𝑦} ↔ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦})))
1813, 15, 17e11 42960 . . . . . . . . . 10 (   𝐴𝐶   ▶   (𝐴 / 𝑥(𝐹 “ {𝐵}) = 𝐴 / 𝑥{𝑦} ↔ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦})   )
19 bibi1 351 . . . . . . . . . . 11 (([𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦} ↔ 𝐴 / 𝑥(𝐹 “ {𝐵}) = 𝐴 / 𝑥{𝑦}) → (([𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦} ↔ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}) ↔ (𝐴 / 𝑥(𝐹 “ {𝐵}) = 𝐴 / 𝑥{𝑦} ↔ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦})))
2019biimprd 247 . . . . . . . . . 10 (([𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦} ↔ 𝐴 / 𝑥(𝐹 “ {𝐵}) = 𝐴 / 𝑥{𝑦}) → ((𝐴 / 𝑥(𝐹 “ {𝐵}) = 𝐴 / 𝑥{𝑦} ↔ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}) → ([𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦} ↔ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦})))
213, 18, 20e11 42960 . . . . . . . . 9 (   𝐴𝐶   ▶   ([𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦} ↔ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦})   )
2221gen11 42888 . . . . . . . 8 (   𝐴𝐶   ▶   𝑦([𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦} ↔ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦})   )
23 abbi 2808 . . . . . . . . 9 (∀𝑦([𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦} ↔ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}) ↔ {𝑦[𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}})
2423biimpi 215 . . . . . . . 8 (∀𝑦([𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦} ↔ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}) → {𝑦[𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}})
2522, 24e1a 42899 . . . . . . 7 (   𝐴𝐶   ▶   {𝑦[𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}}   )
26 csbab 4397 . . . . . . . . 9 𝐴 / 𝑥{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦[𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦}}
2726a1i 11 . . . . . . . 8 (𝐴𝐶𝐴 / 𝑥{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦[𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦}})
281, 27e1a 42899 . . . . . . 7 (   𝐴𝐶   ▶   𝐴 / 𝑥{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦[𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦}}   )
29 eqeq2 2748 . . . . . . . 8 ({𝑦[𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}} → (𝐴 / 𝑥{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦[𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦}} ↔ 𝐴 / 𝑥{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}}))
3029biimpd 228 . . . . . . 7 ({𝑦[𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}} → (𝐴 / 𝑥{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦[𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦}} → 𝐴 / 𝑥{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}}))
3125, 28, 30e11 42960 . . . . . 6 (   𝐴𝐶   ▶   𝐴 / 𝑥{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}}   )
32 unieq 4876 . . . . . 6 (𝐴 / 𝑥{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}} → 𝐴 / 𝑥{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}})
3331, 32e1a 42899 . . . . 5 (   𝐴𝐶   ▶    𝐴 / 𝑥{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}}   )
34 csbuni 4897 . . . . . . 7 𝐴 / 𝑥 {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = 𝐴 / 𝑥{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}}
3534a1i 11 . . . . . 6 (𝐴𝐶𝐴 / 𝑥 {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = 𝐴 / 𝑥{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}})
361, 35e1a 42899 . . . . 5 (   𝐴𝐶   ▶   𝐴 / 𝑥 {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = 𝐴 / 𝑥{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}}   )
37 eqeq2 2748 . . . . . 6 ( 𝐴 / 𝑥{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}} → (𝐴 / 𝑥 {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = 𝐴 / 𝑥{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} ↔ 𝐴 / 𝑥 {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}}))
3837biimpd 228 . . . . 5 ( 𝐴 / 𝑥{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}} → (𝐴 / 𝑥 {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = 𝐴 / 𝑥{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} → 𝐴 / 𝑥 {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}}))
3933, 36, 38e11 42960 . . . 4 (   𝐴𝐶   ▶   𝐴 / 𝑥 {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}}   )
40 dffv4 6839 . . . . . 6 (𝐹𝐵) = {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}}
4140ax-gen 1797 . . . . 5 𝑥(𝐹𝐵) = {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}}
42 csbeq2 3860 . . . . . 6 (∀𝑥(𝐹𝐵) = {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} → 𝐴 / 𝑥(𝐹𝐵) = 𝐴 / 𝑥 {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}})
4342a1i 11 . . . . 5 (𝐴𝐶 → (∀𝑥(𝐹𝐵) = {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} → 𝐴 / 𝑥(𝐹𝐵) = 𝐴 / 𝑥 {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}}))
441, 41, 43e10 42966 . . . 4 (   𝐴𝐶   ▶   𝐴 / 𝑥(𝐹𝐵) = 𝐴 / 𝑥 {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}}   )
45 eqeq2 2748 . . . . 5 (𝐴 / 𝑥 {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}} → (𝐴 / 𝑥(𝐹𝐵) = 𝐴 / 𝑥 {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} ↔ 𝐴 / 𝑥(𝐹𝐵) = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}}))
4645biimpd 228 . . . 4 (𝐴 / 𝑥 {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}} → (𝐴 / 𝑥(𝐹𝐵) = 𝐴 / 𝑥 {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} → 𝐴 / 𝑥(𝐹𝐵) = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}}))
4739, 44, 46e11 42960 . . 3 (   𝐴𝐶   ▶   𝐴 / 𝑥(𝐹𝐵) = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}}   )
48 dffv4 6839 . . 3 (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵) = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}}
49 eqeq2 2748 . . . 4 ((𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵) = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}} → (𝐴 / 𝑥(𝐹𝐵) = (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵) ↔ 𝐴 / 𝑥(𝐹𝐵) = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}}))
5049biimprcd 249 . . 3 (𝐴 / 𝑥(𝐹𝐵) = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}} → ((𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵) = {𝑦 ∣ (𝐴 / 𝑥𝐹 “ {𝐴 / 𝑥𝐵}) = {𝑦}} → 𝐴 / 𝑥(𝐹𝐵) = (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵)))
5147, 48, 50e10 42966 . 2 (   𝐴𝐶   ▶   𝐴 / 𝑥(𝐹𝐵) = (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵)   )
5251in1 42843 1 (𝐴𝐶𝐴 / 𝑥(𝐹𝐵) = (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wal 1539   = wceq 1541  wcel 2106  {cab 2713  [wsbc 3739  csb 3855  {csn 4586   cuni 4865  cima 5636  cfv 6496
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 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-xp 5639  df-cnv 5641  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fv 6504  df-vd1 42842
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator